This utility is intended for system hackers, not standard ACL2 users.
ACL2 prints summaries at the conclusions of processing events
(unless summaries are inhibited; see set-inhibit-output-lst and also
see set-inhibited-summary-types). You may arrange for processing to
take place just after the summary, by defining a function with argument
(defun finalize-event-user-test (ctx body state) (declare (xargs :stobjs state) (ignore ctx body)) (cond ((and (boundp-global 'abbrev-evisc-tuple state) (open-output-channel-p *standard-co* :character state)) (pprogn (if (eq (f-get-global 'abbrev-evisc-tuple state) :DEFAULT) (princ$ "Abbrev-evisc-tuple has its default value." *standard-co* state) (princ$ "Abbrev-evisc-tuple has been modified." *standard-co* state)) (newline *standard-co* state))) (t state))) (defattach-system finalize-event-user finalize-event-user-test)
After admission of the two events above, an event summary will conclude with extra printout, for example:
Note: Abbrev-evisc-tuple has its default value.
If the attachment function (above,
(defun finalize-event-user-test2 (ctx body state) (declare (xargs :stobjs state :mode :program) (ignore ctx body)) (observation 'my-test "~|Value of term-evisc-tuple: ~x0~|" (f-get-global 'term-evisc-tuple state))) (defttag t) ; needed for :skip-checks t (defattach-system (finalize-event-user finalize-event-user-test2) :skip-checks t)
So for example:
ACL2 !>(set-term-evisc-tuple (evisc-tuple 2 7 nil nil) state) (:TERM) ACL2 !>(defconst *foo6* '(a b c)) Summary Form: ( DEFCONST *FOO6* ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2 Observation in MY-TEST: Value of term-evisc-tuple: (NIL 2 7 NIL) *FOO6* ACL2 !>
Note that (as of this writing) the macro observation expands to a
call of a
Finally, as promised above, we briefly describe the arguments
(cons 'defthm name)