From 598e3ae4a8eb8d9bce316e13d71ee48d9ba1a01f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 28 Oct 2017 21:02:48 +0200 Subject: [build] Remove coqmktop in favor of ocamlfind. We remove coqmktop in favor of a couple of simple makefile rules using ocamlfind. In order to do that, we introduce a new top-level file that calls the coqtop main entry. This is very convenient in order to use other builds systems such as `ocamlbuild` or `jbuilder`. An additional consideration is that we must perform a side-effect on init depending on whether we have an OCaml toplevel available [byte] or not. We do that by using two different object files, one for the bytecode version other for the native one, but we may want to review our choice. We also perform some smaller cleanups taking profit from ocamlfind. --- Makefile.build | 73 ++++++++++++++++++++++++++++++++-------------------------- 1 file changed, 40 insertions(+), 33 deletions(-) (limited to 'Makefile.build') diff --git a/Makefile.build b/Makefile.build index 39b793d2b..3e4c5a0b4 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): tools/tolink.cmx $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT_MLTOP) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -o $@ + $(HIDE)$(OCAMLOPT) -linkall -linkpkg -I vernac -I toplevel -I tools \ + -I kernel/byterun/ -cclib -lcoqrun \ + $(SYSMOD) -package camlp5.gramlib \ + tools/tolink.cmx $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) \ + $(COQTOP_OPT_MLTOP) toplevel/coqtop_bin.ml -o $@ $(STRIP) $@ $(CODESIGN) $@ else @@ -390,21 +400,18 @@ $(COQTOPEXE): $(COQTOPBYTE) cp $< $@ endif -$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) +# Are "-cclib lcoqrun -dllib -lcoqrun" necessary? +$(COQTOPBYTE): tools/tolink.cmo $(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)) + $(HIDE)$(OCAMLC) -linkall -linkpkg -I vernac -I toplevel -I tools \ + -I kernel/byterun -dllpath $(abspath kernel/byterun) -cclib -lcoqrun -dllib -lcoqrun \ + $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \ + tools/tolink.cmo $(LINKCMO) $(BYTEFLAGS) \ + $(COQTOP_BYTE_MLTOP) toplevel/coqtop_bin.ml -o $@ tools/tolink.ml: Makefile.build Makefile.common $(SHOW)"ECHO... >" $@ - $(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@ + $(HIDE)echo "let static_modules = \""$(STATICPLUGINS)"\"" > $@ $(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@ $(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@ @@ -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) $(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 -- cgit v1.2.3 From f5cb7eb3e68e4b7d1bb5eeb8d9c58666201945d4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 10 Dec 2017 03:31:55 +0100 Subject: [make] remove unneeded generated file "tolink.ml" When statically linking plugins, the "DECLARE PLUGIN" macro takes care of properly setting up the loaded module table. This setup was also done by `coqmktop`, thus in order to ease bisecting, we didn't take care of it in the `coqmktop` deprecation. Fixes #6364. --- .gitignore | 1 - Makefile | 2 +- Makefile.build | 18 ++++++------------ doc/refman/RefMan-uti.tex | 11 ++++------- toplevel/coqtop_bin.ml | 6 +----- 5 files changed, 12 insertions(+), 26 deletions(-) (limited to 'Makefile.build') diff --git a/.gitignore b/.gitignore index 36536ec96..cec51986d 100644 --- a/.gitignore +++ b/.gitignore @@ -157,7 +157,6 @@ plugins/ssr/ssrvernac.ml kernel/byterun/coq_jumptbl.h kernel/copcodes.ml -tools/tolink.ml ide/index_urls.txt .lia.cache checker/names.ml diff --git a/Makefile b/Makefile index 0078dba20..2637996ed 100644 --- a/Makefile +++ b/Makefile @@ -87,7 +87,7 @@ EXISTINGMLI := $(call find, '*.mli') ## Files that will be generated GENML4FILES:= $(ML4FILES:.ml4=.ml) -export GENMLFILES:=$(LEXFILES:.mll=.ml) tools/tolink.ml kernel/copcodes.ml +export GENMLFILES:=$(LEXFILES:.mll=.ml) kernel/copcodes.ml export GENHFILES:=kernel/byterun/coq_jumptbl.h export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) diff --git a/Makefile.build b/Makefile.build index 3e4c5a0b4..f11719c07 100644 --- a/Makefile.build +++ b/Makefile.build @@ -386,12 +386,12 @@ $(COQTOP_BYTE_MLTOP): toplevel/coqtop_byte_bin.ml $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -package compiler-libs.toplevel -c $< ifeq ($(BEST),opt) -$(COQTOPEXE): tools/tolink.cmx $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT_MLTOP) +$(COQTOPEXE): $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT_MLTOP) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(OCAMLOPT) -linkall -linkpkg -I vernac -I toplevel -I tools \ + $(HIDE)$(OCAMLOPT) -linkall -linkpkg -I toplevel \ -I kernel/byterun/ -cclib -lcoqrun \ $(SYSMOD) -package camlp5.gramlib \ - tools/tolink.cmx $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) \ + $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) \ $(COQTOP_OPT_MLTOP) toplevel/coqtop_bin.ml -o $@ $(STRIP) $@ $(CODESIGN) $@ @@ -401,20 +401,14 @@ $(COQTOPEXE): $(COQTOPBYTE) endif # Are "-cclib lcoqrun -dllib -lcoqrun" necessary? -$(COQTOPBYTE): tools/tolink.cmo $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP) +$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(OCAMLC) -linkall -linkpkg -I vernac -I toplevel -I tools \ + $(HIDE)$(OCAMLC) -linkall -linkpkg -I toplevel \ -I kernel/byterun -dllpath $(abspath kernel/byterun) -cclib -lcoqrun -dllib -lcoqrun \ $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \ - tools/tolink.cmo $(LINKCMO) $(BYTEFLAGS) \ + $(LINKCMO) $(BYTEFLAGS) \ $(COQTOP_BYTE_MLTOP) toplevel/coqtop_bin.ml -o $@ -tools/tolink.ml: Makefile.build Makefile.common - $(SHOW)"ECHO... >" $@ - $(HIDE)echo "let static_modules = \""$(STATICPLUGINS)"\"" > $@ - $(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@ - $(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@ - # coqc COQCCMO:=lib/clib.cma lib/cErrors.cmo toplevel/usage.cmo tools/coqc.cmo diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 002e9625c..962aa98b6 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -12,19 +12,16 @@ linking. Nowadays, the preferred method is to use \texttt{ocamlfind}. The most basic custom toplevel is built using: \begin{quotation} -\texttt{\% make tools/tolink.cmx} \texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg - -package coq.toplevel -I tools tolink.cmx toplevel/coqtop\_bin.ml -o my\_toplevel.native} + -package coq.toplevel toplevel/coqtop\_bin.ml -o my\_toplevel.native} \end{quotation} -For example, to statically link LTAC, you can add it to \texttt{tools/tolink.ml} and use: +For example, to statically link LTAC, you can just do: \begin{quotation} -\texttt{\% make tools/tolink.cmx} \texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg - -package coq.toplevel -package coq.ltac -I tools tolink.cmx toplevel/coqtop\_bin.ml -o my\_toplevel.native} + -package coq.toplevel -package coq.ltac toplevel/coqtop\_bin.ml -o my\_toplevel.native} \end{quotation} - -We will remove the need for the \texttt{tolink} file in the future. +and similarly for other plugins. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/toplevel/coqtop_bin.ml b/toplevel/coqtop_bin.ml index 62459003b..56aced92a 100644 --- a/toplevel/coqtop_bin.ml +++ b/toplevel/coqtop_bin.ml @@ -1,6 +1,2 @@ (* Main coqtop initialization *) -let () = - (* XXX: We should make this a configure option *) - List.iter Mltop.add_known_module Str.(split (regexp " ") Tolink.static_modules); - (* Start the toplevel loop *) - Coqtop.start() +let () = Coqtop.start() -- cgit v1.2.3