trace the indicated functions
Major Section:  TRACE

(trace$ foo bar)

General Form: (trace$ fn1 fn2 ... fnk)

where the fni are defined or even constrained functions.

see untrace$ for how to undo the effect of trace$.

Basically, trace$ calls on the underlying Lisp to trace the specified functions as well as their executable-counterparts. However, for GCL and Allegro CL the underlying Lisp trace routines are modified before an image is saved in order to hide the ACL2 world and other large data structures and provide slightly prettier output.

Recursive calls of executable-counterpart functions will not generally be traced.

Output from trace$ normally goes to the screen, i.e., standard-co. But it can be redirected to a file; see open-trace-file.

Also see wet (``with-error-trace'') for a different way that ACL2 takes advantage of the underlying Lisp, namely to provide a backtrace when there is an error.

Note that from a logical perspective all trace printing is a fiction. For a related fiction, see cw. Trace$ returns nil