From 598e3ae4a8eb8d9bce316e13d71ee48d9ba1a01f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
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{<your \texttt{.cmo} files>}
+\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 <e+git@x80.org>
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

