|
|
|---|
|
|
|
|---|
Key checkpoints in ACL2(p)
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,
For those familiar with the ACL2 waterfall, we note 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.