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, namely, in the value of state global
variable last-event-data (see programming-with-state). That alist
contains certain information stored at the conclusion of the immediately
preceding event, some of which corresponds to the event's summary. For
each key the corresponding value, VAL, is 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).
- 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
- 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
- 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