		Search-engine friendly clone of the ACL2 documentation.

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