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,

**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

Examples may be found in the community-books file
`run-script` tool) in that same directory, in file

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 tonil , 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 tonil as part of a larger program, the caller ofcheckpoint-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.