CHECKPOINTS
seeing what is the prover up to
Major Section: OTHER
General Forms:
(checkpoints) ; inspect break
(checkpoints t) ; inspect break, printing formals of all calls
When the form (checkpoints) is executed during a break from a proof, or
at the end of a proof that the user has aborted, a backtrace stack will be
printed that gives some idea of what the theorem prover has been doing.
Moreover, by evaluating (print-checkpoints t) (see print-checkpoints)
one can get trace-like information about prover functions, including time
summaries, printed to the screen during a proof. This feature is currently
quite raw and may be refined considerably as time goes on. For example, the
usual inhibit-output-lst control of printing is irrelevant for printing these
checkpoints.
