Major Section: MISCELLANEOUS
The ACL2 system provides utilities that deal with elapsed time. The most visible of these is in the time summaries printed when completing evaluation of events. For others, see with-prover-time-limit, see read-run-time, see time-tracker, see time-tracker-tau, and see pstack.
By default, these utilities all use an underlying notion of run time provided
by the host Common Lisp implementation: specifically, Common Lisp function
get-internal-run-time. However, Common Lisp also provides function
get-internal-run-time, which returns the real time (wall clock time).
While the latter is specified to measure elapsed time, the former is left to
the implementation, which might well only measure time spent in the Lisp
process. Consider the following example, which is a bit arcane but basically
sleeps for 2 seconds.
(defttag t) ; to allow sys-call
(make-event
(prog2$ (sys-call "sleep" '("2"))
(value '(value-triple nil))))
A typical time summary might be as follows, drastically under-reporting the
elapsed time.
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)However, you can instruct ACL2 to switch to using elapsed time (run time), in summaries and elsewhere, by evaluating the following form.
(assign get-internal-time-as-realtime t)To return to using runtime:
(assign get-internal-time-as-realtime nil)While the above example is rather silly, the issue becomes significant in time summaries for proofs that call out to external tools (see sys-call and see clause-processor).
Note that a function get-internal-time is defined in raw Lisp but is not
available inside the ACL2 loop. However, the expression
(read-run-time state) provides an interface to this function that is
available inside the ACL2 loop; see read-run-time.
We are open to changing the default to elapsed wall-clock time (realtime), and may do so in future ACL2 releases.
