• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
      • With-output
      • Summary
      • Set-inhibit-output-lst
      • Set-gag-mode
      • Goal-spec
      • Set-warnings-as-errors
      • Saving-event-data
      • Pso
      • Finalize-event-user
      • Set-inhibit-er
      • Checkpoint-list
      • Set-inhibit-warnings
      • Get-event-data
      • Set-inhibited-summary-types
      • Set-print-clause-ids
      • Set-let*-abstractionp
      • Gag-mode
      • Initialize-event-user
      • Set-raw-proof-format
      • Checkpoint-list-pretty
      • Psof
      • Set-raw-warning-format
      • Toggle-inhibit-warning
      • Toggle-inhibit-er
      • Warnings
      • Show-checkpoint-list
      • Wof
      • Psog
      • Checkpoint-info-list
      • Pso!
      • Toggle-inhibit-warning!
      • Set-duplicate-keys-action!
      • Toggle-inhibit-er!
      • Set-inhibit-warnings!
      • Set-inhibit-er!
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Output-controls

Initialize-event-user

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 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-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, 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-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 !>