Major Section: PARALLEL-PROOF
This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism.
For printing output, the parallel version of the waterfall follows the
precedent of gag-mode. The idea behind gag mode is to print only the
subgoals most relevant to debugging a failed proof attempt. These subgoals
are called 'key checkpoints' (see set-gag-mode for the definition of ``key''
and ``checkpoint''), and we restrict the default output mode for the parallel
version of the waterfall to printing checkpoints similar to these key
checkpoints.
As of this writing, we are aware of exactly one discrepancy between gag mode's key checkpoints and the parallel version of the waterfall's checkpoints. This discrepancy occurs when using ``by'' hints (see hints). As an example, take the following form, which attempts to prove a non-theorem:
(thm (equal (append x y z) (append z (append y x)))
:hints (("Subgoal *1/2'''" :by nil)))
With waterfall parallelism enabled, Subgoal *1/2'' will be printed as a
key checkpoint. This is different from using gag-mode while running
the serial version of the waterfall, which skips printing the subgoal as a
checkpoint.
For those familiar with the ACL2 waterfall, we note that that the parallel version of the waterfall prints key checkpoints that are unproved in the following sense: a subgoal is a key checkpoint if it leads, in the current call of the waterfall, to a goal that is pushed for induction.
