		Search-engine friendly clone of the ACL2 documentation.

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.
Suppose a proof attempt is aborted in favor of proving the original goal by induction, as typically indicated with the following prover output.
```
We therefore abandon our previous work on this conjecture and
reassign the name *1 to the original conjecture.
```
In that case, the unique top-level checkpoint is (<GOAL>), so the list of top-level checkpoints is ((<GOAL>)). Moreover, all information stored for the proof attempt is based on the part of the attempt starting after returning to prove the original goal by induction; all checkpoints produced before that happens will be lost. If that isn't what you want, consider using :otf-flg.
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.