Runtime vs. realtime in ACL2 timings
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, the Common Lisp
(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 (real 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)
Note that a function
We are open to changing the default to elapsed wall-clock time (realtime), and may do so in future ACL2 releases.
Implementation note (GCL only): If the host Lisp is Gnu Common Lisp, then