With-output
Suppressing or turning on specified output for an event
The macro with-output can be used to control ACL2 output. It
can be wrapped around an event to create a new event; see embedded-event-form. The macro with-output! is identical except that
it does not create an event and, unlike with-output, it can be called in
code.
Examples
; Turn off all controllable output during evaluation of the indicated thm form.
(with-output
:off :all
:gag-mode nil
:inhibit-er-hard t
(thm (equal (app (app x y) z) (app x (app y z)))))
; Equivalent to the example just above.
(with-output
:off :all!
(thm (equal (app (app x y) z) (app x (app y z)))))
; Prove the indicated theorem with the event summary turned off and
; using the :goals setting for gag-mode.
(with-output
:off summary
:gag-mode :goals
(defthm app-assoc (equal (app (app x y) z) (app x (app y z)))))
; Same effect as just above:
(with-output
:on summary
:summary-off :all
:gag-mode :goals
(defthm app-assoc (equal (app (app x y) z) (app x (app y z)))))
; Turn off all but the ``time'' and ``rules'' parts of the summary.
(with-output
:on summary
:summary-off (:other-than time rules)
:gag-mode :goals ; default: use gag-mode, with goal names printed
(defthm app-assoc (equal (app (app x y) z) (app x (app y z)))))
; Same as specifying :off :all!, but with output types made explicit
; (that is, using the value of constant *valid-output-names*):
(with-output
:off (error warning warning! observation prove proof-builder event history
summary proof-tree)
:gag-mode nil
(thm (equal (app (app x y) z) (app x (app y z)))))
; Same as above, but :stack :push says to save the current
; inhibit-output-lst, which can be restored in a subsidiary with-output call
; that specifies :stack :pop.
(with-output
:stack :push
:off :all
:gag-mode nil
(thm (equal (app (app x y) z) (app x (app y z)))))
; Abbreviate printing in gag-mode for guard goals and induction schemes, but
; defeat abbreviated printing (if any) for terms.
(with-output
:evisc (:gag-mode (evisc-tuple 3 4 nil nil)
:term nil)
(defun h (x)
(declare (xargs :guard t))
(append (cons (make-list 10) x) x)))
; The following use of :ctx causes the error message to start with
; ``ACL2 Error in MY-CUSTOM-CTX'' instead of
; ``ACL2 Error in ( DEFUN FOO ...)''.
(with-output
:ctx 'my-custom-ctx
(defun foo (x) y))
General Form
(with-output :key1 val1 ... :keyk valk form)
where form should evaluate to an error-triple. That evaluation
takes place with output that is according to the values vali of the
keywords, :keyi, as described below. When the scope of with-output
is exited, then all modifications are undone, including the states of output
and summary inhibition, gag-mode, and evisc-tuples. Each
keyword may occur at most once.
Use of the argument :off :all! is treated exactly the same as using
arguments :off :all :gag-mode nil. We assume below that any use of
:off :all! has been expanded away in that manner.
On-off specs
Before discussing the keywords we introduce the notion of ``on-off specs'',
which are the legal values of the keywords :on, :off,
:summary-on, and :summary-off. (As noted above, we ignore
:off :all! below, as it is just an abbreviation for :off :all
:gag-mode nil.) An on-off spec has one of the following forms, where each
symi is a symbol, and subject to restrictions discussed below
- :all
- sym ; a symbol that is not :all
- (sym1 ... symk)
- (:other-than sym1 ... symk)
The set of ``associated valid symbols'' is defined as follows. For
:off or :on, these symbols are the output types that can be
inhibited — that is, members of the list stored in the constant
*valid-output-names*, which is the list (proof-tree error
warning! warning observation prove event
summary proof-builder comment history) —
and they are treated as in set-inhibit-output-lst. Similarly, for
:summary-on or :summary-off, these are the summary types: the
parts of the summary that can be inhibited as in set-inhibited-summary-types, that is, members of the list stored in the
constant *summary-types*, which is the list (errors form header hint-events
redundant rules splitter-rules steps
system-attachments time value warnings). An
on-off spec consisting of associated valid symbols, (sym1 ... symk),
indicates the set of symbols, {sym1,...,symk}. The other legal forms of
on-off spec and their meanings are as follows: :all represents the set of
all associated valid symbols, any other symbol sym abbreviates
(sym), and (:other-than sym1 ... symk) represents the set of
associated valid symbols that are not in the list (sym1 ... symk).
Note that these two notions of ``associated valid symbols'' — the
output types controlled by keywords :on and :off, and the
summary types controlled by keywords :summary-on and
:summary-off — operate independently in the following sense. The
keywords :on and :off control output types from the list
*valid-output-names* displayed above, one of whose members is
SUMMARY. The keywords :summary-on and :summary-off control
summary types from the list *summary-types* displayed above, indicating
which types of summary are to be printed in the case that SUMMARY is
among the output types that are on. This summary control persists even as the
SUMMARY type changes state between off and on. Consider the following
example.
(with-output :off (summary)
(with-output :summary-off (time)
(with-output :on (summary)
(thm (equal (car (append x y)) (if (consp x) (car x) (car y)))))))
The resulting output does not include TIME output in the summary. The
reason is that the second with-output form specifies that TIME
summary output is off; then when the third (innermost) output turns
SUMMARY output on, still, the TIME summary output is off, so the
THM call does not print the TIME part of the summary output. Note
that the same reasoning applies if the third with-output call above
specifies :on :all instead of :on (summary); that case also produces
no time output in the summary. That is, the use of :on :all specifies
which output types are on, but does not affect which summary types are on;
again, output types and summary types are controlled independently by the
respective pairs :on/:off and :summary-on/:summary-off.
Keyword arguments
We turn now to a discussion of the keyword arguments.
:on, :off
The values for these keywords, which are not evaluated, must be on-off
specs for these keywords (as discussed above). If :on :all is specified,
then then every output type is turned on except for those in the set specified
by the value of :off. Otherwise, if :off :all is specified, then
every output type is inhibited except as specified by the value of
:on. Otherwise :all is not specified for either :on or
:off, and the currently-inhibited output types are reduced as specified
by the value of :on and then extended as specified by the value of
:off.
:summary-on, :summary-off
The values for these keywords, which are not evaluated, must be on-off
specs for these keywords. They are interpreted exactly as are the values for
:on and :off as described above, except that instead of output types
they are interpreted with respect to the summary types (i.e., in the
terminology introduced above, with respect to the set of associated valid
symbols for :summary-on and :summary-off).
:gag-mode
The value should evaluate to one of the legal values for set-gag-mode. The effect is as though set-gag-mode has been called with
this argument, before modifying how output is inhibited, at the start of
evaluating the given form.
:evisc
The value should evaluate to a keyword-value-listp, where each key
is a legal keyword for the :sites keyword argument of set-evisc-tuple other than :trace and :brr (that is, a member of
the list (:term :ld :abbrev :gag-mode)), and
each value evaluates to a legal evisc-tuple for that keyword. The
effect is as though set-evisc-tuple has been called, before modifying how
output is inhibited, with this argument at the start of evaluating the given
form.
:ctx
The value should evaluate to a context — see ctx — that
will generally be used throughout evaluation of the given form, in place of
the usual event context (including the "Form" field of the summary).
:stack
The value, which is not evaluated, must be :push or :pop. The
effect of :push is essentially to create a new environment for inferior
calls of with-output that can be reverted (popped) by inferior calls of
with-output, as discussed in the next section. Note that the handling of
the :stack argument pays no attention to the :summary-on or
:summary-off arguments.
:inhibit-er-hard
By default, ACL2 prints messages for hard errors — errors whose
message starts with “HARD ACL2 ERROR” — even when error
output is inhibited (whether by using the keyword, :off, or by calling
set-inhibit-output-lst). This behavior holds when state global
inhibit-er-hard has its default value of nil; see set-inhibit-output-lst. When keyword :inhibit-er-hard is supplied an
expression, the value v of that expression overrides the global value of
inhibit-er-hard: thus when error output is inhibited, hard error messages
are printed if v is nil and they are not printed if v is not
nil. Note that this behavior automatically takes place when
with-output is supplied the arguments :off :all!, but not
:off :all.
More about the stack argument
The :stack keyword's effect is illustrated by the following example,
where ``(encapsulate nil)'' may replaced by ``(progn'' without any
change to the output that is printed.
(with-output
:stack :push :off :all
(encapsulate ()
(defun f1 (x) x)
(with-output :stack :pop (defun f2 (x) x))
(defun f3 (x) x)
(with-output :stack :pop :off warning (in-theory nil))
(defun f4 (x) x)))
The outer with-output call saves the current output settings (as may
have been modified by earlier calls of set-inhibit-output-lst), by
pushing them onto a stack, and then turns off all output. Each inner
with-output call temporarily pops that stack, restoring the starting
output settings, until it completes and undoes the effects of that pop.
Unless event output was inhibited at the top level (see set-inhibit-output-lst), the following output is shown:
Since F2 is non-recursive, its admission is trivial. We observe that
the type of F2 is described by the theorem (EQUAL (F2 X) X).
And then, if summary output was not inhibited at the top level, we get
the rest of this output:
Summary
Form: ( DEFUN F2 ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Summary
Form: ( IN-THEORY NIL)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Note that the use of :off warning suppresses a "Theory" warning
for the (in-theory nil) event, and that in no case will output be printed
for definitions of f1, f3, or f4, or for the encapsulate event itself.
The following more detailed explanation of :stack is intended only for
advanced users. After :gag-mode and :evisc are handled (if present)
but before :on or :off is handled, the value of :stack is
handled as follows. If the value is :push, then state global
inhibit-output-lst-stack is modified by pushing the cons of the values of
state globals inhibit-output-lst and gag-mode onto the value
of state global inhibit-output-lst-stack, which is nil at the
top level. If the value is :pop, then state global
inhibit-output-lst-stack is modified only if non-nil, in which case
its top element is popped and provides the values of state globals
inhibit-output-lst and gag-mode.
Concluding remarks
With-output has no effect in raw Lisp, in the sense that a call
(with-output ... form) macroexpands to form in raw Lisp. Normally
this produces desired behavior, but occasionally you may be a bit surprised.
Consider for example the following book.
(in-package "ACL2")
(with-output
:off :all
(make-event (prog2$ (cw "@@@ NOISE @@@")
'(defun f (x) x))
:check-expansion t))
(make-event (with-output!
:off :all
(value (prog2$ (cw "@@@ QUIET @@@")
'(defun g (x) x))))
:check-expansion t)
When certifying this book, we do not see either ‘NOISE’ or
‘QUIET’. But then when we include this book, we see
‘NOISE’ (but not ‘QUIET’). To see why, we
first note that both events are evaluated in raw Lisp when including the
book (as discussed briefly in the documentation topic, book-compiled-file). The first calls with-output, which (as noted
above) disappears during macroexpansion. The second calls with-output!,
which has the desired effect of suppressing output.
