TIME$

time a form
Major Section:  OTHER

Examples:
(time$ (foo 3 4))
(time$ (mini-proveall))
(defun bar (x) (time$ (f x)))

General Form: (time$ form)

where 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.