key checkpoints in ACL2(p)
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.

Some Related Topics

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.