Get-event-data
Obtain data stored after at the conclusion of an event
Warning: This is a low-level system utility that may change
somewhat over time. For more details, see the ACL2 source code.
Evaluation of the form (get-event-data key state) returns the value of
key in an association list, which we call an event-data alist.
Such an alist is the value of state global variable
last-event-data. (See programming-with-state for a discussion of
state global variables.) An event-data alist contains certain information
stored at the conclusion of the immediately preceding event, some of which
corresponds to the event's summary. We anticipate continuing to
support at least the following keys, each with value VAL as follows.
- ABORT-CAUSES: VAL is a list of reasons why the proof aborted.
In particular, if the value INTERRUPT is in the list, then the proof was
interrupted (typically with Control-C).
- EVENT: the event.
- FORM: VAL is the ``context'' for the event, printed in the
summary, warnings, and errors.
- HINT-EVENTS: VAL is as in the corresponding field of the event
summary.
- NAMEX: VAL is 0, a single name, or a list of names; see
comments in ACL2 source function access-event-tuple-namex.
- PROVER-STEPS-COUNTED: VAL is as in the corresponding field of
the event summary. Note: This value can be obtained using last-prover-steps.
- RULES: VAL is as in the corresponding field of the event
summary.
- SPLITTER-RULES: VAL represents the corresponding field of the
event summary, as the list (case-split immed-forced if-intro).
- SYSTEM-ATTACHMENTS: VAL lists the pairs (f . g) for which
f is a system function with attachment g (defattach), which
differs from the attachment to f when ACL2 starts up.
- TIME: VAL represents the corresponding field of the event
summary, as the list (prove print proof-tree other).
- WARNINGS: VAL is as in the corresponding field of the event
summary.
