Summary
The summary printed at the conclusion of an event
At the conclusion of an event form, ACL2 prints (by default)
information summarizing the event. The entire summary may be avoided —
see set-inhibit-output-lst — or if you prefer, you may inhibit
just specified components of the summary — see set-inhibited-summary-types. The components are listed in the constant
*summary-types* and most are available programmatically: see get-event-data. Some are omitted, however, if they would otherwise be empty.
Here is a brief summary of the components, listed alphabetically. Most are
printed with an initial field indicator, e.g., ``Rules: ''; a few, as
indicated below, are not.
- Errors (no field indicator): The final error message
- Form (no field indicator): The ``context'' for the event (ctx)
- Header (no field indicator): The initial word ``Summary''
- Hint-events: Certain hints (e.g., :use hints) supplied
- Redundant: There is field indicator, but a message is printed that
notes a redundant event (see redundant-events) above the rest of the
summary. That message is printed even when SUMMARY output or the
REDUNDANT summary-type is inhibited, if EVENT output is not
inhibited.
- Rules: Runes contributing to the proof or storage of the
event
- Splitter-rules: Potential causes of case splits (see splitter)
- Steps (field indicator is "Prover steps counted"): Prover
steps (see set-prover-step-limit)
- System-attachments: List of doublets (f g) for which f is a
system function with attachment g (see defattach), when g
differs from the initial attachment to f
- Time: Runtime (or real time; see get-internal-time)
- Value: When an event form under progn or encapsulate
evaluates to (mv nil val state), val is printed immediately under
the summary fields. (No field indicator)
- Warnings: All warning string summaries printed during processing of
the event
Subtopics
- Checkpoint-summary-limit
- Control printing of key checkpoints upon a proof's failure
