Set-waterfall-printing
For ACL2(p): configuring the printing that occurs within the parallelized waterfall
This documentation topic relates to the experimental
extension of ACL2 supporting parallel execution and proof; see parallelism.
General Forms:
(set-waterfall-printing :full) ; print everything
(set-waterfall-printing :limited) ; print a subset that's thought to be useful
(set-waterfall-printing :very-limited) ; print an even smaller subset
Set-waterfall-printing evaluates its argument, which indicates how
much printing should occur when executing ACL2 with the parallelized version
of the waterfall. It only affects the printing that occurs when parallelism
mode is enabled for the waterfall (see set-waterfall-parallelism).
A value of :full is intended to print the same output as in serial
mode. This output will be interleaved unless the waterfall-parallelism mode
is one of nil or :pseudo-parallel.
A value of :limited omits most of the output that occurs in the serial
version of the waterfall. Instead, the proof attempt prints key checkpoints
(see ACL2p-key-checkpoints). The value of :limited also prints
messages that indicate which subgoal is currently being proved, along with the
wall-clock time elapsed since the theorem began its proof; and if state global
'waterfall-printing-when-finished has a non-nil value, then such a
message will also be printed at the completion of each subgoal. The function
print-clause-id-okp may receive an attachment to limit such printing; see
set-print-clause-ids. Naturally, these subgoal numbers can appear out
of order, because the subgoals can be proved in parallel.
A value of :very-limited is treated the same as :limited, except
that instead of printing subgoal numbers, the proof attempt prints a period
(`.') each time it starts a new subgoal.
Note that this form cannot be used at the top level of a book, or of a
progn or encapsulate event. Here is a workaround for use in
such contexts; of course, you may replace :very-limited with any other
legal argument for set-waterfall-printing.
(make-event (er-progn (set-waterfall-printing :very-limited)
(value '(value-triple nil))))
(For more about event contexts and the use of make-event, see make-event, in particular the section ``Restriction to Event Contexts.'')
The following form has the effect described above, except that it will
affect waterfall-printing even when including a certified book that contains
it.
(make-event (er-progn (set-waterfall-printing :very-limited)
(value '(value-triple nil)))
:check-expansion t)
Note that set-waterfall-printing is automatically called by set-waterfall-parallelism.
To enable the printing of information when a subgoal is finished, assign a
non-nil value to global waterfall-printing-when-finished. This can
be accomplished by entering the following at the top level:
(f-put-global 'waterfall-printing-when-finished t state)
