Checkpoint-list
Return prover key checkpoint clauses programmatically.
Recall the key checkpoints printed at the end of a failed proof
attempt. Some are labeled ``Key checkpoint at the top level''; let us call
these checkpoints ``top-level'', and denote others as ``not top-level''. When
the most recent proof attempt was one that failed, (checkpoint-list top-p
state) returns clauses corresponding to key checkpoints, as follows. If
top-p is t, then the list of top-level checkpoints is returned.
Otherwise the list of checkpoints that are not top-level is returned. In each
case, the order of checkpoints is the same as would be found in the summary of
a proof attempt; that is, their order agrees with the order in which they are
generated during the proof attempt.
Related tools. Note that each returned checkpoint is a clause, that
is, a list of terms, implicitly disjoined. For a similar utility that
instead returns each checkpoint as an untranslated term such as one
would see during a proof, see checkpoint-list-pretty. See also show-checkpoint-list for a related tool that displays checkpoints rather than
returning them, and see checkpoint-info-list for a tool similar to
checkpoint-list that returns additional information.
Examples may be found in the community-books file
checkpoints-tests-input.lsp, with corresponding output (using the run-script tool) in that same directory, in file
checkpoints-tests-log.txt.
Here are details to keep in mind.
- A return value of :UNAVAILABLE indicates that no information on
checkpoints is available, presumably because the most recent proof attempt
succeeded.
- This utility produces the appropriate result even when inhibited
SUMMARY output (see set-inhibit-output-lst) suppresses the
printing of key checkpoints in a proof attempt.
- Each forcing round (see forcing-round) is considered a new proof
attempt for purposes of this tool.
- The notion of ``most recent proof attempt'' includes proof attempts made
during make-event expansion.
- If the form (checkpoint-list t state) evaluates to nil, then the
most recent proof attempt produced no checkpoints at the top level. This
happens when a failed proof is aborted before producing any checkpoints
because of reaching a time-limit or a step-limit. So when
(checkpoint-list t state) evaluates to nil as part of a larger
program, the caller of checkpoint-list might be well served by instead
treating the list of top-level checkpoints as (list (list <goal>)), where
<goal> is the translated form of the most recent conjecture supplied to
the prover.
