tracing functions in ACL2
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.

Some Related Topics