• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
      • Defun
      • Declare
      • System-utilities
      • Stobj
      • State
        • World
        • Io
          • Fmt
          • Msg
          • Cw
          • Set-evisc-tuple
          • Set-iprint
          • Print-control
          • Read-file-into-string
          • Std/io
          • Msgp
          • Printing-to-strings
          • Evisc-tuple
          • Output-controls
            • With-output
            • Summary
            • Set-inhibit-output-lst
            • Set-gag-mode
              • Set-checkpoint-summary-limit
              • Checkpoint-summary-limit
            • Goal-spec
            • Set-warnings-as-errors
            • Saving-event-data
            • Pso
            • Finalize-event-user
            • Set-inhibit-er
            • Checkpoint-list
            • Set-inhibit-warnings
            • Get-event-data
            • Set-inhibited-summary-types
            • Set-print-clause-ids
            • Set-let*-abstractionp
            • Gag-mode
            • Initialize-event-user
            • Set-raw-proof-format
            • Checkpoint-list-pretty
            • Psof
            • Set-raw-warning-format
            • Toggle-inhibit-warning
            • Toggle-inhibit-er
            • Warnings
            • Show-checkpoint-list
            • Wof
            • Psog
            • Checkpoint-info-list
            • Pso!
            • Toggle-inhibit-warning!
            • Set-duplicate-keys-action!
            • Toggle-inhibit-er!
            • Set-inhibit-warnings!
            • Set-inhibit-er!
          • Observation
          • *standard-co*
          • Ppr-special-syms
          • Standard-oi
          • Standard-co
          • Without-evisc
          • Serialize
          • Output-to-file
          • Fmt-to-comment-window
          • Princ$
          • Character-encoding
          • Open-output-channel!
          • Cw-print-base-radix
          • Set-print-case
          • Set-print-base
          • Print-object$
          • Extend-pathname
          • Print-object$+
          • Fmx-cw
          • Set-print-radix
          • Set-fmt-hard-right-margin
          • File-write-date$
          • Proofs-co
          • Set-print-base-radix
          • Print-base-p
          • *standard-oi*
          • Wof
          • File-length$
          • Fms!-lst
          • Delete-file$
          • *standard-ci*
          • Write-list
          • Trace-co
          • Fmt!
          • Fms
          • Cw!
          • Fmt-to-comment-window!
          • Fms!
          • Eviscerate-hide-terms
          • Fmt1!
          • Fmt-to-comment-window!+
          • Read-file-into-byte-array-stobj
          • Fmt1
          • Fmt-to-comment-window+
          • Cw-print-base-radix!
          • Read-file-into-character-array-stobj
          • Fmx
          • Cw!+
          • Read-objects-from-book
          • Newline
          • Cw+
          • Probe-file
          • Write-objects-to-file!
          • Write-objects-to-file
          • Read-objects-from-file
          • Read-object-from-file
          • Read-file-into-byte-list
          • Set-fmt-soft-right-margin
          • Read-file-into-character-list
          • Io-utilities
        • Wormhole
        • Programming-with-state
        • W
        • Set-state-ok
        • Random$
      • Mutual-recursion
      • Memoize
      • Mbe
      • Io
        • Fmt
        • Msg
        • Cw
        • Set-evisc-tuple
        • Set-iprint
        • Print-control
        • Read-file-into-string
        • Std/io
        • Msgp
        • Printing-to-strings
        • Evisc-tuple
        • Output-controls
          • With-output
          • Summary
          • Set-inhibit-output-lst
          • Set-gag-mode
            • Set-checkpoint-summary-limit
            • Checkpoint-summary-limit
          • Goal-spec
          • Set-warnings-as-errors
          • Saving-event-data
          • Pso
          • Finalize-event-user
          • Set-inhibit-er
          • Checkpoint-list
          • Set-inhibit-warnings
          • Get-event-data
          • Set-inhibited-summary-types
          • Set-print-clause-ids
          • Set-let*-abstractionp
          • Gag-mode
          • Initialize-event-user
          • Set-raw-proof-format
          • Checkpoint-list-pretty
          • Psof
          • Set-raw-warning-format
          • Toggle-inhibit-warning
          • Toggle-inhibit-er
          • Warnings
          • Show-checkpoint-list
          • Wof
          • Psog
          • Checkpoint-info-list
          • Pso!
          • Toggle-inhibit-warning!
          • Set-duplicate-keys-action!
          • Toggle-inhibit-er!
          • Set-inhibit-warnings!
          • Set-inhibit-er!
        • Observation
        • *standard-co*
        • Ppr-special-syms
        • Standard-oi
        • Standard-co
        • Without-evisc
        • Serialize
        • Output-to-file
        • Fmt-to-comment-window
        • Princ$
        • Character-encoding
        • Open-output-channel!
        • Cw-print-base-radix
        • Set-print-case
        • Set-print-base
        • Print-object$
        • Extend-pathname
        • Print-object$+
        • Fmx-cw
        • Set-print-radix
        • Set-fmt-hard-right-margin
        • File-write-date$
        • Proofs-co
        • Set-print-base-radix
        • Print-base-p
        • *standard-oi*
        • Wof
        • File-length$
        • Fms!-lst
        • Delete-file$
        • *standard-ci*
        • Write-list
        • Trace-co
        • Fmt!
        • Fms
        • Cw!
        • Fmt-to-comment-window!
        • Fms!
        • Eviscerate-hide-terms
        • Fmt1!
        • Fmt-to-comment-window!+
        • Read-file-into-byte-array-stobj
        • Fmt1
        • Fmt-to-comment-window+
        • Cw-print-base-radix!
        • Read-file-into-character-array-stobj
        • Fmx
        • Cw!+
        • Read-objects-from-book
        • Newline
        • Cw+
        • Probe-file
        • Write-objects-to-file!
        • Write-objects-to-file
        • Read-objects-from-file
        • Read-object-from-file
        • Read-file-into-byte-list
        • Set-fmt-soft-right-margin
        • Read-file-into-character-list
        • Io-utilities
      • Defpkg
      • Apply$
      • Loop$
      • Programming-with-state
      • Arrays
      • Characters
      • Time$
      • Defmacro
      • Loop$-primer
      • Fast-alists
      • Defconst
      • Evaluation
      • Guard
      • Equality-variants
      • Compilation
      • Hons
      • ACL2-built-ins
      • Developers-guide
      • System-attachments
      • Advanced-features
      • Set-check-invariant-risk
      • Numbers
      • Efficiency
      • Irrelevant-formals
      • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
      • Redefining-programs
      • Lists
      • Invariant-risk
      • Errors
      • Defabbrev
      • Conses
      • Alists
      • Set-register-invariant-risk
      • Strings
      • Program-wrapper
      • Get-internal-time
      • Basics
      • Packages
      • Oracle-eval
      • Defmacro-untouchable
      • <<
      • Primitive
      • Revert-world
      • Unmemoize
      • Set-duplicate-keys-action
      • Symbols
      • Def-list-constructor
      • Easy-simplify-term
      • Defiteration
      • Fake-oracle-eval
      • Defopen
      • Sleep
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
      • With-output
      • Summary
      • Set-inhibit-output-lst
      • Set-gag-mode
        • Set-checkpoint-summary-limit
        • Checkpoint-summary-limit
      • Goal-spec
      • Set-warnings-as-errors
      • Saving-event-data
      • Pso
      • Finalize-event-user
      • Set-inhibit-er
      • Checkpoint-list
      • Set-inhibit-warnings
      • Get-event-data
      • Set-inhibited-summary-types
      • Set-print-clause-ids
      • Set-let*-abstractionp
      • Gag-mode
      • Initialize-event-user
      • Set-raw-proof-format
      • Checkpoint-list-pretty
      • Psof
      • Set-raw-warning-format
      • Toggle-inhibit-warning
      • Toggle-inhibit-er
      • Warnings
      • Show-checkpoint-list
      • Wof
      • Psog
      • Checkpoint-info-list
      • Pso!
      • Toggle-inhibit-warning!
      • Set-duplicate-keys-action!
      • Toggle-inhibit-er!
      • Set-inhibit-warnings!
      • Set-inhibit-er!
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Summary
• Set-gag-mode

Checkpoint-summary-limit

Control printing of key checkpoints upon a proof's failure

See set-checkpoint-summary-limit for a discussion of the checkpoint-summary-limit. Evaluation of the form (checkpoint-summary-limit) produces the current checkpoint-summary-limit, and can be invoked with the keyword hack (see keyword-commands). For example:

ACL2 !>:checkpoint-summary-limit
(NIL . 3)
ACL2 !>