Major Section: OTHER
(time$ x ...) equals
x. However, its evaluation may
write timing output to the trace output (which is usually the terminal), as
explained further below.
; 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. (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 :mintime
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. The particular message you see varies from Lisp to
Lisp, and may contain 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.
Without any keyword arguments,
time$ often prints a rather verbose
message. However, if
time$ is provided with at least one keyword
argument, then it will display a custom message, either provided by ACL2 or
configured using the
Time$ can also
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))))))The following log shows a sample execution of the function defined just above.
(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)))))
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) You may see that the form being timed is a call of the ACL2 evaluator
ev-rec. This is normal.