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)