diff options
Diffstat (limited to 'Makefile.build')
-rw-r--r-- | Makefile.build | 124 |
1 files changed, 67 insertions, 57 deletions
diff --git a/Makefile.build b/Makefile.build index 867c494a1..cbc1cbaab 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=$(if $(filter plugins/%,$@),-I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(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) @@ -228,8 +234,8 @@ endef define bestocaml $(if $(OPT),\ -$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@ && $(CODESIGN) $@,\ -$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^) +$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ -linkpkg $(1) $^ && $(STRIP) $@ && $(CODESIGN) $@,\ +$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ -linkpkg $(1) $^) endef # Camlp5 settings @@ -239,9 +245,8 @@ CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) -SYSMOD:=str unix dynlink threads -SYSCMA:=$(addsuffix .cma,$(SYSMOD)) -SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD)) +# Main packages linked by Coq. +SYSMOD:=-package num,str,unix,dynlink,threads # We do not repeat the dependencies already in SYSMOD here P4CMA:=gramlib.cma @@ -370,19 +375,30 @@ grammar/%.cmi: grammar/%.mli ########################################################################### -# Main targets (coqmktop, coqtop.opt, coqtop.byte) +# Main targets (coqtop.opt, coqtop.byte) ########################################################################### .PHONY: coqbinaries coqbyte -coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) +coqbinaries: $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) coqbyte: $(COQTOPBYTE) $(CHICKENBYTE) +COQTOP_OPT_MLTOP=toplevel/coqtop_opt_bin.cmx +COQTOP_BYTE_MLTOP=toplevel/coqtop_byte_bin.cmo + +$(COQTOP_BYTE_MLTOP): toplevel/coqtop_byte_bin.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -package compiler-libs.toplevel -c $< + ifeq ($(BEST),opt) -$(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) +$(COQTOPEXE): $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT_MLTOP) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -o $@ + $(HIDE)$(OCAMLOPT) -linkall -linkpkg -I toplevel \ + -I kernel/byterun/ -cclib -lcoqrun \ + $(SYSMOD) -package camlp5.gramlib \ + $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) \ + $(COQTOP_OPT_MLTOP) toplevel/coqtop_bin.ml -o $@ $(STRIP) $@ $(CODESIGN) $@ else @@ -390,23 +406,14 @@ $(COQTOPEXE): $(COQTOPBYTE) cp $< $@ endif -$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) +# Are "-cclib lcoqrun -dllib -lcoqrun" necessary? +$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ - -# coqmktop - -COQMKTOPCMO:=lib/clib.cma lib/cErrors.cmo tools/tolink.cmo tools/coqmktop.cmo - -$(COQMKTOP): $(call bestobj, $(COQMKTOPCMO)) - $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) - -tools/tolink.ml: Makefile.build Makefile.common - $(SHOW)"ECHO... >" $@ - $(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@ - $(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@ - $(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@ + $(HIDE)$(OCAMLC) -linkall -linkpkg -I toplevel \ + -I kernel/byterun -dllpath $(abspath kernel/byterun) -cclib -lcoqrun -dllib -lcoqrun \ + $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \ + $(LINKCMO) $(BYTEFLAGS) \ + $(COQTOP_BYTE_MLTOP) toplevel/coqtop_bin.ml -o $@ # coqc @@ -414,7 +421,7 @@ COQCCMO:=lib/clib.cma lib/cErrors.cmo toplevel/usage.cmo tools/coqc.cmo $(COQC): $(call bestobj, $(COQCCMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) + $(HIDE)$(call bestocaml, $(SYSMOD)) ########################################################################### # other tools @@ -451,11 +458,11 @@ tools/coqdep_boot.cmx : tools/coqdep_common.cmx $(COQDEPBOOT): $(call bestobj, $(COQDEPBOOTSRC)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, -I tools, unix) + $(HIDE)$(call bestocaml, -I tools -package unix) $(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, -I tools, unix) + $(HIDE)$(call bestocaml, -I tools -package unix) # The full coqdep (unused by this build, but distributed by make install) @@ -466,36 +473,36 @@ COQDEPCMO:=lib/clib.cma lib/cErrors.cmo lib/cWarnings.cmo \ $(COQDEP): $(call bestobj, $(COQDEPCMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) + $(HIDE)$(call bestocaml, $(SYSMOD)) $(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,) + $(HIDE)$(call bestocaml,) COQMAKEFILECMO:=lib/clib.cma tools/coq_makefile.cmo $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,str unix threads) + $(HIDE)$(call bestocaml, -package str,unix,threads) $(COQTEX): $(call bestobj, tools/coq_tex.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,str) + $(HIDE)$(call bestocaml, -package str) $(COQWC): $(call bestobj, tools/coqwc.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,) + $(HIDE)$(call bestocaml, -package str) COQDOCCMO:=lib/clib.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,,str unix) + $(HIDE)$(call bestocaml, -package str,unix) -$(COQWORKMGR): $(call bestobj, lib/clib.cma stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo) +$(COQWORKMGR): $(call bestobj, lib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,, $(SYSMOD)) + $(HIDE)$(call bestocaml, $(SYSMOD)) # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave @@ -506,13 +513,13 @@ FAKEIDECMO:= lib/clib.cma lib/cErrors.cmo lib/spawn.cmo ide/document.cmo \ $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,-I ide,str unix threads) + $(HIDE)$(call bestocaml, -I ide -package str,unix,threads) # 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) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, -I checker,) + $(HIDE)$(call bestocaml, -I checker) ########################################################################### # Csdp to micromega special targets @@ -524,7 +531,7 @@ CSDPCERTCMO:=lib/clib.cma $(addprefix plugins/micromega/, \ $(CSDPCERT): $(call bestobj, $(CSDPCERTCMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,nums unix) + $(HIDE)$(call bestocaml, -package num,unix) ########################################################################### # tests @@ -670,21 +677,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 @@ -756,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) ########################################################################### |