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. --- doc/refman/RefMan-uti.tex | 56 +++++++++++++---------------------------------- 1 file changed, 15 insertions(+), 41 deletions(-) (limited to 'doc/refman/RefMan-uti.tex') diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index c411db100..002e9625c 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -4,53 +4,27 @@ The distribution provides utilities to simplify some tedious works beside proof development, tactics writing or documentation. -\section[Building a toplevel extended with user tactics]{Building a toplevel extended with user tactics\label{Coqmktop}\ttindex{coqmktop}} +\section[Using Coq as a library]{Using Coq as a library} -The native-code version of \Coq\ cannot dynamically load user tactics -using {\ocaml} code. It is possible to build a toplevel of \Coq, -with {\ocaml} code statically linked, with the tool {\tt - coqmktop}. - -For example, one can build a native-code \Coq\ toplevel extended with a tactic -which source is in {\tt tactic.ml} with the command -\begin{verbatim} - % coqmktop -opt -o mytop.out tactic.cmx -\end{verbatim} -where {\tt tactic.ml} has been compiled with the native-code -compiler {\tt ocamlopt}. This command generates an executable -called {\tt mytop.out}. To use this executable to compile your \Coq\ -files, use {\tt coqc -image mytop.out}. - -A basic example is the native-code version of \Coq\ ({\tt coqtop.opt}), -which can be generated by {\tt coqmktop -opt -o coqopt.opt}. - - -\paragraph[Application: how to use the {\ocaml} debugger with Coq.]{Application: how to use the {\ocaml} debugger with Coq.\index{Debugger}} - -One useful application of \texttt{coqmktop} is to build a \Coq\ toplevel in -order to debug your tactics with the {\ocaml} debugger. -You need to have configured and compiled \Coq\ for debugging -(see the file \texttt{INSTALL} included in the distribution). -Then, you must compile the Caml modules of your tactic with the -option \texttt{-g} (with the bytecode compiler) and build a stand-alone -bytecode toplevel with the following command: +In previous versions, \texttt{coqmktop} was used to build custom +toplevels --- for example for better debugging or custom static +linking. Nowadays, the preferred method is to use \texttt{ocamlfind}. +The most basic custom toplevel is built using: \begin{quotation} -\texttt{\% coqmktop -g -o coq-debug}~\emph{} +\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} \end{quotation} +For example, to statically link LTAC, you can add it to \texttt{tools/tolink.ml} and use: +\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} +\end{quotation} -To launch the \ocaml\ debugger with the image you need to execute it in -an environment which correctly sets the \texttt{COQLIB} variable. -Moreover, you have to indicate the directories in which -\texttt{ocamldebug} should search for Caml modules. - -A possible solution is to use a wrapper around \texttt{ocamldebug} -which detects the executables containing the word \texttt{coq}. In -this case, the debugger is called with the required additional -arguments. In other cases, the debugger is simply called without additional -arguments. Such a wrapper can be found in the \texttt{dev/} -subdirectory of the sources. +We will remove the need for the \texttt{tolink} file in the future. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- 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 'doc/refman/RefMan-uti.tex') 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