user-supplied code to complete events, e.g., with extra summary output

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 of state that returns one value, namely state. Your function should normally be a guard-verified :logic mode function with no guard other than that provided by the input requirement on state, that is, (state-p state); but later below we discuss how to avoid this requirement. You then attach (see defattach) your function to the function finalize-event-user. The following example illustrates how this all works.

(defun finalize-event-user-test (state)
  (declare (xargs :stobjs state))
  (cond ((and (boundp-global 'abbrev-evisc-tuple state)
              (open-output-channel-p *standard-co*
          (if (eq (f-get-global 'abbrev-evisc-tuple state) :DEFAULT)
              (princ$ "Abbrev-evisc-tuple has its default value.~%"
            (princ$ "Abbrev-evisc-tuple has been modified.~%"
        (t state)))

(defattach 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, finalize-event-user-test) does not meet all the requirements stated above, then you can use the :skip-checks argument of defattach to get around the requirement, as illustrated by the following example.

(defun finalize-event-user-test2 (state)
  (declare (xargs :stobjs state
                  :mode :program))
   "~|Value of term-evisc-tuple: ~x0~|"
   (f-get-global 'term-evisc-tuple state)))

(defttag t) ; needed for :skip-checks t

(defattach (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)
ACL2 !>(defconst *foo6* '(a b c))

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)
ACL2 !>

Note that (as of this writing) the macro observation expands to a call of a :program-mode function. Thus, the trick shown above involving :skip-checks allows the use of :program-mode functions; for example, you can print with fmt.

See community book books/misc/defattach-bang.lisp for a variant of defattach that uses ec-call to avoid issues of guard verification.

Also see initialize-event-user, which discusses the handling of state globals by that utility as well as by finalize-event-user.