diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-05-31 23:20:21 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-01 00:53:09 +0200 |
| commit | 1532e4d57fce07e8a1cd6838853a4a31ea84e453 (patch) | |
| tree | a1c3e1f1ca8b5924f60e3756a1f81a6ae8764c7e /Makefile.build | |
| parent | b3485ddc8c4f98743426bb58c8d49b76edd43d61 (diff) | |
Makefile: restore the use of coqdep_boot for creating .v.d files
Coqdep_boot has almost no dependencies, and hence can be compiled
very early during the build, without relying on .ml.d files.
Some code of system.ml is now in a separate file minisys.ml,
which is also included in system.ml for compatibility.
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build index 190a62d00..dbf60afb7 100644 --- a/Makefile.build +++ b/Makefile.build @@ -611,6 +611,16 @@ tools: $(TOOLS) $(DEBUGPRINTERS) $(OCAMLLIBDEP) # to avoid using implicit rules and hence .ml.d files that would need # coqdep_boot. +COQDEPBOOTSRC := \ + lib/minisys.ml \ + tools/coqdep_lexer.mli tools/coqdep_lexer.ml \ + tools/coqdep_common.mli tools/coqdep_common.ml \ + tools/coqdep_boot.ml + +$(COQDEPBOOT): $(COQDEPBOOTSRC) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml, -I tools, unix) + OCAMLLIBDEPSRC:= tools/ocamllibdep.ml $(OCAMLLIBDEP): $(OCAMLLIBDEPSRC) @@ -1093,9 +1103,9 @@ dev/%.mllib.d: $(D_DEPEND_BEFORE_SRC) dev/%.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLL $(SHOW)'OCAMLLIBDEP $<' $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET) -%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEP) $(GENVFILES) +%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) -boot $(DEPNATDYN) "$<" $(TOTARGET) + $(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET) %_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC) $(SHOW)'CCDEP $<' |