Major Section: OTHER
General Forms: (checkpoints) ; inspect break (checkpoints t) ; inspect break, printing formals of all callsWhen 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.