Time an evaluation
Note: Some of the functionality below is available only for certain host Common Lisp implementations.
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 :mintime
The simplest form is
We next document the keyword arguments in some detail.
:real-mintime(or :mintime) and :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, :mintime.
: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.
The following directives allow you to report timing information using the
~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
The following apply only when the host Lisp is GCL. The two system times will likely be
nilunless the GCL version is 2.6.10 or later. Note the upper-case characters for child times.
~sC— the child run time (cpu time) taken, in seconds
~ss— the system time taken, in seconds ~sS— the child system time taken, in seconds
We turn now to an example that illustrates how
(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
(2) Unless the