for ACL2(p): configuring the printing that occurs within the parallelized waterfall

This documentation topic relates to the experimental extension of ACL2 supporting parallel evaluation 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 takes an argument that 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 proof checkpoints, similar to (but still distinct from) gag-mode (see set-gag-mode). As applies to much of the parallelism extension, the presentation of these checkpoints is still under development, and feedback concerning them is welcome. The value of :limited also prints messages that indicate which subgoal is currently being proved. (The function print-clause-id-okp may receive an attachment to limit such printing; see set-print-clause-ids.) Naturally, these subgoal numbers can be out of order, because they 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: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. Moreover, set-waterfall-printing events are never redundant (see redundant-events).