[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.

1 files changed, 15 insertions, 41 deletions

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.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%