Major Section: SWITCHES-PARAMETERS-AND-MODES
See set-gag-mode for a discussion of key checkpoints.
Examples: ; (Default) When a proof fails, print all key checkpoints before ; induction but at most 3 key checkpoints after induction: (set-checkpoint-summary-limit (nil . 3)) ; When a proof fails, print at most 3 key checkpoints before ; induction but all 3 key checkpoints after induction: (set-checkpoint-summary-limit (3 . nil)) ; When a proof fails, print at most 3 key checkpoints before ; induction and at most 5 key checkpoints after induction: (set-checkpoint-summary-limit (3 . 5)) ; When a proof fails, print at most 3 key checkpoints before ; induction and at most 3 key checkpoints after induction: (set-checkpoint-summary-limit (3 . 3)) ; or equivalently, (set-checkpoint-summary-limit 3) ; When a proof fails, print all key checkpoints: (set-checkpoint-summary-limit (nil . nil)) ; or equivalently, (set-checkpoint-summary-limit nil) ; When a proof fails, print no information at all about key checkpoints: (set-checkpoint-summary-limit t) General Forms: (set-checkpoint-summary-limit (n1 . n2)) (set-checkpoint-summary-limit n) (set-checkpoint-summary-limit t)where each of
n1 and n2 is a natural number or nil. For the
second form, n can be a natural number or nil and is treated as
(n . n). The value t inhibits all printing of checkpoint summary
information. The values n1 and n2 determine printing of key
checkpoints generated before the first induction and generated after the
first induction, respectively, where at most n1 or n2 (respectively)
such key checkpoints are printed unless the value is nil, in which case
there is no limitation.The argument x for set-checkpoint-summary-limit, as described above,
may be quoted, i.e. supplied as 'x or (quote x). Thus, you may use
the keyword form (see keyword-commands) if you prefer, for example:
:set-checkpoint-summary-limit (nil . 3)
