Major Section: SWITCHES-PARAMETERS-AND-MODES
This utility is intended for system hackers, not standard ACL2 users.
See finalize-event-user to see how to supply code to be run at the end of
events. We assume familiarity with finalize-event-user; here we
focus on how to supply code for the beginning as well as the end of events.
As with finalize-event-user, you attach your own function of argument
list (ctx qbody state) to initialize-event-user.
(See finalize-event-user for discussion of ctx and body.) The
attachment should return state and have a trivial guard,
requiring (implicitly) only that state satisfies state-p unless you
use trust tags to avoid that requirement. For example:
(defattach initialize-event-user initialize-event-user-test)
Why would you want to do this? Presumably you are building a system on top
of ACL2 and you want to track your own data. For example, suppose you want
to save the time in some state global variable, my-time. You could
do the following.
(defun my-init (ctx body state)
(declare (xargs :stobjs state
:guard-hints
(("Goal" :in-theory (enable read-run-time))))
(ignore ctx body))
(mv-let (seconds state)
(read-run-time state)
(f-put-global 'start-time seconds state)))
(defun my-final (ctx body state)
(declare (xargs :stobjs state
:guard-hints
(("Goal" :in-theory (enable read-run-time))))
(ignore ctx body))
(mv-let (seconds state)
(read-run-time state)
(prog2$ (if (boundp-global 'start-time state)
(cw "Time: ~x0 seconds~%"
(- seconds (fix (@ start-time))))
(cw "BIG SURPRISE!~%"))
(f-put-global 'end-time seconds state))))
(defattach initialize-event-user my-init)
(defattach finalize-event-user my-final)
Here is an abbreviated log, showing the time being printed at the end.
ACL2 !>(thm (equal (append (append x y) x y x y x y x y)
(append x y x y x y x y x y)))
*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.
....
ACL2 Error in ( THM ...): See :DOC failure.
******** FAILED ********
Time: 869/100 seconds
ACL2 !>
