• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Miscellaneous
      • Output-controls
        • With-output
        • Summary
        • Set-inhibit-output-lst
        • Set-gag-mode
        • 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!
        • Bdd
        • Macros
        • Installation
        • Mailing-lists
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Kestrel-utilities
    • Output-controls

    Show-checkpoint-list

    Display prover key checkpoint information.

    See checkpoint-list for relevant background. Evaluation of the macro call (show-checkpoint-list) prints checkpoint clauses (as returned by checkpoint-list) as well as related information. An optional argument has default nil; when it is not nil, then the checkpoints are printed as untranslated terms, as described in the documentation for checkpoint-list-pretty. Whether printed as a clause or as an untranslated term, each checkpoint is printed with its goal-spec, i.e., the user-friendly goal name that one sees in prover output for a clause-identifier.

    Also shown are whether or not at least one goal was forced during the failed proof and whether the proof was aborted, and (briefly) why.