diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-02-27 18:03:49 +0100 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-02-27 18:48:23 +0100 |
commit | e372b7244bcb8cc449196c29a7dabee6f7f84aa2 (patch) | |
tree | d249777e9bdc9ba03aaf1f4455f1a1aee3e8c274 /Makefile | |
parent | ca64cc032a3f03381d00d7c9b128688f3f920844 (diff) |
Makefile: re-introduce 2 phases to avoid make strange -include's
Yet another revision of the build system. We avoid relying on the awkward
include-which-fails-but-works-finally-after-a-retry feature of gnu make.
This was working, but was quite hard to understand. Instead, we reuse
the idea of two explicit phases (as in 2007 and its stage{1,2,3}), but
in a lighter way. The main Makefile calls Makefile.build twice :
- first for building grammar.cma (and q_constr.cmo), with a restricted
set of .ml4 to consider (see variables BUILDGRAMMAR and ML4BASEFILES).
- then on the true target(s) asked by the user (using the special variable
MAKECMDGOALS).
In pratice, this should change very little to the concrete developper's life,
let me know otherwise. A few more messages of make due to the explicit
first sub-call, but no more strange "not ready yet" messages...
Btw: we should handle correctly now the parallel compilation of multiple
targets (e.g. make -jX foo bar). As reported by Pierre B, this was
triggering earlier two separate sub-calls to Makefile.build, one
for foo, the other for bar, with possibly nasty interactions in case
of parallelism.
In addition, some cleanup of Makefile.build, removal of useless :: rules,
etc etc.
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 46 |
1 files changed, 32 insertions, 14 deletions
@@ -59,11 +59,20 @@ define find $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -print | sed 's|^\./||') endef +define findx + $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -exec $(2) {} \; | sed 's|^\./||') +endef + +# We now discriminate .ml4 files according to their need of grammar.cma +# or q_constr.cmo +USEGRAMMAR := '(\*.*camlp4deps.*grammar' + ## Files in the source tree YACCFILES:=$(call find, '*.mly') LEXFILES := $(call find, '*.mll') export MLLIBFILES := $(call find, '*.mllib') +export ML4BASEFILES := $(call findx, '*.ml4', grep -L -e $(USEGRAMMAR)) export ML4FILES := $(call find, '*.ml4') export CFILES := $(call find, '*.c') @@ -77,13 +86,13 @@ EXISTINGMLI := $(call find, '*.mli') ## Files that will be generated GENML4FILES:= $(ML4FILES:.ml4=.ml) -GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \ - tools/tolink.ml kernel/copcodes.ml GENMLIFILES:=$(YACCFILES:.mly=.mli) GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml)) +export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \ + tools/tolink.ml kernel/copcodes.ml $(GENPLUGINSMOD) export GENHFILES:=kernel/byterun/coq_jumptbl.h export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v -export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) $(GENPLUGINSMOD) +export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) # NB: all files in $(GENFILES) can be created initially, while # .ml files in $(GENML4FILES) might need some intermediate building. @@ -95,8 +104,7 @@ define diff $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f))) endef -export MLEXTRAFILES := $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD) -export MLSTATICFILES := $(call diff, $(EXISTINGML), $(MLEXTRAFILES)) +export MLSTATICFILES := $(call diff, $(EXISTINGML), $(GENMLFILES) $(GENML4FILES)) export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) include Makefile.common @@ -107,7 +115,7 @@ include Makefile.common NOARG: world -.PHONY: NOARG help always +.PHONY: NOARG help noconfig submake help: @echo "Please use either" @@ -131,17 +139,27 @@ endif # Apart from clean and tags, everything will be done in a sub-call to make # on Makefile.build. This way, we avoid doing here the -include of .d : -# since they trigger some compilations, we do not want them for a mere clean +# since they trigger some compilations, we do not want them for a mere clean. +# Moreover, we regroup this sub-call in a common target named 'submake'. +# This way, multiple user-given goals (cf the MAKECMDGOALS variable) won't +# trigger multiple (possibly parallel) make sub-calls ifdef COQ_CONFIGURED -%:: always - $(MAKE) --warn-undefined-variable --no-builtin-rules -f Makefile.build "$@" +%:: submake ; else -%:: always - @echo "Please run ./configure first" >&2; exit 1 +%:: noconfig ; endif -always : ; +MAKE_OPTS := --warn-undefined-variable --no-builtin-rules + +GRAM_TARGETS := grammar/grammar.cma grammar/q_constr.cmo + +submake: + $(MAKE) $(MAKE_OPTS) -f Makefile.build BUILDGRAMMAR=1 $(GRAM_TARGETS) + $(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS) + +noconfig: + @echo "Please run ./configure first" >&2; exit 1 # To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles @@ -165,7 +183,7 @@ cruftclean: ml4clean indepclean: rm -f $(GENFILES) - rm -f $(COQTOPBYTE) $(CHICKENBYTE) bin/fake_ide + rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(FAKEIDE) find . \( -name '*~' -o -name '*.cm[ioat]' -o -name '*.cmti' \) -delete rm -f */*.pp[iox] plugins/*/*.pp[iox] rm -rf $(SOURCEDOCDIR) @@ -234,7 +252,7 @@ devdocclean: # Emacs tags ########################################################################### -.PHONY: tags +.PHONY: tags printenv tags: echo $(MLIFILES) $(MLSTATICFILES) $(ML4FILES) | sort -r | xargs \ |