diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-22 10:13:03 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-22 10:46:33 +0200 |
| commit | 28c118aa3a82c03a18a31b802674e1f56b693796 (patch) | |
| tree | 65934b7ba110e177d62d2105eeec1fbfb17820d7 /Makefile.build | |
| parent | 39861a12445742b481496baf2caafeb391773aba (diff) | |
Makefile.build: "make;make" should redo nothing
As reported by PMP, this was not yet the case. The culprit
was the build of coqdep_boot by a one-liner ocamlopt taking all
the necessary .ml files as arguments (in the right order). This
was nice and short, and correct wrt dependencies, but had the
inconvenient of building some .cmi *after* their corresponding
.cmx, while the rest of the Makefile relies on the reverse order
(see the section about MLWITHOUTMLI). Hence on the next run,
make was thinking that these .cmx weren't up-to-date.
For solving this issue, we now build coqdep_boot (and other tools)
via a list of .cmx and let our infractructure build them (after
their .cmi). The only drawback is the 6 extra lines to hardcode
the dependencies of the *.cm(o|i|x) needed for coqdep_boot.
(since the .ml.d aren't already taken in account by make at that
time).
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 27 |
1 files changed, 14 insertions, 13 deletions
diff --git a/Makefile.build b/Makefile.build index 3a24d8dbc..b225140bd 100644 --- a/Makefile.build +++ b/Makefile.build @@ -364,24 +364,25 @@ $(COQC): $(call bestobj, $(COQCCMO)) tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT) # coqdep_boot : a basic version of coqdep, with almost no dependencies. +# We state these dependencies here explicitly, since some .ml.d files +# may still be missing or not taken in account yet by make when coqdep_boot +# is being built. -# Here it is important to mention .ml files instead of .cmo in order -# to avoid using implicit rules : at the time coqdep_boot is being built, -# some .ml.d files may still be missing or not taken in account yet by make. +COQDEPBOOTSRC := lib/minisys.cmo \ + tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep_boot.cmo -COQDEPBOOTSRC := \ - lib/minisys.ml \ - tools/coqdep_lexer.mli tools/coqdep_lexer.ml \ - tools/coqdep_common.mli tools/coqdep_common.ml \ - tools/coqdep_boot.ml +tools/coqdep_lexer.cmo : tools/coqdep_lexer.cmi +tools/coqdep_lexer.cmx : tools/coqdep_lexer.cmi +tools/coqdep_common.cmo : lib/minisys.cmo tools/coqdep_lexer.cmi tools/coqdep_common.cmi +tools/coqdep_common.cmx : lib/minisys.cmx tools/coqdep_lexer.cmx tools/coqdep_common.cmi +tools/coqdep_boot.cmo : tools/coqdep_common.cmi +tools/coqdep_boot.cmx : tools/coqdep_common.cmx -$(COQDEPBOOT): $(COQDEPBOOTSRC) +$(COQDEPBOOT): $(call bestobj, $(COQDEPBOOTSRC)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -I tools, unix) -# Same for ocamllibdep - -$(OCAMLLIBDEP): tools/ocamllibdep.ml +$(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -I tools, unix) @@ -436,7 +437,7 @@ $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN)) # votour: a small vo explorer (based on the checker) -bin/votour: $(call bestobj, lib/cObj.cmo checker/analyze.cmo checker/values.cmo) checker/votour.ml +bin/votour: $(call bestobj, lib/cObj.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -I checker,) |