Major Section: SWITCHES-PARAMETERS-AND-MODES
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)
