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
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
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
'waterfall-printing-when-finished has a non-
then such a message will also be printed at the completion of each subgoal.
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
.') each time it starts a new subgoal.
Note that this form cannot be used at the top level of a book, or of a
encapsulate event. Here is a workaround for use in such
contexts; of course, you may replace
:very-limited with any other legal
(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)
set-waterfall-printing is automatically called by
To enable the printing of information when a subgoal is finished, assign a
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)