diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 36 |
1 files changed, 17 insertions, 19 deletions
diff --git a/Makefile.build b/Makefile.build index 41220792d5..a790b92b2e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -501,12 +501,13 @@ test-suite: world $(ALLSTDLIB).v ################################################################## .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping -.PHONY: highparsing stm toplevel hightactics +.PHONY: engine highparsing stm toplevel hightactics lib: lib/clib.cma lib/lib.cma kernel: kernel/kernel.cma byterun: $(BYTERUN) library: library/library.cma +engine: engine/engine.cma proofs: proofs/proofs.cma tactics: tactics/tactics.cma interp: interp/interp.cma @@ -597,7 +598,7 @@ theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_g printers: $(DEBUGPRINTERS) -tools: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT) +tools: $(TOOLS) $(DEBUGPRINTERS) $(OCAMLLIBDEP) # coqdep_boot : a basic version of coqdep, with almost no dependencies. @@ -605,12 +606,9 @@ tools: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT) # to avoid using implicit rules and hence .ml.d files that would need # coqdep_boot. -COQDEPBOOTSRC:= \ - tools/coqdep_lexer.mli tools/coqdep_lexer.ml \ - tools/coqdep_common.mli tools/coqdep_common.ml \ - tools/coqdep_boot.ml +OCAMLLIBDEPSRC:= tools/ocamllibdep.ml -$(COQDEPBOOT): $(COQDEPBOOTSRC) +$(OCAMLLIBDEP): $(OCAMLLIBDEPSRC) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -I tools, unix) @@ -1058,33 +1056,33 @@ endif OCAMLDEP_NG = $(OCAMLDEP) -slash -ml-synonym .ml4 -checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) +checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' $(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET) -checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) +checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' $(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET) -%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) +%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' $(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET) -%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) +%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' $(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET) -checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -I checker -c "$<" $(TOTARGET) +checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) $(LOCALCHKLIBS) "$<" $(TOTARGET) -%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -I kernel -I tools/coqdoc -c "$<" $(TOTARGET) +%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET) -%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES) +%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEP) $(GENVFILES) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) $(DEPNATDYN) "$<" $(TOTARGET) + $(HIDE)$(COQDEP) -boot $(DEPNATDYN) "$<" $(TOTARGET) %_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC) $(SHOW)'CCDEP $<' |