Major Section: SWITCHES-PARAMETERS-AND-MODES
Examples: (set-saved-output t t) ; save proof output for later, but inhibit it now (set-saved-output t :all) ; save proof output for later, but inhibit all ; output (except WARNING!, for critical warnings, ; and ERROR, unless these are already inhibited) :set-saved-output t :all ; same as the line above (set-saved-output t nil) ; save proof output for later, but print it now too (set-saved-output nil t) ; do not save proof output, and inhibit it (set-saved-output nil nil); do not save proof output or inhibit output (set-saved-output nil :same), (set-saved-output t :same) ; save proof output or not, as indicated, but do ; not change which output is inhibited (set-saved-output nil :normal) ; the behavior when ACL2 first starts up: do not ; save output, and only inhibit proof-tree output (set-saved-output t '(warning observation proof-tree prove)) ; save proof output for later, and inhibit the ; indicated kinds of output General Form: (set-saved-output save-flg inhibit-flg)Parameter
tto cause output to be saved for later display using
pso!; see pso and see pso!, and see the documentation for proof-checker commands of the same names. Set
nilto turn off this feature; except, it always stays on in proof-checker sessions entered with
verify. The other argument,
inhibit-flg, controls whether output should be inhibited when it is created (normally, during a proof attempt). So a common combination is to set both arguments to
t, to indicate that output should be suppressed for now but saved for printing with
pso!. The examples above give a good summary of the functionality for the second argument.
Saved output is cleared at the start of every event, and also at the start of
every proof-checker commands that invoke the prover. Note that
interactive proof-checker commands, that is, from a proof-checker
session entered with
verify, are always run with output saved.
Also see set-gag-mode; and see set-print-clause-ids, which causes subgoal numbers to be printed during proof attempts when output is inhibited.
See set-inhibit-output-lst if you want to inhibit certain output from the prover but not other output (e.g., not the summary), and you don't want to save any output.