• 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
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • 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!
      • Macros
      • Interfacing-tools
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • ACL2
  • Io

Output-controls

Methods for controlling the output produced by the ACL2 prover

This topic pertains primarily to processing of events, often involving the prover. For a general discussion about redirection of ACL2 output to a file, see output-to-file.

Subtopics

With-output
Suppressing or turning on specified output for an event
Summary
The summary printed at the conclusion of an event
Set-inhibit-output-lst
Control output
Set-gag-mode
Modify the nature of proof output
Goal-spec
To indicate where a hint is to be used
Set-warnings-as-errors
Changing warnings to hard errors (and vice-versa)
Saving-event-data
Save data stored for subsidiary events
Pso
Show the most recently saved output
Finalize-event-user
User-supplied code to complete events, e.g., with extra summary output
Set-inhibit-er
Control the error output
Checkpoint-list
Return prover key checkpoint clauses programmatically.
Set-inhibit-warnings
Control warnings
Get-event-data
Obtain data stored after at the conclusion of an event
Set-inhibited-summary-types
Control which parts of the summary are printed
Set-print-clause-ids
Cause subgoal numbers to be printed when 'prove output is inhibited
Set-let*-abstractionp
To shorten many prettyprinted clauses
Gag-mode
Verbosity of proof output
Initialize-event-user
User-supplied code to initiate events
Set-raw-proof-format
Proof output with runes as lists and maybe clausal goals
Checkpoint-list-pretty
Return prover key checkpoint goals programmatically.
Psof
Show the most recently saved output
Set-raw-warning-format
Print some warnings in a ``raw'', s-expression format
Toggle-inhibit-warning
Add or delete a warning string from the inhibit-warnings-table
Toggle-inhibit-er
Add or delete an error output string from the inhibit-er-table
Warnings
Warnings emitted by the ACL2 proof process
Show-checkpoint-list
Display prover key checkpoint information.
Wof
Direct standard output and proofs output to a file
Psog
Show the most recently saved output with gag-mode
Checkpoint-info-list
Return prover key checkpoint information programmatically.
Pso!
Show the most recently saved output, including proof-tree output
Toggle-inhibit-warning!
Toggle an inhibit-warnings-table entry non-locally
Set-duplicate-keys-action!
Non-local version of set-duplicate-keys-action
Toggle-inhibit-er!
Toggle an inhibit-er-table entry non-locally
Set-inhibit-warnings!
Control warnings non-locally
Set-inhibit-er!
Control error output non-locally