diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 148 |
1 files changed, 77 insertions, 71 deletions
diff --git a/Makefile.build b/Makefile.build index a9dbc4b44..f0dd46b0f 100644 --- a/Makefile.build +++ b/Makefile.build @@ -147,8 +147,14 @@ endif # For creating the missing .d, make will recursively build things like # coqdep_boot (for the .v.d files) or grammar.cma (for .ml4 -> .ml -> .ml.d). +VDFILE := .vfiles +MLDFILE := .mlfiles +PLUGMLDFILE := plugins/.mlfiles +MLLIBDFILE := .mllibfiles +PLUGMLLIBDFILE := plugins/.mllibfiles + DEPENDENCIES := \ - $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(MLPACKFILES) $(CFILES) $(VFILES)) + $(addsuffix .d, $(MLDFILE) $(MLLIBDFILE) $(PLUGMLDFILE) $(PLUGMLLIBDFILE) $(CFILES) $(VDFILE)) -include $(DEPENDENCIES) @@ -189,7 +195,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) COQOPTS=$(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile -LOCALINCLUDES=$(if $(filter plugins/%,$<),-I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS))) +LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS)) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) @@ -197,7 +203,7 @@ OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(FLAMBDA_FLAGS) -DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$<),, -I ide -I ide/utils) +DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$@),, -I ide -I ide/utils) # On MacOS, the binaries are signed, except our private ones ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin) @@ -301,7 +307,7 @@ kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h -e '/^}/q' $< $(TOTARGET) kernel/copcodes.ml: kernel/byterun/coq_instruct.h - sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' $< | \ + tr -d "\r" < $< | sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' | \ awk -f kernel/make-opcodes $(TOTARGET) %.o: %.c @@ -411,7 +417,7 @@ $(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP) # coqc -COQCCMO:=lib/clib.cma lib/cErrors.cmo toplevel/usage.cmo tools/coqc.cmo +COQCCMO:=clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo $(COQC): $(call bestobj, $(COQCCMO)) $(SHOW)'OCAMLBEST -o $@' @@ -432,21 +438,21 @@ tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT) # Remember to update the dependencies below when you add files! COQDEPBOOTSRC := \ - lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo lib/minisys.cmo \ + clib/segmenttree.cmo clib/unicodetable.cmo clib/unicode.cmo clib/minisys.cmo \ tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep_boot.cmo -lib/segmenttree.cmo : lib/segmenttree.cmi -lib/segmenttree.cmx : lib/segmenttree.cmi -lib/unicodetable.cmo : lib/segmenttree.cmo -lib/unicodetable.cmx : lib/segmenttree.cmx -lib/unicode.cmo : lib/unicodetable.cmo lib/unicode.cmi -lib/unicode.cmx : lib/unicodetable.cmx lib/unicode.cmi -lib/minisys.cmo : lib/unicode.cmo -lib/minisys.cmx : lib/unicode.cmx -tools/coqdep_lexer.cmo : lib/unicode.cmi tools/coqdep_lexer.cmi -tools/coqdep_lexer.cmx : lib/unicode.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 +clib/segmenttree.cmo : clib/segmenttree.cmi +clib/segmenttree.cmx : clib/segmenttree.cmi +clib/unicodetable.cmo : clib/segmenttree.cmo +clib/unicodetable.cmx : clib/segmenttree.cmx +clib/unicode.cmo : clib/unicodetable.cmo clib/unicode.cmi +clib/unicode.cmx : clib/unicodetable.cmx clib/unicode.cmi +clib/minisys.cmo : clib/unicode.cmo +clib/minisys.cmx : clib/unicode.cmx +tools/coqdep_lexer.cmo : clib/unicode.cmi tools/coqdep_lexer.cmi +tools/coqdep_lexer.cmx : clib/unicode.cmx tools/coqdep_lexer.cmi +tools/coqdep_common.cmo : clib/minisys.cmo tools/coqdep_lexer.cmi tools/coqdep_common.cmi +tools/coqdep_common.cmx : clib/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 @@ -460,10 +466,8 @@ $(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo) # The full coqdep (unused by this build, but distributed by make install) -COQDEPCMO:=lib/clib.cma lib/cErrors.cmo lib/cWarnings.cmo \ - lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo lib/minisys.cmo \ - lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo \ - tools/coqdep.cmo +COQDEPCMO:=clib/clib.cma lib/lib.cma tools/coqdep_lexer.cmo \ + tools/coqdep_common.cmo tools/coqdep.cmo $(COQDEP): $(call bestobj, $(COQDEPCMO)) $(SHOW)'OCAMLBEST -o $@' @@ -473,7 +477,7 @@ $(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,) -COQMAKEFILECMO:=lib/clib.cma tools/coq_makefile.cmo +COQMAKEFILECMO:=clib/clib.cma lib/lib.cma tools/coq_makefile.cmo $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO)) $(SHOW)'OCAMLBEST -o $@' @@ -487,23 +491,24 @@ $(COQWC): $(call bestobj, tools/coqwc.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -package str) -COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \ +COQDOCCMO:=clib/clib.cma lib/lib.cma $(addprefix tools/coqdoc/, \ cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo ) $(COQDOC): $(call bestobj, $(COQDOCCMO)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -package str,unix) -$(COQWORKMGR): $(call bestobj, lib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo) +$(COQWORKMGR): $(call bestobj, clib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, $(SYSMOD)) # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave -FAKEIDECMO:= lib/clib.cma lib/cErrors.cmo lib/spawn.cmo ide/document.cmo \ - ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo ide/xml_printer.cmo \ - ide/richpp.cmo ide/xmlprotocol.cmo tools/fake_ide.cmo +FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/document.cmo \ + ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo \ + ide/xml_printer.cmo ide/richpp.cmo ide/xmlprotocol.cmo \ + tools/fake_ide.cmo $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN)) $(SHOW)'OCAMLBEST -o $@' @@ -511,7 +516,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.cmo) +bin/votour: $(call bestobj, clib/cObj.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -I checker) @@ -519,7 +524,7 @@ bin/votour: $(call bestobj, lib/cObj.cmo checker/analyze.cmo checker/values.cmo # Csdp to micromega special targets ########################################################################### -CSDPCERTCMO:=lib/clib.cma $(addprefix plugins/micromega/, \ +CSDPCERTCMO:=clib/clib.cma $(addprefix plugins/micromega/, \ mutils.cmo micromega.cmo \ sos_types.cmo sos_lib.cmo sos.cmo csdpcert.cmo ) @@ -571,12 +576,6 @@ kernel/kernel.cma: kernel/kernel.mllib $(SHOW)'OCAMLC -a -o $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(VMBYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^) -# Specific rule for API/API.cmi -# Make sure that API/API.mli cannot leak types from the Coq codebase. -API/API.cmi : API/API.mli - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) -I lib -I $(MYCAMLP4LIB) -c $< - %.cma: %.mllib $(SHOW)'OCAMLC -a -o $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^) @@ -604,10 +603,26 @@ COND_BYTEFLAGS= \ COND_OPTFLAGS= \ $(COND_IDEFLAGS) $(MLINCLUDES) $(OPTFLAGS) +plugins/micromega/%.cmi: plugins/micromega/%.mli + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< + +plugins/nsatz/%.cmi: plugins/nsatz/%.mli + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< + %.cmi: %.mli $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< +plugins/micromega/%.cmo: plugins/micromega/%.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< + +plugins/nsatz/%.cmo: plugins/nsatz/%.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< + %.cmo: %.ml $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< @@ -641,6 +656,14 @@ plugins/micromega/sos_FORPACK:= plugins/micromega/sos_print_FORPACK:= plugins/micromega/csdpcert_FORPACK:= +plugins/micromega/%.cmx: plugins/micromega/%.ml + $(SHOW)'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix,num -c $< + +plugins/nsatz/%.cmx: plugins/nsatz/%.ml + $(SHOW)'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix,num -c $< + plugins/%.cmx: plugins/%.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $< @@ -674,21 +697,24 @@ plugins/%.cmx: plugins/%.ml # Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12) OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack -%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) - $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" $(TOTARGET) +MAINMLFILES := $(filter-out checker/% plugins/%, $(MLFILES) $(MLIFILES)) +MAINMLLIBFILES := $(filter-out checker/% plugins/%, $(MLLIBFILES) $(MLPACKFILES)) + +$(MLDFILE).d: $(D_DEPEND_BEFORE_SRC) $(MAINMLFILES) $(D_DEPEND_AFTER_SRC) $(GENFILES) + $(SHOW)'OCAMLDEP MLFILES MLIFILES' + $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $(MAINMLFILES) $(TOTARGET) -%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) - $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" $(TOTARGET) +$(MLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(MAINMLLIBFILES) $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) + $(SHOW)'OCAMLLIBDEP MLLIBFILES MLPACKFILES' + $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) $(MAINMLLIBFILES) $(TOTARGET) -%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET) +$(PLUGMLDFILE).d: $(D_DEPEND_BEFORE_SRC) $(filter plugins/%, $(MLFILES) $(MLIFILES)) $(D_DEPEND_AFTER_SRC) $(GENFILES) + $(SHOW)'OCAMLDEP plugins/MLFILES plugins/MLIFILES' + $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $(filter plugins/%, $(MLFILES) $(MLIFILES)) $(TOTARGET) -%.mlpack.d: $(D_DEPEND_BEFORE_SRC) %.mlpack $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET) +$(PLUGMLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(filter plugins/%, $(MLLIBFILES) $(MLPACKFILES)) $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) + $(SHOW)'OCAMLLIBDEP plugins/MLLIBFILES plugins/MLPACKFILES' + $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) $(filter plugins/%, $(MLLIBFILES) $(MLPACKFILES)) $(TOTARGET) ########################################################################### # Compilation of .v files @@ -721,26 +747,6 @@ theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) $(HIDE)rm -f theories/Init/$*.glob $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA) -# MExtraction.v generates the ml core file of the micromega tactic. -# We check that this generated code is still in sync with the version -# of micromega.ml in the archive. - -# Note: we now dump to stdout there via "Recursive Extraction" for better -# control on the name of the generated file, and avoid a .ml that -# would end in our $(MLFILES). The "sed" below is to kill the final -# blank line printed by Recursive Extraction (unlike Extraction "foo"). - -MICROMEGAV:=plugins/micromega/MExtraction.v -MICROMEGAML:=plugins/micromega/micromega.ml -MICROMEGAGEN:=plugins/micromega/.micromega.ml.generated - -$(MICROMEGAV:.v=.vo) $(MICROMEGAV:.v=.glob) : $(MICROMEGAV) theories/Init/Prelude.vo $(VO_TOOLS_DEP) - $(SHOW)'COQC $<' - $(HIDE)rm -f $*.glob - $(HIDE)$(BOOTCOQC) $< | sed -e '$$d' > $(MICROMEGAGEN) - $(HIDE)diff -u --strip-trailing-cr $(MICROMEGAML) $(MICROMEGAGEN) || \ - (2>&1 echo "Error: $(MICROMEGAML) and the code generated by $(MICROMEGAV) differ !" && false) - # The general rule for building .vo files : %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) @@ -760,9 +766,9 @@ endif # Dependencies of .v files -%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) "$<" $(TOTARGET) +$(VDFILE).d: $(D_DEPEND_BEFORE_SRC) $(VFILES) $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) + $(SHOW)'COQDEP VFILES' + $(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) $(VFILES) $(TOTARGET) ########################################################################### |