Major Section: OTHER
Examples: (time$ (foo 3 4)) (time$ (mini-proveall)) (defun bar (x) (time$ (f x)))where
General Form: (time$ form)
formis processed as usual except that the host Common Lisp times its evaluation.
(time$ x) equals
x. However, its evaluation produces
timing output, via the
time utility in the host Common Lisp.
(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
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.