Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Newer
Older
100644 983 lines (760 sloc) 31.89 kb
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
1 #######################################################################
2 # v # The Coq Proof Assistant / The Coq Development Team #
3 # <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay #
4 # \VV/ #############################################################
5 # // # This file is distributed under the terms of the #
6 # # GNU Lesser General Public License Version 2.1 #
7 #######################################################################
8
8ec7f72 Makefile: cleanup of comments + a few words about recent changes in dev/...
letouzey authored
9 # This makefile is normally called by the main Makefile after setting
10 # some variables.
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
11
a3fda4a Makefile: no more separate stages
letouzey authored
12 ###########################################################################
13 # Starting rule
14 ###########################################################################
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
15
650f9c3 Configure + Makefile : simplification when -local
letouzey authored
16 # build the different subsystems: coq, coqide
3cb4411 Remove interface plugin
glondu authored
17 world: revision coq coqide
a3fda4a Makefile: no more separate stages
letouzey authored
18
19 ###########################################################################
20 # Includes
21 ###########################################################################
22
23 include Makefile.common
24 include Makefile.doc
25
650f9c3 Configure + Makefile : simplification when -local
letouzey authored
26 ifeq ($(LOCAL),true)
27 install:
28 @echo "Nothing to install in a local build!"
29 else
30 install: install-coq install-coqide install-doc-$(WITHDOC)
65ebb5f Ajout d'une option pour contrôler l'installation automatique de la docum...
notin authored
31 endif
32
650f9c3 Configure + Makefile : simplification when -local
letouzey authored
33 install-doc-all: install-doc
34 install-doc-no:
35
36 world: doc-$(WITHDOC)
37 doc-all: doc
38 doc-no:
39
40 .PHONY: world install install-doc-all install-doc-no doc-all doc-no
41
a3fda4a Makefile: no more separate stages
letouzey authored
42 # All dependency includes must be declared secondary, otherwise make will
43 # delete them if it decided to build them by dependency instead of because
44 # of include, and they will then be automatically deleted, leading to an
45 # infinite loop.
46
bf7cfcf Makefile: avoid too much exported vars (for win32)
letouzey authored
47 MLFILES:=$(MLSTATICFILES) $(MLEXTRAFILES)
48
49 ALLDEPS:=$(addsuffix .d, \
a3fda4a Makefile: no more separate stages
letouzey authored
50 $(ML4FILES) $(MLFILES) $(MLIFILES) $(CFILES) $(MLLIBFILES) $(VFILES))
51
bf7cfcf Makefile: avoid too much exported vars (for win32)
letouzey authored
52 .SECONDARY: $(ALLDEPS) $(GENFILES) $(ML4FILES:.ml4=.ml)
a3fda4a Makefile: no more separate stages
letouzey authored
53
54 # NOTA: the -include below will lauch the build of all .d. Some of them
55 # will _fail_ at first, this is to be expected (no grammar.cma initially).
6b010da Makefile: some more cleanup
letouzey authored
56 # These errors (see below "not ready yet") do not discourage make to
57 # try again and finally succeed.
a3fda4a Makefile: no more separate stages
letouzey authored
58
59 -include $(ALLDEPS)
60
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
61
62 ###########################################################################
63 # Compilation options
64 ###########################################################################
65
6b010da Makefile: some more cleanup
letouzey authored
66 # Variables meant to be modifiable via the command-line of make
67
68 VERBOSE=
69 NO_RECOMPILE_ML4=
70 NO_RECALC_DEPS=
71 READABLE_ML4= # non-empty means .ml of .ml4 will be ascii instead of binary
72 VALIDATE=
73 COQ_XML= # is "-xml" when building XML library
74 VM= # is "-no-vm" to not use the vm"
75
41451e5 Makefile.build: easier compilation with timings info
letouzey authored
76 TIMED= # non-empty will activate a default time command
77 # when compiling .v (see $(STDTIME) below)
78
79 TIMECMD= # if you prefer a specific time command instead of $(STDTIME)
80 # e.g. "'time -p'"
81
82 # NB: if you want to collect compilation timings of .v and import them
83 # in a spreadsheet, I suggest something like:
84 # make TIMED=1 2> timings.csv
85
86 # NB: do not use a variable named TIME, since this variable controls
87 # the output format of the unix command time. For instance:
88 # TIME="%C (%U user, %S sys, %e total, %M maxres)"
89
90 STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)"
91 TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
6b010da Makefile: some more cleanup
letouzey authored
92
637e67a Makefile.build: states/initial.coq was wrongly done with -dont-load-proo...
letouzey authored
93 COQOPTS=$(COQ_XML) $(VM)
41451e5 Makefile.build: easier compilation with timings info
letouzey authored
94 BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
6b010da Makefile: some more cleanup
letouzey authored
95
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
96 # The SHOW and HIDE variables control whether make will echo complete commands
97 # or only abbreviated versions.
98 # Quiet mode is ON by default except if VERBOSE=1 option is given to make
99
6b010da Makefile: some more cleanup
letouzey authored
100 SHOW := $(if $(VERBOSE),@true "",@echo "")
101 HIDE := $(if $(VERBOSE),,@)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
102
55c214e ajout de la tactique groebner de Loic Pottier
barras authored
103 LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) )
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
104 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
391ecb0 Port from 8.4 branch some build fixes concerning win32 :
letouzey authored
105 COREMLINCLUDES=$(addprefix -I , $(CORESRCDIRS)) -I $(MYCAMLP4LIB)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
106
5ea279d @aspiwack Tentative and very experminental support for typerex. Enabled with
aspiwack authored
107 OCAMLC := $(TYPEREX) $(OCAMLC) $(CAMLFLAGS)
108 OCAMLOPT := $(TYPEREX) $(OCAMLOPT) $(CAMLFLAGS)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
109
110 BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS)
3f4cadb Fix caml debug flags configuration, -g works with the native compiler on...
msozeau authored
111 OPTFLAGS=$(MLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
391ecb0 Port from 8.4 branch some build fixes concerning win32 :
letouzey authored
112 COREBYTEFLAGS=$(COREMLINCLUDES) $(CAMLDEBUG) $(USERFLAGS)
113 COREOPTFLAGS=$(COREMLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
e19ab99 Compilation sous windows
notin authored
114 DEPFLAGS= -slash $(LOCALINCLUDES)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
115
6b010da Makefile: some more cleanup
letouzey authored
116 define bestocaml
117 $(if $(OPT),\
118 $(OCAMLOPT) $(OPTFLAGS) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@,\
119 $(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(1) $(addsuffix .cma,$(2)) $^)
120 endef
5ca33dc use TIMECMD instead of TIME in makefile (unix cmd time reads its format ...
letouzey authored
121
c182c9e @pirbo Fixup for macOS 10.8 & Ocaml 4.0
pirbo authored
122 CAMLP4DEPS=$(shell LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $(1) \#))
1b089eb Add (almost) compatibility with camlp4, without breaking support for cam...
letouzey authored
123 ifeq ($(CAMLP4),camlp5)
6af0706 static (and shared) camlp4use instead of per-file declaration
letouzey authored
124 CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
1b089eb Add (almost) compatibility with camlp4, without breaking support for cam...
letouzey authored
125 else
126 CAMLP4USE=-D$(CAMLVERSION)
127 endif
128
129 PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) # works also with new camlp4
130
4e0def8 no need for camlp4 cma's in coq misc tools
letouzey authored
131 SYSMOD:=str unix
132 SYSCMA:=$(addsuffix .cma,$(SYSMOD))
133 SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD))
134
1b089eb Add (almost) compatibility with camlp4, without breaking support for cam...
letouzey authored
135 ifeq ($(CAMLP4),camlp5)
4e0def8 no need for camlp4 cma's in coq misc tools
letouzey authored
136 P4CMA:=gramlib.cma
1b089eb Add (almost) compatibility with camlp4, without breaking support for cam...
letouzey authored
137 else
4e0def8 no need for camlp4 cma's in coq misc tools
letouzey authored
138 P4CMA:=dynlink.cma camlp4lib.cma
1b089eb Add (almost) compatibility with camlp4, without breaking support for cam...
letouzey authored
139 endif
140
58a5a53 Makefile: the .ml of .ml4 are now produced explicitely (in binary ast fo...
letouzey authored
141
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
142 ###########################################################################
143 # Infrastructure for the rest of the Makefile
144 ###########################################################################
145
146 define order-only-template
147 ifeq "order-only" "$(1)"
148 ORDER_ONLY_SEP:=|
149 endif
150 endef
151
152 $(foreach f,$(.FEATURES),$(eval $(call order-only-template,$(f))))
153
e16dafd Makefile: needs GNU Make 3.81
lmamane authored
154 ifndef ORDER_ONLY_SEP
155 $(error This Makefile needs GNU Make 3.81 or later (that is a version that supports the order-only dependency feature without major bugs.))
156 endif
157
492ad5a No more coqtop.opt, produce directly a coqtop binary
letouzey authored
158 VO_TOOLS_DEP := $(COQTOPEXE)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
159 ifdef COQ_XML
160 VO_TOOLS_DEP += $(COQDOC)
161 endif
dc25e1b added coqchk to the main Makefile and a make variable VALIDATE to check ...
barras authored
162 ifdef VALIDATE
492ad5a No more coqtop.opt, produce directly a coqtop binary
letouzey authored
163 VO_TOOLS_DEP += $(CHICKEN)
dc25e1b added coqchk to the main Makefile and a make variable VALIDATE to check ...
barras authored
164 endif
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
165
ca4775a Implement NO_RECALC_DEPS option in build system
lmamane authored
166 ifdef NO_RECALC_DEPS
167 D_DEPEND_BEFORE_SRC:=|
168 D_DEPEND_AFTER_SRC:=
169 else
170 D_DEPEND_BEFORE_SRC:=
171 D_DEPEND_AFTER_SRC:=|
172 endif
173
4d44ec1 Makefile: hide the trick ...||(RV=$$?;rm $@; exit $${RV}) under a macro ...
letouzey authored
174 ## When a rule redirects stdout of a command to the target file : cmd > $@
175 ## then the target file will be created even if cmd has failed.
176 ## Hence relaunching make will go further, as make thinks the target has been
177 ## done ok. To avoid this, we use the following macro:
178
179 TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV})
180
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
181 ###########################################################################
182 # Compilation option for .c files
183 ###########################################################################
184
185 CINCLUDES= -I $(CAMLHLIB)
186
0f4d785 Build coqrun library using ocamlmklib...
glondu authored
187 # libcoqrun.a, dllcoqrun.so
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
188
66267d4 Simpler configure: gcc via ocamlc, no ranlib (done by ocamlmklib)
letouzey authored
189 # NB: We used to do a ranlib after ocamlmklib, but it seems that
190 # ocamlmklib is already doing it
191
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
192 $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN)
0f4d785 Build coqrun library using ocamlmklib...
glondu authored
193 cd $(dir $(LIBCOQRUN)) && \
194 $(OCAMLMKLIB) -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u)))
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
195
196 #coq_jumptbl.h is required only if you have GCC 2.0 or later
197 kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h
198 sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \
4d44ec1 Makefile: hide the trick ...||(RV=$$?;rm $@; exit $${RV}) under a macro ...
letouzey authored
199 -e '/^}/q' $< $(TOTARGET)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
200
201 kernel/copcodes.ml: kernel/byterun/coq_instruct.h
4d44ec1 Makefile: hide the trick ...||(RV=$$?;rm $@; exit $${RV}) under a macro ...
letouzey authored
202 sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' $< | \
203 awk -f kernel/make-opcodes $(TOTARGET)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
204
205 ###########################################################################
206 # Main targets (coqmktop, coqtop.opt, coqtop.byte)
207 ###########################################################################
208
9dc9bd9 Various fixes in the Makefiles
letouzey authored
209 .PHONY: coqbinaries coq coqlib coqlight states
210
8421370 make world now builds fake_ide (to please coq-bench)
letouzey authored
211 coqbinaries:: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE}
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
212
213 coq: coqlib tools coqbinaries
214
7d220f8 Directory 'contrib' renamed into 'plugins', to end confusion with archiv...
letouzey authored
215 coqlib:: theories plugins
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
216
9cdf9c3 - coq_makefile: target install now respects the original tree structure
herbelin authored
217 coqlight: theories-light tools coqbinaries
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
218
12def92 No more states/initial.coq, instead coqtop now requires Prelude.vo
letouzey authored
219 states: theories/Init/Prelude.vo
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
220
62aa6ad New makefile shortcuts miniopt and minibyte for coqtop + plugins
letouzey authored
221 miniopt: $(COQTOPEXE) pluginsopt
222 minibyte: $(COQTOPBYTE) pluginsbyte
223
492ad5a No more coqtop.opt, produce directly a coqtop binary
letouzey authored
224 ifeq ($(BEST),opt)
225 $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
226 $(SHOW)'COQMKTOP -o $@'
391ecb0 Port from 8.4 branch some build fixes concerning win32 :
letouzey authored
227 $(HIDE)$(COQMKTOP) -boot -opt $(COREOPTFLAGS) -o $@
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
228 $(STRIP) $@
492ad5a No more coqtop.opt, produce directly a coqtop binary
letouzey authored
229 else
230 $(COQTOPEXE): $(COQTOPBYTE)
231 cp $< $@
232 endif
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
233
59c9403 @pirbo lib directory is cut in 2 cma.
pirbo authored
234 $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
235 $(SHOW)'COQMKTOP -o $@'
391ecb0 Port from 8.4 branch some build fixes concerning win32 :
letouzey authored
236 $(HIDE)$(COQMKTOP) -boot -top $(COREBYTEFLAGS) -o $@
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
237
55c214e ajout de la tactique groebner de Loic Pottier
barras authored
238 LOCALCHKLIBS:=$(addprefix -I , $(CHKSRCDIRS) )
313de91 improved coqchk targets
barras authored
239 CHKLIBS:=$(LOCALCHKLIBS) -I $(MYCAMLP4LIB)
240 CHKBYTEFLAGS:=$(CHKLIBS) $(CAMLDEBUG) $(USERFLAGS)
451f477 the -g option is not recongnized in ocaml < 3.10.0
jforest authored
241 CHKOPTFLAGS:=$(CHKLIBS) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
dc25e1b added coqchk to the main Makefile and a make variable VALIDATE to check ...
barras authored
242
492ad5a No more coqtop.opt, produce directly a coqtop binary
letouzey authored
243 ifeq ($(BEST),opt)
244 $(CHICKEN): checker/check.cmxa checker/main.ml
dc25e1b added coqchk to the main Makefile and a make variable VALIDATE to check ...
barras authored
245 $(SHOW)'OCAMLOPT -o $@'
1b089eb Add (almost) compatibility with camlp4, without breaking support for cam...
letouzey authored
246 $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ $(SYSCMXA) $^
dc25e1b added coqchk to the main Makefile and a make variable VALIDATE to check ...
barras authored
247 $(STRIP) $@
492ad5a No more coqtop.opt, produce directly a coqtop binary
letouzey authored
248 else
249 $(CHICKEN): $(CHICKENBYTE)
250 cp $< $@
251 endif
dc25e1b added coqchk to the main Makefile and a make variable VALIDATE to check ...
barras authored
252
253 $(CHICKENBYTE): checker/check.cma checker/main.ml
254 $(SHOW)'OCAMLC -o $@'
1b089eb Add (almost) compatibility with camlp4, without breaking support for cam...
letouzey authored
255 $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(SYSCMA) $^
dc25e1b added coqchk to the main Makefile and a make variable VALIDATE to check ...
barras authored
256
59c9403 @pirbo lib directory is cut in 2 cma.
pirbo authored
257 # coqmktop
258 $(COQMKTOP): $(patsubst %.cma,%$(BESTLIB),$(COQMKTOPCMO:.cmo=$(BESTOBJ)))
259 $(SHOW)'OCAMLBEST -o $@'
260 $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
261
262 scripts/tolink.ml: Makefile.build Makefile.common
263 $(SHOW)"ECHO... >" $@
264 $(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@
265 $(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@
dffb615 Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey authored
266 $(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
267
268 # coqc
59c9403 @pirbo lib directory is cut in 2 cma.
pirbo authored
269 $(COQC): $(patsubst %.cma,%$(BESTLIB),$(COQCCMO:.cmo=$(BESTOBJ)))
270 $(SHOW)'OCAMLBEST -o $@'
271 $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
272
273 # target for libraries
274
dffb615 Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey authored
275 %.cma: | %.mllib.d
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
276 $(SHOW)'OCAMLC -a -o $@'
c215c44 Take advantage of natdynlink when available: almost all contribs become ...
letouzey authored
277 $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $^
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
278
dffb615 Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey authored
279 %.cmxa: | %.mllib.d
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
280 $(SHOW)'OCAMLOPT -a -o $@'
c215c44 Take advantage of natdynlink when available: almost all contribs become ...
letouzey authored
281 $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $^
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
282
c215c44 Take advantage of natdynlink when available: almost all contribs become ...
letouzey authored
283 # For the checker, different flags may be used
284
dffb615 Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey authored
285 checker/check.cma: | checker/check.mllib.d
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
286 $(SHOW)'OCAMLC -a -o $@'
c215c44 Take advantage of natdynlink when available: almost all contribs become ...
letouzey authored
287 $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -a -o $@ $^
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
288
dffb615 Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey authored
289 checker/check.cmxa: | checker/check.mllib.d
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
290 $(SHOW)'OCAMLOPT -a -o $@'
c215c44 Take advantage of natdynlink when available: almost all contribs become ...
letouzey authored
291 $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -a -o $@ $^
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
292
293 ###########################################################################
7c51ef2 Intégration de micromega ("omicron" pour fourier et sa variante sur Z,
herbelin authored
294 # Csdp to micromega special targets
295 ###########################################################################
296
6b010da Makefile: some more cleanup
letouzey authored
297 plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ))
298 $(SHOW)'OCAMLBEST -o $@'
299 $(HIDE)$(call bestocaml,,nums unix)
7c51ef2 Intégration de micromega ("omicron" pour fourier et sa variante sur Z,
herbelin authored
300
301 ###########################################################################
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
302 # CoqIde special targets
303 ###########################################################################
304
9dc9bd9 Various fixes in the Makefiles
letouzey authored
305 .PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files
306
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
307 # target to build CoqIde
f0b936e @pirbo Fix coqide compilation with lablgtk 2.16
pirbo authored
308 coqide:: coqide-files coqide-binaries theories/Init/Prelude.vo
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
309
302482b Ajout option -lablgtkdir au configure (basé sur patch de Guillaume
herbelin authored
310 COQIDEFLAGS=-thread $(COQIDEINCLUDES)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
311
312 .SUFFIXES:.vo
313
fed7d0f @pirbo Coqide highligthing is back (done by gtksourceview).
pirbo authored
314 IDEFILES=ide/coq.lang ide/coq_style.xml ide/coq.png ide/mac_default_accel_map
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
315
316 coqide-binaries: coqide-$(HASCOQIDE)
317 coqide-no:
318 coqide-byte: $(COQIDEBYTE) $(COQIDE)
492ad5a No more coqtop.opt, produce directly a coqtop binary
letouzey authored
319 coqide-opt: $(COQIDEBYTE) $(COQIDE)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
320 coqide-files: $(IDEFILES)
321
492ad5a No more coqtop.opt, produce directly a coqtop binary
letouzey authored
322 ifeq ($(HASCOQIDE),opt)
323 $(COQIDE): $(LINKIDEOPT) | $(COQTOPEXE)
ccfcc92 @pirbo Coqide is not built with coqmktop any more
pirbo authored
324 $(SHOW)'OCAMLOPT -o $@'
a6dac99 @pirbo MacOS integration uses lablgtkosx >= 1.1
pirbo authored
325 $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa \
326 lablgtk.cmxa lablgtksourceview2.cmxa $(IDEOPTFLAGS) gtkThread.cmx \
327 str.cmxa $(LINKIDEOPT)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
328 $(STRIP) $@
492ad5a No more coqtop.opt, produce directly a coqtop binary
letouzey authored
329 else
330 $(COQIDE): $(COQIDEBYTE)
331 cp $< $@
332 endif
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
333
27aa815 @pirbo weak dependency of coqtop for coqide and coqc (bug 2390)
pirbo authored
334 $(COQIDEBYTE): $(LINKIDE) | $(COQTOPBYTE)
da9f320 @pirbo Makefile.build typo in echo
pirbo authored
335 $(SHOW)'OCAMLC -o $@'
88a931f @pirbo Configure asks for lablgtk >= 2.12 with gtksourceview2
pirbo authored
336 $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma\
337 lablgtksourceview2.cma gtkThread.cmo str.cma $(COQRUNBYTEFLAGS) $(LINKIDE)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
338
339 # install targets
340
9dc9bd9 Various fixes in the Makefiles
letouzey authored
341 .PHONY: install-coqide install-ide-no install-ide-byte install-ide-opt
21bb352 @pirbo Makefile.build: add targets install-devfiles and install-ide-devfiles
pirbo authored
342 .PHONY: install-ide-files install-ide-info install-im install-ide-devfiles
9dc9bd9 Various fixes in the Makefiles
letouzey authored
343
b373c5b Makefile: revised install-coqide rule
letouzey authored
344 ifeq ($(HASCOQIDE),no)
345 install-coqide:
346 else
347 install-coqide: install-ide-bin install-ide-files install-ide-info install-ide-devfiles
348 endif
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
349
b373c5b Makefile: revised install-coqide rule
letouzey authored
350 install-ide-bin:
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
351 $(MKDIR) $(FULLBINDIR)
b373c5b Makefile: revised install-coqide rule
letouzey authored
352 $(INSTALLBIN) $(COQIDE) $(FULLBINDIR)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
353
21bb352 @pirbo Makefile.build: add targets install-devfiles and install-ide-devfiles
pirbo authored
354 install-ide-devfiles:
355 $(MKDIR) $(FULLCOQLIB)
356 $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \
357 $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib))))
358 ifeq ($(BEST),opt)
359 $(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a)
360 endif
361
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
362 install-ide-files:
5536b6d @pirbo CoqIde files position is freedesktop compliant.
pirbo authored
363 $(MKDIR) $(FULLDATADIR)
fed7d0f @pirbo Coqide highligthing is back (done by gtksourceview).
pirbo authored
364 $(INSTALLLIB) ide/coq.png ide/coq.lang ide/coq_style.xml $(FULLDATADIR)
5e62a6a @pirbo coqide default pref files are by default in /etc/xdg/coq/
pirbo authored
365 $(MKDIR) $(FULLCONFIGDIR)
366 if [ $(IDEOPTINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
367
368 install-ide-info:
5536b6d @pirbo CoqIde files position is freedesktop compliant.
pirbo authored
369 $(MKDIR) $(FULLDOCDIR)
370 $(INSTALLLIB) ide/FAQ $(FULLDOCDIR)/FAQ-CoqIde
afd1cb8 Polishing the setup of CoqIDE Input Method
vgross authored
371
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
372 ###########################################################################
373 # tests
374 ###########################################################################
375
9dc9bd9 Various fixes in the Makefiles
letouzey authored
376 .PHONY: validate check test-suite $(ALLSTDLIB).v
377
dc1f525 porting r11900 11905 and 11953 to trunk
barras authored
378 VALIDOPTS=-silent -o -m
379
492ad5a No more coqtop.opt, produce directly a coqtop binary
letouzey authored
380 validate:: $(CHICKEN) $(ALLVO)
7d220f8 Directory 'contrib' renamed into 'plugins', to end confusion with archiv...
letouzey authored
381 $(SHOW)'COQCHK <theories & plugins>'
492ad5a No more coqtop.opt, produce directly a coqtop binary
letouzey authored
382 $(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
3e314a8 added Makefile target: validate (to recheck all .vo in a row)
barras authored
383
8966d62 Add a test for sorting all universes of stdlib
glondu authored
384 $(ALLSTDLIB).v:
385 $(SHOW)'MAKE $(notdir $@)'
386 $(HIDE)echo "Require $(ALLMODS)." > $@
387
492ad5a No more coqtop.opt, produce directly a coqtop binary
letouzey authored
388 MAKE_TSOPTS=-C test-suite -s VERBOSE=$(VERBOSE)
ffa867c Run parallelized test-suite in "check" target of main Makefile
glondu authored
389
0743e5a Re-enable validation in "make check", run it in parallel with test-suite
glondu authored
390 check:: validate test-suite
391
8421370 make world now builds fake_ide (to please coq-bench)
letouzey authored
392 test-suite: world $(ALLSTDLIB).v
ffa867c Run parallelized test-suite in "check" target of main Makefile
glondu authored
393 $(MAKE) $(MAKE_TSOPTS) clean
394 $(MAKE) $(MAKE_TSOPTS) all
395 $(HIDE)if grep -F 'Error!' test-suite/summary.log ; then false; fi
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
396
dffb615 Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey authored
397 ##################################################################
398 # partial targets: 1) core ML parts
399 ##################################################################
400
9dc9bd9 Various fixes in the Makefiles
letouzey authored
401 .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping
402 .PHONY: highparsing toplevel hightactics
403
59c9403 @pirbo lib directory is cut in 2 cma.
pirbo authored
404 lib: lib/clib.cma lib/lib.cma
dffb615 Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey authored
405 kernel: kernel/kernel.cma
406 byterun: $(BYTERUN)
407 library: library/library.cma
408 proofs: proofs/proofs.cma
409 tactics: tactics/tactics.cma
410 interp: interp/interp.cma
411 parsing: parsing/parsing.cma
412 pretyping: pretyping/pretyping.cma
413 highparsing: parsing/highparsing.cma
414 toplevel: toplevel/toplevel.cma
415 hightactics: tactics/hightactics.cma
416
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
417 ###########################################################################
dffb615 Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey authored
418 # 2) theories and plugins files
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
419 ###########################################################################
420
9dc9bd9 Various fixes in the Makefiles
letouzey authored
421 .PHONY: init theories theories-light
422 .PHONY: logic arith bool narith zarith qarith lists strings sets
423 .PHONY: fsets relations wellfounded reals setoids sorting numbers noreal
424
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
425 init: $(INITVO)
426
427 theories: $(THEORIESVO)
428 theories-light: $(THEORIESLIGHTVO)
429
430 logic: $(LOGICVO)
431 arith: $(ARITHVO)
432 bool: $(BOOLVO)
433 narith: $(NARITHVO)
434 zarith: $(ZARITHVO)
435 qarith: $(QARITHVO)
436 lists: $(LISTSVO)
437 strings: $(STRINGSVO)
438 sets: $(SETSVO)
439 fsets: $(FSETSVO)
440 relations: $(RELATIONSVO)
441 wellfounded: $(WELLFOUNDEDVO)
442 reals: $(REALSVO)
443 setoids: $(SETOIDSVO)
444 sorting: $(SORTINGVO)
445 numbers: $(NUMBERSVO)
01d92cf Completed list of theories targets
herbelin authored
446 unicode: $(UNICODEVO)
447 classes: $(CLASSESVO)
448 program: $(PROGRAMVO)
449 structures: $(STRUCTURESVO)
450 vectors: $(VECTORSVO)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
451
f4d8159 Do not forget to build the unicode libraries, necessary to compile and l...
msozeau authored
452 noreal: unicode logic arith bool zarith qarith lists sets fsets \
453 relations wellfounded setoids sorting
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
454
455 ###########################################################################
3cb4411 Remove interface plugin
glondu authored
456 # 3) plugins
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
457 ###########################################################################
458
2ed6aeb Legacy Ring and Legacy Field migrated to contribs
letouzey authored
459 .PHONY: plugins omega micromega setoid_ring nsatz xml extraction
62aa6ad New makefile shortcuts miniopt and minibyte for coqtop + plugins
letouzey authored
460 .PHONY: fourier funind cc rtauto btauto pluginsopt pluginsbyte
9dc9bd9 Various fixes in the Makefiles
letouzey authored
461
7d220f8 Directory 'contrib' renamed into 'plugins', to end confusion with archiv...
letouzey authored
462 plugins: $(PLUGINSVO)
eb93dfa Makefile: ml dependencies of contribs are moved to .mllib files
letouzey authored
463 omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA)
464 micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT)
2ed6aeb Legacy Ring and Legacy Field migrated to contribs
letouzey authored
465 setoid_ring: $(RINGVO) $(RINGCMA)
da2a0a4 Backporting modifications to nsatz (doc + fix of bug #2328) from trunk t...
herbelin authored
466 nsatz: $(NSATZVO) $(NSATZCMA)
eb93dfa Makefile: ml dependencies of contribs are moved to .mllib files
letouzey authored
467 xml: $(XMLVO) $(XMLCMA)
468 extraction: $(EXTRACTIONCMA)
469 fourier: $(FOURIERVO) $(FOURIERCMA)
470 funind: $(FUNINDCMA) $(FUNINDVO)
471 cc: $(CCVO) $(CCCMA)
472 rtauto: $(RTAUTOVO) $(RTAUTOCMA)
28000ea @ppedrot Added a Btauto plugin, that solves boolean tautologies.
ppedrot authored
473 btauto: $(BTAUTOVO) $(BTAUTOCMA)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
474
b36e75c Extraction: allow to use Extraction Inline / NoInline even from under a ...
letouzey authored
475 pluginsopt: $(PLUGINSOPT)
62aa6ad New makefile shortcuts miniopt and minibyte for coqtop + plugins
letouzey authored
476 pluginsbyte: $(PLUGINS)
b36e75c Extraction: allow to use Extraction Inline / NoInline even from under a ...
letouzey authored
477
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
478 ###########################################################################
12def92 No more states/initial.coq, instead coqtop now requires Prelude.vo
letouzey authored
479 # rules to make theories and plugins
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
480 ###########################################################################
481
ac98362 Remove broken makefile option NO_RECOMPILE_LIB
letouzey authored
482 theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/%.v.d
12def92 No more states/initial.coq, instead coqtop now requires Prelude.vo
letouzey authored
483 $(SHOW)'COQC -noinit $<'
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
484 $(HIDE)rm -f theories/Init/$*.glob
12def92 No more states/initial.coq, instead coqtop now requires Prelude.vo
letouzey authored
485 $(HIDE)$(BOOTCOQC) theories/Init/$* -noinit
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
486
a7f2497 NMake: several things need not be macro-generated
letouzey authored
487 theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml
4d44ec1 Makefile: hide the trick ...||(RV=$$?;rm $@; exit $${RV}) under a macro ...
letouzey authored
488 $(OCAML) $< $(TOTARGET)
e5a5332 Integration of theories/Ints into theories/Numbers, part 3: auto-generat...
letouzey authored
489
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
490 ###########################################################################
491 # tools
492 ###########################################################################
493
9dc9bd9 Various fixes in the Makefiles
letouzey authored
494 .PHONY: printers tools
495
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
496 printers: $(DEBUGPRINTERS)
497
a4d3729 make coqdep_boot in stage1, not stage2
lmamane authored
498 tools:: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
499
251b34a avoid dependency nightmare by creating coqdep_{lexer,common}.mli
letouzey authored
500 # coqdep_boot : a basic version of coqdep, with almost no dependencies.
d63dee2 coqdep_boot: a specialized and dependency-free coqdep for killing one of...
letouzey authored
501
251b34a avoid dependency nightmare by creating coqdep_{lexer,common}.mli
letouzey authored
502 # Here it is important to mention .ml files instead of .cmo in order
503 # to avoid using implicit rules and hence .ml.d files that would need
504 # coqdep_boot.
505
506 COQDEPBOOTSRC:= \
507 tools/coqdep_lexer.mli tools/coqdep_lexer.ml \
508 tools/coqdep_common.mli tools/coqdep_common.ml \
509 tools/coqdep_boot.ml
510
511 $(COQDEPBOOT): $(COQDEPBOOTSRC)
6b010da Makefile: some more cleanup
letouzey authored
512 $(SHOW)'OCAMLBEST -o $@'
513 $(HIDE)$(call bestocaml, -I tools, unix)
d63dee2 coqdep_boot: a specialized and dependency-free coqdep for killing one of...
letouzey authored
514
515 # the full coqdep
516
59c9403 @pirbo lib directory is cut in 2 cma.
pirbo authored
517 $(COQDEP): $(patsubst %.cma,%$(BESTLIB),$(COQDEPCMO:.cmo=$(BESTOBJ)))
6b010da Makefile: some more cleanup
letouzey authored
518 $(SHOW)'OCAMLBEST -o $@'
1b089eb Add (almost) compatibility with camlp4, without breaking support for cam...
letouzey authored
519 $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
520
6b010da Makefile: some more cleanup
letouzey authored
521 $(GALLINA): $(addsuffix $(BESTOBJ), tools/gallina_lexer tools/gallina)
522 $(SHOW)'OCAMLBEST -o $@'
523 $(HIDE)$(call bestocaml,,)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
524
8837c23 @pirbo Revert copy/pasted function in to minilib thanks to clib.cma
pirbo authored
525 $(COQMAKEFILE): $(patsubst %.cma,%$(BESTLIB),$(COQMAKEFILECMO:.cmo=$(BESTOBJ)))
6b010da Makefile: some more cleanup
letouzey authored
526 $(SHOW)'OCAMLBEST -o $@'
0d72756 @pirbo same_file in Minilib
pirbo authored
527 $(HIDE)$(call bestocaml,,str unix)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
528
6b010da Makefile: some more cleanup
letouzey authored
529 $(COQTEX): tools/coq_tex$(BESTOBJ)
530 $(SHOW)'OCAMLBEST -o $@'
531 $(HIDE)$(call bestocaml,,str)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
532
6b010da Makefile: some more cleanup
letouzey authored
533 $(COQWC): tools/coqwc$(BESTOBJ)
534 $(SHOW)'OCAMLBEST -o $@'
535 $(HIDE)$(call bestocaml,,)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
536
59c9403 @pirbo lib directory is cut in 2 cma.
pirbo authored
537 $(COQDOC): $(patsubst %.cma,%$(BESTLIB),$(COQDOCCMO:.cmo=$(BESTOBJ)))
6b010da Makefile: some more cleanup
letouzey authored
538 $(SHOW)'OCAMLBEST -o $@'
539 $(HIDE)$(call bestocaml,,str unix)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
540
0298861 fake_ide: a short program to mimic an ide talking to coqtop -ideslave
letouzey authored
541 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
542 # a connection to coqtop -ideslave
543
59c9403 @pirbo lib directory is cut in 2 cma.
pirbo authored
544 $(FAKEIDE): lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_utils$(BESTOBJ) lib/serialize$(BESTOBJ) tools/fake_ide$(BESTOBJ)
0298861 fake_ide: a short program to mimic an ide talking to coqtop -ideslave
letouzey authored
545 $(SHOW)'OCAMLBEST -o $@'
546 $(HIDE)$(call bestocaml,,unix)
547
25533df Finish adding out-of-the-box support for camlp4
letouzey authored
548 # Special rule for the compatibility-with-camlp5 extension for camlp4
549
550 ifeq ($(CAMLP4),camlp4)
551 tools/compat5.cmo: tools/compat5.mlp
335a3d9 Win32: some quote fixes
letouzey authored
552 $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $<
25533df Finish adding out-of-the-box support for camlp4
letouzey authored
553 tools/compat5b.cmo: tools/compat5b.mlp
335a3d9 Win32: some quote fixes
letouzey authored
554 $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $<
25533df Finish adding out-of-the-box support for camlp4
letouzey authored
555 else
556 tools/compat5.cmo: tools/compat5.ml
557 $(OCAMLC) -c $<
558 tools/compat5b.cmo: tools/compat5b.ml
559 $(OCAMLC) -c $<
560 endif
561
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
562 ###########################################################################
563 # Installation
564 ###########################################################################
565
5e88ae6 Quelques amendements liées à la compilation des packages.
herbelin authored
566 #These variables are intended to be set by the caller to make
567 #COQINSTALLPREFIX=
568 #OLDROOT=
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
569
570 # Can be changed for a local installation (to make packages).
571 # You must NOT put a "/" at the end (Cygnus for win32 does not like "//").
572
bffe056 Makefile.build: avoid warning about undefined variable during make insta...
letouzey authored
573 ifdef COQINSTALLPREFIX
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
574 FULLBINDIR=$(BINDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
677b63f $(COQLIB) -> $(COQLIBINSTALL) in Makefiles
glondu authored
575 FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
5e62a6a @pirbo coqide default pref files are by default in /etc/xdg/coq/
pirbo authored
576 FULLCONFIGDIR=$(CONFIGDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
5536b6d @pirbo CoqIde files position is freedesktop compliant.
pirbo authored
577 FULLDATADIR=$(DATADIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
578 FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
579 FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
580 FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
26b8d44 Use COQINSTALLPREFIX for doc too
glondu authored
581 FULLDOCDIR=$(DOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
bffe056 Makefile.build: avoid warning about undefined variable during make insta...
letouzey authored
582 else
583 FULLBINDIR=$(BINDIR)
584 FULLCOQLIB=$(COQLIBINSTALL)
5e62a6a @pirbo coqide default pref files are by default in /etc/xdg/coq/
pirbo authored
585 FULLCONFIGDIR=$(CONFIGDIR)
5536b6d @pirbo CoqIde files position is freedesktop compliant.
pirbo authored
586 FULLDATADIR=$(DATADIR)
bffe056 Makefile.build: avoid warning about undefined variable during make insta...
letouzey authored
587 FULLMANDIR=$(MANDIR)
588 FULLEMACSLIB=$(EMACSLIB)
589 FULLCOQDOCDIR=$(COQDOCDIR)
590 FULLDOCDIR=$(DOCDIR)
591 endif
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
592
9dc9bd9 Various fixes in the Makefiles
letouzey authored
593 .PHONY: install-coq install-coqlight install-binaries install-byte install-opt
21bb352 @pirbo Makefile.build: add targets install-devfiles and install-ide-devfiles
pirbo authored
594 .PHONY: install-tools install-library install-library-light install-devfiles
9dc9bd9 Various fixes in the Makefiles
letouzey authored
595 .PHONY: install-coq-info install-coq-manpages install-emacs install-latex
596
21bb352 @pirbo Makefile.build: add targets install-devfiles and install-ide-devfiles
pirbo authored
597 install-coq: install-binaries install-library install-coq-info install-devfiles
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
598 install-coqlight: install-binaries install-library-light
599
492ad5a No more coqtop.opt, produce directly a coqtop binary
letouzey authored
600 install-binaries: install-tools
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
601 $(MKDIR) $(FULLBINDIR)
492ad5a No more coqtop.opt, produce directly a coqtop binary
letouzey authored
602 $(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
603
604 install-tools::
605 $(MKDIR) $(FULLBINDIR)
606 # recopie des fichiers de style pour coqide
607 $(MKDIR) $(FULLCOQLIB)/tools/coqdoc
2f79513 Correction du bug #1715
notin authored
608 touch $(FULLCOQLIB)/tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715)
6aad0d9 Remplacement des 'cp' et 'mkdir' par 'install'
notin authored
609 $(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
610 $(INSTALLBIN) $(TOOLS) $(FULLBINDIR)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
611
61c090d Makefile: force the installation of all .cmi (and remove some obsolete ....
letouzey authored
612 # The list of .cmi to install, including the ones obtained
613 # from .mli without .ml, and the ones obtained from .ml without .mli
614
615 INSTALLCMI = $(sort \
616 $(CONFIG:.cmo=.cmi) \
617 $(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \
618 $(foreach lib,$(CORECMA) $(PLUGINSCMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES)))))
619
21bb352 @pirbo Makefile.build: add targets install-devfiles and install-ide-devfiles
pirbo authored
620 install-devfiles:
621 $(MKDIR) $(FULLBINDIR)
622 $(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR)
623 $(MKDIR) $(FULLCOQLIB)
624 $(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(GRAMMARCMA)
625 $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI)
626 ifeq ($(BEST),opt)
627 $(INSTALLSH) $(FULLCOQLIB) $(LINKCMX) $(CONFIG:.cmo=.o) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a)
628 endif
629
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
630 install-library:
631 $(MKDIR) $(FULLCOQLIB)
9f208c9 @pirbo Bug 2679: Do not try to install cmxs with -byte-only
pirbo authored
632 $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
633 $(MKDIR) $(FULLCOQLIB)/user-contrib
830e2fc Installation des librairies: on utilise maintenant LINKCMO au lieu de
notin authored
634 $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
9cba6da Fix build/install failures when ocamlopt is not available
glondu authored
635 ifeq ($(BEST),opt)
830e2fc Installation des librairies: on utilise maintenant LINKCMO au lieu de
notin authored
636 $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
21bb352 @pirbo Makefile.build: add targets install-devfiles and install-ide-devfiles
pirbo authored
637 $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT)
9cba6da Fix build/install failures when ocamlopt is not available
glondu authored
638 endif
f73034a Do not install csdpcert in $(BINDIR)
glondu authored
639 # csdpcert is not meant to be directly called by the user; we install
640 # it with libraries
0329bbb Makefile made compatible with Solaris 10 (bug #2078, continued - see
herbelin authored
641 -$(MKDIR) $(FULLCOQLIB)/plugins/micromega
7d220f8 Directory 'contrib' renamed into 'plugins', to end confusion with archiv...
letouzey authored
642 $(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/plugins/micromega
5611d73 @pirbo Bug 2377 part 2: old revision file is erased by install
pirbo authored
643 rm -f $(FULLCOQLIB)/revision
25e8fd4 Fix de divers petits problèmes d'installation
notin authored
644 -$(INSTALLLIB) revision $(FULLCOQLIB)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
645
646 install-library-light:
647 $(MKDIR) $(FULLCOQLIB)
9f208c9 @pirbo Bug 2679: Do not try to install cmxs with -byte-only
pirbo authored
648 $(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS)
5611d73 @pirbo Bug 2377 part 2: old revision file is erased by install
pirbo authored
649 rm -f $(FULLCOQLIB)/revision
25e8fd4 Fix de divers petits problèmes d'installation
notin authored
650 -$(INSTALLLIB) revision $(FULLCOQLIB)
9f208c9 @pirbo Bug 2679: Do not try to install cmxs with -byte-only
pirbo authored
651 ifeq ($(BEST),opt)
652 $(INSTALLSH) $(FULLCOQLIB) $(INITPLUGINSOPT)
653 endif
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
654
655 install-coq-info: install-coq-manpages install-emacs install-latex
656
657 install-coq-manpages:
658 $(MKDIR) $(FULLMANDIR)/man1
6aad0d9 Remplacement des 'cp' et 'mkdir' par 'install'
notin authored
659 $(INSTALLLIB) $(MANPAGES) $(FULLMANDIR)/man1
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
660
661 install-emacs:
662 $(MKDIR) $(FULLEMACSLIB)
9303e45 Fix installation of emacs files
glondu authored
663 $(INSTALLLIB) tools/coq-db.el tools/coq-font-lock.el tools/coq-syntax.el tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
664
665 # command to update TeX' kpathsea database
666 #UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null
667
668 install-latex:
669 $(MKDIR) $(FULLCOQDOCDIR)
6aad0d9 Remplacement des 'cp' et 'mkdir' par 'install'
notin authored
670 $(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
671 # -$(UPDATETEX)
672
673 ###########################################################################
674 # Documentation of the source code (using ocamldoc)
675 ###########################################################################
676
8e66761 @pirbo "make source-doc" builds documentation of mli in html and pdf at
pirbo authored
677 .PHONY: source-doc mli-doc ml-doc
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
678
8e66761 @pirbo "make source-doc" builds documentation of mli in html and pdf at
pirbo authored
679 source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf
680
681 $(OCAMLDOCDIR)/coq.tex:: $(DOCMLIS:.mli=.cmi)
f975575 remove -rectypes except for term.ml
letouzey authored
682 $(OCAMLDOC) -latex -I $(MYCAMLP4LIB) $(MLINCLUDES)\
8e66761 @pirbo "make source-doc" builds documentation of mli in html and pdf at
pirbo authored
683 $(DOCMLIS) -t "Coq mlis documentation" \
684 -intro $(OCAMLDOCDIR)/docintro -o $@
685
686 mli-doc:: $(DOCMLIS:.mli=.cmi)
f975575 remove -rectypes except for term.ml
letouzey authored
687 $(OCAMLDOC) -html -I $(MYCAMLP4LIB) $(MLINCLUDES)\
8e66761 @pirbo "make source-doc" builds documentation of mli in html and pdf at
pirbo authored
688 $(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
689 -t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
690 -css-style style.css
691
a9e25d7 @ppedrot Added a ml-dot option to Makefile to generate dependency graph of core m...
ppedrot authored
692 ml-dot:: $(MLEXTRAFILES)
693 $(OCAMLDOC) -dot -dot-reduce -rectypes -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES)\
694 $(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot
695
5a5f774 @pirbo ocamldoc related fixes
pirbo authored
696 %_dep.png: %.dot
8e66761 @pirbo "make source-doc" builds documentation of mli in html and pdf at
pirbo authored
697 $(DOT) -Tpng $< -o $@
698
5a5f774 @pirbo ocamldoc related fixes
pirbo authored
699 %_types.dot: %.mli
f975575 remove -rectypes except for term.ml
letouzey authored
700 $(OCAMLDOC) $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $<
8e66761 @pirbo "make source-doc" builds documentation of mli in html and pdf at
pirbo authored
701
f975575 remove -rectypes except for term.ml
letouzey authored
702 OCAMLDOC_MLLIBD = $(OCAMLDOC) $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
68801aa @pirbo Makefile install rule fix
pirbo authored
703 $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib))))
8e66761 @pirbo "make source-doc" builds documentation of mli in html and pdf at
pirbo authored
704
705 %.dot: | %.mllib.d
706 $(OCAMLDOC_MLLIBD)
707
708 ml-doc:
2a0b8d8 Makefile: cleanup of variables containing lists of files, such as MLFILE...
letouzey authored
709 $(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) $(MLSTATICFILES)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
710
8e66761 @pirbo "make source-doc" builds documentation of mli in html and pdf at
pirbo authored
711 parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d
712 $(OCAMLDOC_MLLIBD)
713
463e464 place all files specific to camlp4 syntax extensions in grammar/
letouzey authored
714 grammar/grammar.dot : | grammar/grammar.mllib.d
3854ae1 Makefile.build: a rule for building grammar.dot
letouzey authored
715 $(OCAMLDOC_MLLIBD)
716
8e66761 @pirbo "make source-doc" builds documentation of mli in html and pdf at
pirbo authored
717 tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d
718 $(OCAMLDOC_MLLIBD)
719
720 %.dot: %.mli
f975575 remove -rectypes except for term.ml
letouzey authored
721 $(OCAMLDOC) $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $<
8e66761 @pirbo "make source-doc" builds documentation of mli in html and pdf at
pirbo authored
722
723 $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
724 (cd $(OCAMLDOCDIR) ; pdflatex $*.tex && pdflatex $*.tex)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
725
726 ###########################################################################
727 ### Special rules
728 ###########################################################################
729
dffb615 Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey authored
730 dev/printers.cma: | dev/printers.mllib.d
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
731 $(SHOW)'Testing $@'
4e0def8 no need for camlp4 cma's in coq misc tools
letouzey authored
732 $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(SYSCMA) $(P4CMA) $^ -o test-printer
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
733 @rm -f test-printer
734 $(SHOW)'OCAMLC -a $@'
791db4d Do not link system library into installed .cma
glondu authored
735 $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
736
463e464 place all files specific to camlp4 syntax extensions in grammar/
letouzey authored
737 grammar/grammar.cma: | grammar/grammar.mllib.d
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
738 $(SHOW)'Testing $@'
739 @touch test.ml4
335a3d9 Win32: some quote fixes
letouzey authored
740 $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp '$(CAMLP4O) -I $(CAMLLIB) $^ -impl' -impl test.ml4 -o test-grammar
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
741 @rm -f test-grammar test.*
742 $(SHOW)'OCAMLC -a $@'
791db4d Do not link system library into installed .cma
glondu authored
743 $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
744
2b636a0 @pirbo MacOS integration
pirbo authored
745 ide/coqide_main.ml: ide/coqide_main.ml4
746 $(SHOW)'CAMLP4O $<'
907c5df Avoid generating ide/coqide_main*.ml as cleartext (except if READABLE_ML...
letouzey authored
747 $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -impl $< -o $@
2b636a0 @pirbo MacOS integration
pirbo authored
748
749 ide/coqide_main_opt.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here
750 $(SHOW)'CAMLP4O $<'
907c5df Avoid generating ide/coqide_main*.ml as cleartext (except if READABLE_ML...
letouzey authored
751 $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -D$(IDEOPTINT) -impl $< -o $@
2b636a0 @pirbo MacOS integration
pirbo authored
752
f975575 remove -rectypes except for term.ml
letouzey authored
753 # Specific rule for term.ml which uses -rectypes
754 # Since term.mli doesn't need -rectypes, this doesn't impact the other ml files
755
756 TERM:=kernel/term
757
758 $(TERM).cmo: $(TERM).ml | $(TERM).ml.d
759 $(SHOW)'OCAMLC -rectypes $<'
760 $(HIDE)$(OCAMLC) $(BYTEFLAGS) -rectypes -c $<
761
762 $(TERM).cmx: $(TERM).ml | $(TERM).ml.d
763 $(SHOW)'OCAMLOPT -rectypes $<'
764 $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -intf-suffix .cmi -rectypes -c $<
2b636a0 @pirbo MacOS integration
pirbo authored
765
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
766 # pretty printing of the revision number when compiling a checked out
767 # source tree
768 .PHONY: revision
769
f930602 Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk
notin authored
770 revision:
6f8b2da Attempt to avoid killing+recreating the file revision with same content.
letouzey authored
771 $(SHOW)'CHECK revision'
772 $(HIDE)rm -f revision.new
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
773 ifeq ($(CHECKEDOUT),svn)
98231b9 Fix last commit about revision: I'm unsure about the role of "set -e",
letouzey authored
774 $(HIDE)set -e; \
6f8b2da Attempt to avoid killing+recreating the file revision with same content.
letouzey authored
775 if test -x "`which svn`"; then \
4862093 Calcul plus robuste du numéro de révision (ne marche en positionnant
herbelin authored
776 export LC_ALL=C;\
f930602 Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk
notin authored
777 svn info . | sed -ne '/URL/s/.*\/\([^\/]\{1,\}\)/\1/p' > revision.new; \
778 svn info . | sed -ne '/Revision/s/Revision: \([0-9]\{1,\}\)/\1/p'>> revision.new; \
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
779 fi
780 endif
781 ifeq ($(CHECKEDOUT),gnuarch)
98231b9 Fix last commit about revision: I'm unsure about the role of "set -e",
letouzey authored
782 $(HIDE)set -e; \
6f8b2da Attempt to avoid killing+recreating the file revision with same content.
letouzey authored
783 if test -x "`which tla`"; then \
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
784 LANG=C; export LANG; \
f930602 Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk
notin authored
785 tla tree-version > revision.new ; \
786 tla tree-revision | sed -ne 's|.*--||p' >> revision.new ; \
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
787 fi
788 endif
789 ifeq ($(CHECKEDOUT),git)
12e9483 Fix build for git users
glondu authored
790 $(HIDE)set -e; \
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
791 if test -x "`which git`"; then \
792 LANG=C; export LANG; \
f930602 Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk
notin authored
793 GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \
8e66761 @pirbo "make source-doc" builds documentation of mli in html and pdf at
pirbo authored
794 GIT_HOST=$$(hostname); \
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
795 GIT_PATH=$$(pwd); \
f930602 Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk
notin authored
796 (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \
797 (echo "$$(git log -1 --pretty='format:%H')") >> revision.new; \
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
798 fi
799 endif
98231b9 Fix last commit about revision: I'm unsure about the role of "set -e",
letouzey authored
800 $(HIDE)set -e; \
f930602 Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk
notin authored
801 if test -e revision.new; then \
802 if test -e revision; then \
803 if test "`cat revision`" = "`cat revision.new`" ; then \
804 rm -f revision.new; \
805 else \
806 mv -f revision.new revision; \
807 fi; \
808 else \
809 mv -f revision.new revision; \
810 fi \
db6363f - Fixed the recompilation of config/revision.ml once every two conmpilat...
herbelin authored
811 fi
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
812
813 ###########################################################################
814 # Default rules
815 ###########################################################################
816
139bf11 Makefile: factorization of default rules for .cmi/.cmo/.cmx
letouzey authored
817 ## Three flavor of flags: checker/* ide/* and normal files
dc25e1b added coqchk to the main Makefile and a make variable VALIDATE to check ...
barras authored
818
139bf11 Makefile: factorization of default rules for .cmi/.cmo/.cmx
letouzey authored
819 COND_BYTEFLAGS= \
820 $(if $(filter checker/%,$<), $(CHKBYTEFLAGS), \
821 $(if $(filter ide/%,$<),$(COQIDEFLAGS),) $(BYTEFLAGS))
dc25e1b added coqchk to the main Makefile and a make variable VALIDATE to check ...
barras authored
822
139bf11 Makefile: factorization of default rules for .cmi/.cmo/.cmx
letouzey authored
823 COND_OPTFLAGS= \
824 $(if $(filter checker/%,$<), $(CHKOPTFLAGS), \
825 $(if $(filter ide/%,$<),$(COQIDEFLAGS),) $(OPTFLAGS))
dc25e1b added coqchk to the main Makefile and a make variable VALIDATE to check ...
barras authored
826
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
827 %.o: %.c
9ef3acb Rely on ocamlc to call the C compiler...
glondu authored
828 $(SHOW)'OCAMLC $<'
829 $(HIDE)cd $(dir $<) && $(OCAMLC) -ccopt "$(CFLAGS)" -c $(notdir $<)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
830
139bf11 Makefile: factorization of default rules for .cmi/.cmo/.cmx
letouzey authored
831 %.cmi: %.mli | %.mli.d
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
832 $(SHOW)'OCAMLC $<'
139bf11 Makefile: factorization of default rules for .cmi/.cmo/.cmx
letouzey authored
833 $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $<
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
834
139bf11 Makefile: factorization of default rules for .cmi/.cmo/.cmx
letouzey authored
835 %.cmo: %.ml | %.ml.d
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
836 $(SHOW)'OCAMLC $<'
139bf11 Makefile: factorization of default rules for .cmi/.cmo/.cmx
letouzey authored
837 $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $<
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
838
252aa14 Makefile: try to avoid rare make failures related with make -j + ocamlop...
letouzey authored
839 ## NB: for the moment ocamlopt erases and recreates .cmi if there's no .mli around.
840 ## This can lead to nasty things with make -j. To avoid that:
841 ## 1) We make .cmx always depend on .cmi
842 ## 2) This .cmi will be created from the .mli, or trigger the compilation of the
843 ## .cmo if there's no .mli (see rule below about MLWITHOUTMLI)
0bdb694 Makefile: a nicer hack concerning ocamlopt with no .mli: -intf-suffix .c...
letouzey authored
844 ## 3) We tell ocamlopt to use the .cmi as the interface source file. With this
845 ## hack, everything goes as if there is a .mli, and the .cmi is preserved
846 ## and the .cmx is checked with respect to this .cmi
252aa14 Makefile: try to avoid rare make failures related with make -j + ocamlop...
letouzey authored
847
0bdb694 Makefile: a nicer hack concerning ocamlopt with no .mli: -intf-suffix .c...
letouzey authored
848 HACKMLI = $(if $(wildcard $<i),,-intf-suffix .cmi)
849
bf7cfcf Makefile: avoid too much exported vars (for win32)
letouzey authored
850 define diff
851 $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f)))
852 endef
853
854 MLWITHOUTMLI := $(call diff, $(MLFILES), $(MLIFILES:.mli=.ml))
855
0bdb694 Makefile: a nicer hack concerning ocamlopt with no .mli: -intf-suffix .c...
letouzey authored
856 $(MLWITHOUTMLI:.ml=.cmx): %.cmx: %.cmi # for .ml with .mli this is already the case
252aa14 Makefile: try to avoid rare make failures related with make -j + ocamlop...
letouzey authored
857
858 $(MLWITHOUTMLI:.ml=.cmi): %.cmi: %.cmo
859
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
860 %.cmx: %.ml | %.ml.d
861 $(SHOW)'OCAMLOPT $<'
0bdb694 Makefile: a nicer hack concerning ocamlopt with no .mli: -intf-suffix .c...
letouzey authored
862 $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $<
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
863
59b4a43 Add implicit rules for native plugins (.cmxs)
glondu authored
864 %.cmxs: %.cmxa
47ac37a fixed groebner as a plugin + pattern matching Timeout
barras authored
865 $(SHOW)'OCAMLOPT -shared -o $@'
301d6bf ocamlbuild: many improvements (macos 10.5 fix, correct dllpath, etc)
letouzey authored
866 ifeq ($(HASNATDYNLINK),os5fixme)
cd048fa Complementary fix to have ocamlopt_shared_os5fix.sh working correctly
herbelin authored
867 $(HIDE)dev/ocamlopt_shared_os5fix.sh "$(OCAMLOPT)" $@
8c06744 Workaround to compile the coq archive with dynamic loading on Mac OS 10....
herbelin authored
868 else
301d6bf ocamlbuild: many improvements (macos 10.5 fix, correct dllpath, etc)
letouzey authored
869 $(HIDE)$(OCAMLOPT) -linkall -shared -o $@ $<
8c06744 Workaround to compile the coq archive with dynamic loading on Mac OS 10....
herbelin authored
870 endif
59b4a43 Add implicit rules for native plugins (.cmxs)
glondu authored
871
872 %.cmxs: %.cmx
47ac37a fixed groebner as a plugin + pattern matching Timeout
barras authored
873 $(SHOW)'OCAMLOPT -shared -o $@'
59b4a43 Add implicit rules for native plugins (.cmxs)
glondu authored
874 $(HIDE)$(OCAMLOPT) -shared -o $@ $<
875
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
876 %.ml: %.mll
877 $(SHOW)'OCAMLLEX $<'
cc1eab7 Ajout de cibles pour le manuel de référence (refman-nodep, stdlib-nodep,...
notin authored
878 $(HIDE)$(OCAMLLEX) -o $@ "$*.mll"
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
879
880 %.ml %.mli: %.mly
881 $(SHOW)'OCAMLYACC $<'
882 $(HIDE)$(OCAMLYACC) $<
883
dffb615 Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey authored
884 plugins/%_mod.ml: plugins/%.mllib
885 $(SHOW)'ECHO... > $@'
886 $(HIDE)sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@
887 $(HIDE)echo "let _=Mltop.add_known_module\"$(notdir $*)\"" >> $@
888
25533df Finish adding out-of-the-box support for camlp4
letouzey authored
889 # NB: compatibility modules for camlp4:
890 # - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded
891 # - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with
892 # syntax such that VERNAC EXTEND, we only load it for a few files via camlp4deps
893
894 %.ml: %.ml4 | %.ml4.d tools/compat5.cmo tools/compat5b.cmo
ded46fc Implement KEEP_ML4_PREPROCESSED option in build system
lmamane authored
895 $(SHOW)'CAMLP4O $<'
6b010da Makefile: some more cleanup
letouzey authored
896 $(HIDE)\
cf6b384 @pirbo make otags only relies on otags
pirbo authored
897 DEPS="$(call CAMLP4DEPS,$<)"; \
6b010da Makefile: some more cleanup
letouzey authored
898 if ls $${DEPS} > /dev/null 2>&1; then \
25533df Finish adding out-of-the-box support for camlp4
letouzey authored
899 $(CAMLP4O) $(PR_O) -I $(CAMLLIB) tools/compat5.cmo $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@; \
6b010da Makefile: some more cleanup
letouzey authored
900 else echo $< : Dependency $${DEPS} not ready yet; false; fi
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
901
ac98362 Remove broken makefile option NO_RECOMPILE_LIB
letouzey authored
902 %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
903 $(SHOW)'COQC $<'
904 $(HIDE)rm -f $*.glob
637e67a Makefile.build: states/initial.coq was wrongly done with -dont-load-proo...
letouzey authored
905 $(HIDE)$(BOOTCOQC) $*
dc25e1b added coqchk to the main Makefile and a make variable VALIDATE to check ...
barras authored
906 ifdef VALIDATE
3e314a8 added Makefile target: validate (to recheck all .vo in a row)
barras authored
907 $(SHOW)'COQCHK $(call vo_to_mod,$@)'
492ad5a No more coqtop.opt, produce directly a coqtop binary
letouzey authored
908 $(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \
dc25e1b added coqchk to the main Makefile and a make variable VALIDATE to check ...
barras authored
909 || ( RV=$$?; rm -f "$@"; exit $${RV} )
910 endif
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
911
912 ###########################################################################
913 # Dependencies
914 ###########################################################################
915
916 # .ml4.d contains the dependencies to generate the .ml from the .ml4
917 # NOT to generate object code.
6b010da Makefile: some more cleanup
letouzey authored
918
919 %.ml4.d: $(D_DEPEND_BEFORE_SRC) %.ml4
920 $(SHOW)'CAMLP4DEPS $<'
cf6b384 @pirbo make otags only relies on otags
pirbo authored
921 $(HIDE)echo "$*.ml: $(if $(NO_RECOMPILE_ML4),$(ORDER_ONLY_SEP)) $(call CAMLP4DEPS,$<)" $(TOTARGET)
58a5a53 Makefile: the .ml of .ml4 are now produced explicitely (in binary ast fo...
letouzey authored
922
923 # We now use coqdep_boot to wrap around ocamldep -modules, since it is aware
924 # of .ml4 files
925
926 OCAMLDEP_NG = $(COQDEPBOOT) -mldep $(OCAMLDEP)
927
928 checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
dc25e1b added coqchk to the main Makefile and a make variable VALIDATE to check ...
barras authored
929 $(SHOW)'OCAMLDEP $<'
58a5a53 Makefile: the .ml of .ml4 are now produced explicitely (in binary ast fo...
letouzey authored
930 $(HIDE)$(OCAMLDEP_NG) -slash $(LOCALCHKLIBS) "$<" $(TOTARGET)
dc25e1b added coqchk to the main Makefile and a make variable VALIDATE to check ...
barras authored
931
58a5a53 Makefile: the .ml of .ml4 are now produced explicitely (in binary ast fo...
letouzey authored
932 checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
dc25e1b added coqchk to the main Makefile and a make variable VALIDATE to check ...
barras authored
933 $(SHOW)'OCAMLDEP $<'
58a5a53 Makefile: the .ml of .ml4 are now produced explicitely (in binary ast fo...
letouzey authored
934 $(HIDE)$(OCAMLDEP_NG) -slash $(LOCALCHKLIBS) "$<" $(TOTARGET)
dc25e1b added coqchk to the main Makefile and a make variable VALIDATE to check ...
barras authored
935
58a5a53 Makefile: the .ml of .ml4 are now produced explicitely (in binary ast fo...
letouzey authored
936 %.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
96876c7 fixed dependency problems with the checker
barras authored
937 $(SHOW)'OCAMLDEP $<'
58a5a53 Makefile: the .ml of .ml4 are now produced explicitely (in binary ast fo...
letouzey authored
938 $(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET)
96876c7 fixed dependency problems with the checker
barras authored
939
58a5a53 Makefile: the .ml of .ml4 are now produced explicitely (in binary ast fo...
letouzey authored
940 %.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
96876c7 fixed dependency problems with the checker
barras authored
941 $(SHOW)'OCAMLDEP $<'
58a5a53 Makefile: the .ml of .ml4 are now produced explicitely (in binary ast fo...
letouzey authored
942 $(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET)
96876c7 fixed dependency problems with the checker
barras authored
943
58a5a53 Makefile: the .ml of .ml4 are now produced explicitely (in binary ast fo...
letouzey authored
944 checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
dffb615 Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey authored
945 $(SHOW)'COQDEP $<'
58a5a53 Makefile: the .ml of .ml4 are now produced explicitely (in binary ast fo...
letouzey authored
946 $(HIDE)$(COQDEPBOOT) -slash -I checker -c "$<" $(TOTARGET)
dffb615 Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey authored
947
58a5a53 Makefile: the .ml of .ml4 are now produced explicitely (in binary ast fo...
letouzey authored
948 %.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
eb93dfa Makefile: ml dependencies of contribs are moved to .mllib files
letouzey authored
949 $(SHOW)'COQDEP $<'
58a5a53 Makefile: the .ml of .ml4 are now produced explicitely (in binary ast fo...
letouzey authored
950 $(HIDE)$(COQDEPBOOT) -slash -I kernel -I tools/coqdoc -c "$<" $(TOTARGET)
481bc97 Makefile: more robustness all around
lmamane authored
951
d63dee2 coqdep_boot: a specialized and dependency-free coqdep for killing one of...
letouzey authored
952 %.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
953 $(SHOW)'COQDEP $<'
58a5a53 Makefile: the .ml of .ml4 are now produced explicitely (in binary ast fo...
letouzey authored
954 $(HIDE)$(COQDEPBOOT) $(DEPNATDYN) -slash "$<" $(TOTARGET)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
955
8de2295 @pirbo no more errors at _stubs.c.d generation
pirbo authored
956 %_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC)
957 $(SHOW)'CCDEP $<'
958 $(HIDE)echo "$@ $(@:.c.d=.o): $(@:.c.d=.c)" > $@
959
ca4775a Implement NO_RECALC_DEPS option in build system
lmamane authored
960 %.c.d: $(D_DEPEND_BEFORE_SRC) %.c $(D_DEPEND_AFTER_SRC) $(GENHFILES)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
961 $(SHOW)'CCDEP $<'
66267d4 Simpler configure: gcc via ocamlc, no ranlib (done by ocamlmklib)
letouzey authored
962 $(HIDE)$(OCAMLC) -ccopt "-MM -MQ $@ -MQ $(<:.c=.o) -isystem $(CAMLHLIB)" $< $(TOTARGET)
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
963
964 ###########################################################################
965 # this sets up developper supporting stuff
966 ###########################################################################
967
cf6b384 @pirbo make otags only relies on otags
pirbo authored
968 .PHONY: devel otags
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
969 devel: $(DEBUGPRINTERS)
970
cf6b384 @pirbo make otags only relies on otags
pirbo authored
971 otags:
972 otags $(MLIFILES) $(MLSTATICFILES) \
973 $(foreach i,$(ML4FILES),-pc -pa tools/compat5.cmo -pa op -pa g -pa m -pa rq $(patsubst %,-pa %,$(call CAMLP4DEPS,$i)) -impl $i)
974
975
8f4b7f1 New bootstrapping, improved, Makefile system
corbinea authored
976 ###########################################################################
c5f77c4 A emacs-specific comment to use makefile-mode on Makefile.*
letouzey authored
977
d581efa Amélioration de la génération des graphes de dépendances
notin authored
978
c5f77c4 A emacs-specific comment to use makefile-mode on Makefile.*
letouzey authored
979 # For emacs:
980 # Local Variables:
981 # mode: makefile
982 # End:
Something went wrong with that request. Please try again.