• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
      • 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
          • 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
      • Defttag
      • Sys-call
      • Save-exec
      • Quicklisp
      • Std/io
      • Oslib
      • Bridge
      • Clex
      • Tshell
      • Unsound-eval
      • Hacker
      • ACL2s-interface
      • Startup-banner
      • Command-line
    • 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