Major Section: ACL2 Documentation
ACL2 provides utilities that rely on the underlying Lisp image to trace functions. There are two interfaces to the underlying lisp trace:
untrace$call the underlying Lisp's
untrace, respectively. See trace$ and see untrace$.
wetfor short, provides a backtrace showing function calls that lead to an error. See wet.
wet turns off all tracing (i.e., executes Lisp
than temporarily doing some tracing under-the-hood in the evaluation of the
form supplied to it.
2. The underlying Lisp
untrace utilities have been modified
for GCL and Allegro CL to trace the executable counterparts. Other Lisps may
give unsatisfying results. For GCL and Allegro CL, you can invoke the
untrace by exiting the ACL2 loop and invoking
3. Trace output for
untrace$ can be redirected to a
file. See open-trace-file and see close-trace-file. However, the backtrace
wet always goes to