Major Section: ACL2-BUILT-INS
(time$ x ...) equals
x. However, its evaluation may
write timing output to the trace output (which is usually the terminal), as
explained further below.
Examples: ; Basic examples: (time$ (foo 3 4)) (time$ (mini-proveall)) (defun bar (x) (time$ (f x))) ; Custom examples, which use a custom timing message rather than a built-in ; message from Lisp: ; Report only if real time is at least 1/2 second (two equivalent forms). (time$ (foo) :mintime 1/2) (time$ (foo) :real-mintime 1/2) ; Report only if allocation is at least 1000 bytes (and if the Lisp supports ; :minalloc). (time$ (foo) :minalloc 1000) ; Report only if real time is at least 1/2 second and (if the Lisp supports ; :minalloc) allocation is at least 931 bytes. (time$ (foo) :real-mintime 1/2 :minalloc 931) ; Print "Hello Moon, Goodbye World" instead of any timing data. (time$ (foo) :msg "Hello ~s0, ~s1 World." :args (list "Moon" "Goodbye")) ; Print default custom timing message (same as omitting :mintime 0): (time$ (foo) :mintime 0) ; Print supplied custom timing message. (let ((bar ...)) (time$ (foo) :msg "The execution of ~xf took ~st seconds of real ~ time and ~sc seconds of run time (cpu time), and ~ allocated ~sa bytes. In an unrelated note, bar ~ currently has the value ~x0.~%" :args (list bar))) General Forms: (time$ form) (time$ form ; arguments below are optional :real-mintime <rational number of seconds> :run-mintime <rational number of seconds> :minalloc <number of bytes> :msg <fmt string> :args <list of arguments for msg> ) ; Note: :real-mintime can be replaced by :mintimewhere
formis processed as usual except that the host Common Lisp times its evaluation.
The simplest form is
(time$ x), which will call the
time utility in
the underlying Lisp, and will print a small default message. If you want to
see a message printed by the host Lisp, use
(time$ x :mintime nil)
instead, which may provide detailed, implementation-specific data such as the
amounts of time spent in user and system mode, the gc time, the number of
page faults encountered, and so on. Of you can create a custom message,
configured using the
Time$ can also
be made to report timing information only conditionally: the
:real-mintime (or equivalently,
:minalloc arguments can be used to avoid reporting timing information for
computations that take a small amount of time (perhaps as might be expected
in ordinary cases), but to draw the user's attention to computations that
take longer or allocate more memory than expected.
We next document the keyword arguments in some detail.
:run-mintimecan be used to specify a minimum time threshold for time reporting. That is, no timing information will be printed if the execution of
formtakes less than the specified number of seconds of real (total) time or run (cpu) time, respectively. Note that rational numbers like 1/2 may be used to specify a fractional amount of seconds. It is an error to specify both
:real-mintimeand its synonym,
:minallocis not supported on all Lisps. When it is not supported, it is ignored. But on supported Lisps,
:minalloccan be used to specify a minimum memory allocation threshold. If
formresults in fewer than this many bytes being allocated, then no timing information will be reported.
:msg, when provided, should be a string accepted by the
fmtfamily of functions (see fmt), and it may refer to the elements of
:argsby their positions, just as for
The following directives allow you to report timing information using the
:msg string. The examples at the top of this documentation topic
illustrate the use of these directives.
~xf-- the form that was executed
~sa-- the amount of memory allocated, in bytes (in supported Lisps)
~st-- the real time taken, in seconds
~sc-- the run time (cpu time) taken, in seconds
We turn now to an example that illustrates how
time$ can be called in
function bodies. Consider the following definition of the Fibonacci
function, followed by the definition of a function that times
k calls of
(defun fib (n) (if (zp n) 1 (if (= n 1) 1 (+ (fib (- n 1)) (fib (- n 2)))))) (defun time-fib (k) (if (zp k) nil (prog2$ (time$ (fib k) :mintime 1/2 :msg "(fib ~x0) took ~st seconds, ~sa bytes allocated.~%" :args (list k)) (time-fib (1- k)))))The following log shows a sample execution of the function defined just above.
ACL2 !>(time-fib 36) (fib 36) took 3.19 seconds, 1280 bytes allocated. (fib 35) took 1.97 seconds, 1280 bytes allocated. (fib 34) took 1.21 seconds, 1280 bytes allocated. (fib 33) took 0.75 seconds, 1280 bytes allocated. NIL ACL2 !>
(1) Common Lisp specifies that the
time utility prints to ``trace
time$ follows this convention. Thus, if you have opened a
trace file (see open-trace-file), then you can expect to find the
time$ output there.
(2) Unless the
:msg argument is supplied, an explicit call of
in the top-level loop will show that the form being timed is a call of the
ACL2 evaluator function
ev-rec. This is normal; the curious are invited,
at their own risk, to see return-last for an explanation.