		Search-engine friendly clone of the ACL2 documentation.

Set-gag-mode

Set-checkpoint-summary-limit

Control printing of key checkpoints upon a proof's failure

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)

To see the current limit, invoke (checkpoint-summary-limit).

Note that if some subgoal in a set of key checkpoints is NIL, then such a subgoal will be printed first in the corresponding list, provided of course that the list isn't entirely ignored because of a limit of 0. See nil-goal.