User-supplied code to initiate events
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
As with finalize-event-user, you attach your own function of
(defattach-system 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,
(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-system initialize-event-user my-init) (defattach-system 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 !>