10.6 Testing and Debugging your Tactic
When your tactic does not behave as expected, it is possible to trace it dynamically from Coq. In order to do this, you have first to leave the toplevel of Coq, and come back to the Ocaml interpreter. This can be done using the command Drop (cf. Section 5.8.2). Once in the Ocaml toplevel, load the file tactics/include.ml. This file installs several pretty printers for proof trees, goals, terms, abstract syntax trees, names, etc. It also contains the function go:unit -> unit that enables to go back to Coq's toplevel.The modules Tacmach and Pfedit contain some basic functions for extracting information from the state of the proof engine. Such functions can be used to debug your tactic if necessary. Let us mention here some of them:
- val get_pftreestate : unit -> pftreestate.
Projects the current state of the proof engine. - val proof_of_pftreestate : pftreestate -> proof.
Projects the current state of the proof tree. A pretty-printer displays it in a readable form. - val top_goal_of_pftreestate : pftreestate -> goal sigma.
Projects the goal and the existential variables mapping from the current state of the proof engine. - val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma.
Projects the goal and mapping corresponding to the nth subgoal that remains to be proven - val traverse : int -> pftreestate -> pftreestate.
Yields the children of the node that the current state of the proof engine points to. - val solve_nth_pftreestate :
int -> tactic -> pftreestate -> pftreestate.
Provides the new state of the proof engine obtained applying a given tactic to some unproven sub-goal.
Finally, the traditional Ocaml debugging tools like the directives trace and untrace can be used to follow the execution of your functions. Frequently, a better solution is to use the Ocaml debugger, see Chapter 12.