diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 83 |
1 files changed, 42 insertions, 41 deletions
diff --git a/Makefile.build b/Makefile.build index 991942bf0..940943c41 100644 --- a/Makefile.build +++ b/Makefile.build @@ -228,8 +228,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 +239,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 +369,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 +400,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 +415,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 +452,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 +467,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 +507,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 +525,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 @@ -734,8 +735,8 @@ $(MICROMEGAV:.v=.vo) $(MICROMEGAV:.v=.glob) : $(MICROMEGAV) theories/Init/Prelud $(SHOW)'COQC $<' $(HIDE)rm -f $*.glob $(HIDE)$(BOOTCOQC) $< | sed -e '$$d' > $(MICROMEGAGEN) - $(HIDE)cmp -s $(MICROMEGAML) $(MICROMEGAGEN) || \ - echo "Warning: $(MICROMEGAML) and the code generated by $(MICROMEGAV) differ !" + $(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 : |