Major Section: ACL2 Documentation
ACL2 provides a trace utility, trace$, with corresponding reverse
operation untrace$. These can be used without any dependence on the
underlying Lisp utility, and are the tracing utilities of choice in ACL2;
see trace$ and see untrace$.
However, for advanced users we note that the underlying host Lisp may also
provide a trace utility, trace, and corresponding untrace. Moreover,
these have been modified in the case that the host Lisp is GCL, Allegro CL,
or CCL (OpenMCL), to provide limited support for :entry, :exit, and
perhaps :cond keywords, to hide certain large data structures (world,
enabled structure, rewrite constant), and to trace executable counterparts.
See source files *-trace.lisp. For the above Lisps, you can invoke the
original trace and untrace by invoking old-trace and
old-untrace, respectively, in raw Lisp rather than in the normal ACL2
loop.
