Major Section: OTHER
Examples: (time$ (foo 3 4)) (time$ (mini-proveall)) (defun bar (x) (time$ (f x)))whereGeneral Form: (time$ form)
form is processed as usual except that the host Common Lisp times
its evaluation.
Semantically, (time$ x) equals x. However, its evaluation produces
timing output, via the time utility in the host Common Lisp.
Notes:
(1) Common Lisp specifies that the time utility prints to ``trace
output.'' If you have opened a trace file (see open-trace-file), then
you can expect to find the time$ output there. You can probably arrange
for the time$ output to go to the terminal instead, say by using a
suitable form in raw Lisp, for example:
(let ((*trace-output* *terminal-io*)) (time <form>)).
(2) In some Common Lisp implementations, for example CCL (OpenMCL), you may
see that the form being timed is a call of the ACL2 evaluator function
ev-rec. This is normal.