Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Makefile.extr 4.54 KB
Newer Older
1
2
3
4
5
6
7
8
#######################################################################
#                                                                     #
#              The Compcert verified compiler                         #
#                                                                     #
#          Xavier Leroy, INRIA Paris-Rocquencourt                     #
#                                                                     #
#  Copyright Institut National de Recherche en Informatique et en     #
#  Automatique.  All rights reserved.  This file is distributed       #
9
10
11
12
13
#  under the terms of the GNU Lesser General Public License as        #
#  published by the Free Software Foundation, either version 2.1 of   #
#  the License, or (at your option) any later version.                #
#  This file is also distributed under the terms of the               #
#  INRIA Non-Commercial License Agreement.                            #
14
15
16
17
18
19
20
#                                                                     #
#######################################################################

# Second-stage Makefile, after Coq extraction

include Makefile.config

21
22
#
# Variables from Makefile.config:
Xavier Leroy's avatar
Xavier Leroy committed
23
24
# -OCAML_NATIVE_COMP: native-code compilation is supported
# -OCAML_OPT_COMP: can we use the natively-compiled compilers
25
26
27
28
# -COMPFLAGS: compile options
# -LINK_OPT: additional linker flags for the native binary
#

29
# Menhir configuration.
30
31
32

include Makefile.menhir

33
34
35
36
37
38
#
# Variables from Makefile.menhir:
# -MENHIR_INCLUDES: additional menhir include paths
# -MENHIR_LIBS: additional menhir libraries
#

39
40
41
42
43
# The pre-parser's error message database is compiled as follows.

cparser/pre_parser_messages.ml:
	$(MAKE) -C cparser correct

44
# Directories containing plain Caml code
45

46
47
DIRS=extraction \
  lib common $(ARCH) backend cfrontend cparser driver \
48
  exportclight debug
49

50
INCLUDES=$(patsubst %,-I %, $(DIRS))
51

52
53
# Control of warnings:

54
WARNINGS=-w +a-4-9-27
55
56
extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45-60-67
extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45-60-67
57
58
cparser/pre_parser.cmx: WARNINGS += -w -41
cparser/pre_parser.cmo: WARNINGS += -w -41
59

60
61
62
63
64
65
66
67
# Turn warnings into errors, but not for released tarballs
ifeq ($(wildcard .git),.git)
WARN_ERRORS=-warn-error +a
else
WARN_ERRORS=
endif

COMPFLAGS+=-g -strict-sequence -safe-string $(INCLUDES) -I "$(MENHIR_DIR)" $(WARNINGS) $(WARN_ERRORS)
68
69

# Using .opt compilers if available
70

71
72
73
74
75
76
77
78
ifeq ($(OCAML_OPT_COMP),true)
DOTOPT=.opt
else
DOTOPT=
endif

OCAMLC=ocamlc$(DOTOPT) $(COMPFLAGS)
OCAMLOPT=ocamlopt$(DOTOPT) $(COMPFLAGS)
79
OCAMLDEP=ocamldep$(DOTOPT) -slash $(INCLUDES)
80

81
82
OCAMLLEX=ocamllex -q
MODORDER=tools/modorder .depend.extr
Xavier Leroy's avatar
Xavier Leroy committed
83
COPY=cp
84

85
86
87
PARSERS=cparser/pre_parser.mly
LEXERS=cparser/Lexer.mll lib/Tokenize.mll \
	     lib/Readconfig.mll lib/Responsefile.mll
88

89
90
91
LIBS=str.cmxa unix.cmxa $(MENHIR_LIBS)
LIBS_BYTE=$(patsubst %.cmxa,%.cma,$(patsubst %.cmx,%.cmo,$(LIBS)))

92
EXECUTABLES=ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte
93
GENERATED=$(PARSERS:.mly=.mli) $(PARSERS:.mly=.ml) $(LEXERS:.mll=.ml) cparser/pre_parser_messages.ml
94

95
96
# Beginning of part that assumes .depend.extr already exists

97
98
99
100
ifeq ($(wildcard .depend.extr),.depend.extr)

CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx)

Xavier Leroy's avatar
Xavier Leroy committed
101
ifeq ($(OCAML_NATIVE_COMP),true)
102
103
ccomp: $(CCOMP_OBJS)
	@echo "Linking $@"
104
	@$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+
Xavier Leroy's avatar
Xavier Leroy committed
105
106
107
108
109
else
ccomp: ccomp.byte
	@echo "Copying to $@"
	@$(COPY) $+ $@
endif
110
111
112

ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo)
	@echo "Linking $@"
113
	@$(OCAMLC) -o $@ $(LIBS_BYTE) $+
114
115
116

CLIGHTGEN_OBJS:=$(shell $(MODORDER) exportclight/Clightgen.cmx)

Xavier Leroy's avatar
Xavier Leroy committed
117
ifeq ($(OCAML_NATIVE_COMP),true)
118
119
clightgen: $(CLIGHTGEN_OBJS)
	@echo "Linking $@"
120
	@$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+
Xavier Leroy's avatar
Xavier Leroy committed
121
122
123
124
125
else
clightgen: clightgen.byte
	@echo "Copying to $@"
	@$(COPY) $+ $@
endif
126
127
128

clightgen.byte: $(CLIGHTGEN_OBJS:.cmx=.cmo)
	@echo "Linking $@"
129
	@$(OCAMLC) -o $@ $(LIBS_BYTE) $+
130
131
132
133
134

include .depend.extr

endif

135
136
# End of part that assumes .depend.extr already exists

137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
%.cmi: %.mli
	@echo "OCAMLC   $<"
	@$(OCAMLC) -c $<
%.cmo: %.ml
	@echo "OCAMLC   $<"
	@$(OCAMLC) -c $<
%.cmx: %.ml
	@echo "OCAMLOPT $<"
	@$(OCAMLOPT) -c $<

%.ml: %.mll
	$(OCAMLLEX) $<

clean:
	rm -f $(EXECUTABLES)
	rm -f $(GENERATED)
153
	for d in $(DIRS); do rm -f $$d/*.cm[iotx] $$d/*cmti $$d/*.o; done
154
	$(MAKE) -C cparser clean
155

156
157
# Generation of .depend.extr

158
159
depend: $(GENERATED)
	@echo "Analyzing OCaml dependencies"
160
161
	@$(OCAMLDEP) $(foreach d,$(DIRS),$(wildcard $(d)/*.ml)) $(GENERATED) >.depend.extr || { rm -f .depend.extr; exit 2; }
	@$(OCAMLDEP) $(foreach d,$(DIRS),$(wildcard $(d)/*.mli)) $(GENERATED) >>.depend.extr || { rm -f .depend.extr; exit 2; }