12.1 Building a toplevel extended with user tactics

The native-code version of Coq cannot dynamically load user tactics using Objective Caml code. It is possible to build a toplevel of Coq, with Objective Caml code statically linked, with the tool coqmktop.

For example, one can build a native-code Coq toplevel extended with a tactic which source is in tactic.ml with the command

     % coqmktop -opt -o mytop.out tactic.cmx

where tactic.ml has been compiled with the native-code compiler ocamlopt. This command generates an image of Coq called mytop.out. One can run this new toplevel with the command coqtop -image mytop.out.

A basic example is the native-code version of Coq (coqtop -opt), which can be generated by coqmktop -opt -o coqopt.out.

See the man page of coqmktop for more details and options.

Application: how to use the Objective Caml debugger with Coq.

One useful application of coqmktop is to build a Coq toplevel in order to debug your tactics with the Objective Caml debugger. You need to have configured and compiled Coq for debugging (see the file INSTALL included in the distribution). Then, you must compile the Caml modules of your tactic with the option -g (with the bytecode compiler) and build a stand-alone bytecode toplevel with the following command:

% coqmktop -g -o coq-debug <your .cmo files>

To launch the Objective Camldebugger with the image you need to execute it in an environment which correctly sets the COQLIB variable. Moreover, you have to indicate the directories in which ocamldebug should search for Caml modules.

A possible solution is to use a wrapper around ocamldebug which detects the executables containing the word 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 tools/dev subdirectory of the sources.