Major Section: SWITCHES-PARAMETERS-AND-MODES
Examples: (set-inhibit-output-lst '(warning)) (set-inhibit-output-lst '(proof-tree prove proof-checker)) (set-inhibit-output-lst *valid-output-names*) ; inhibit all prover output :set-inhibit-output-lst (proof-tree prove)where
General Form: (set-inhibit-output-lst lst)
lstis a form (which may mention
state) that evaluates to a list of names, each of which is the name of one of the following ``kinds'' of output produced by ACL2.
error error messages warning warnings other than those related to soundness warning! warnings (of all degrees of importance) observation observations prove commentary produced by the theorem prover proof-checker commentary produced by the proof-checker event non-proof commentary produced by events such as defun and encapsulate expansion commentary produced by make-event expansion summary the summary at the successful conclusion of an event proof-tree proof-tree outputIt is possible to inhibit each kind of output by putting the corresponding name into
lst. For example, if
'warningis included in (the value of)
lst, then no warnings are printed except those related to soundness, e.g., the inclusion of an uncertified book. Note that proof-tree output is affected by
set-inhibit-output-lst; see proof-tree.
See with-output for a variant of this utility that can be used in books.
Printing of events on behalf of
defstobj is inhibited when both
lst. Otherwise, printing of events is controlled by
Note for advanced users. By including
lst, you are
warning as well: all warnings will be inhibited.
This is not the case if you modify value of state global variable
'inhibit-output-lst directly (with
then, if you include
warning! but not
warning, then warnings not
related to soundness will still be printed (which is probably not what was