EVENTS

functions that extend the logic
Major Section:  ACL2 Documentation

Some Related Topics

Any extension of the syntax of ACL2 (i.e., the definition of a new constant or macro), the axioms (i.e., the definition of a function), or the rule database (i.e., the proof of a theorem), constitutes a logical ``event.'' Events change the ACL2 logical world (see world). Indeed, the only way to change the ACL2 world is via the successful evaluation of an event function. Every time the world is changed by an event, a landmark is left on the world and it is thus possible to identify the world ``as of'' the evaluation of a given event. An event may introduce new logical names. Some events introduce no new names (e.g., verify-guards), some introduce exactly one (e.g., defmacro and defthm), and some may introduce many (e.g., encapsulate ).

ACL2 typically completes processing of an event by printing a summary that includes a breakdown of runtime (cpu time) used and, unless proofs are skipped (see ld-skip-proofsp) or summary output is inhibited (see set-inhibit-output-lst), information about the proof attempt (if any) including a list of rules used, a summary of warnings, and the number of ``prover steps'' (if any; see with-prover-step-limit). A detail: The time is calculated using Common Lisp function get-internal-run-time, which may ignore calls to external tools (see sys-call and see clause-processor).

See embedded-event-form for a discussion of events permitted in books.