diff options
Diffstat (limited to 'doc/refman')
-rw-r--r-- | doc/refman/RefMan-uti.tex | 56 |
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. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |