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.