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 standalone bytecode toplevel with the following command:
%coqmktop -g -o coq-debug <your
.cmo files>
Then you can launch Coq under the Objective Caml debugger with the option -db of coqtop:
%coqtop -image coq-debug -db
If for any reason you don't want to run coqtop but to use directly the executable coq-debug (for instance to use the Objective Caml debugger under GNU Emacs) 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 write a wrapper around ocamldebug which detects the executables containing the word coq:
#!/bin/sh
export COQLIB=the Coq library path
export COQTH=$COQLIB/theories
OCAMLDEBUG=the true path to ocamldebug
coqdebug="no"
for op in $*; do case `basename $op` in *coq*) coqdebug="yes";; esac; done
if test $coqdebug = "yes"
then exec $OCAMLDEBUG <debugger options like -I> $*
else exec $OCAMLDEBUG $*
fi
export COQLIB=the Coq library path
export COQTH=$COQLIB/theories
OCAMLDEBUG=the true path to ocamldebug
coqdebug="no"
for op in $*; do case `basename $op` in *coq*) coqdebug="yes";; esac; done
if test $coqdebug = "yes"
then exec $OCAMLDEBUG <debugger options like -I> $*
else exec $OCAMLDEBUG $*
fi