Trace
Tracing functions in ACL2
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 evaluation). 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.
Subtopics
- Trace$
- Trace function evaluations
- Wet
- Evaluate a form and print subsequent error trace
- Trace!
- Trace the indicated functions after creating an active trust tag
- Break-on-error
- Break when encountering a hard or soft error caused by ACL2
- Set-trace-evisc-tuple
- Set the trace evisc tuple
- Untrace$
- Untrace functions
- Open-trace-file
- Redirect trace output to a file
- Open-trace-file!
- Redirect trace output to a file, even within events
- Close-trace-file
- Stop redirecting trace output to a file
