TRACE

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:

o Macros trace$ and untrace$ call the underlying Lisp's trace and untrace, respectively. See trace$ and see untrace$.

o Macro with-error-trace, or wet for short, provides a backtrace showing function calls that lead to an error. See wet.

1. wet turns off all tracing (i.e., executes Lisp (untrace)) other than temporarily doing some tracing under-the-hood in the evaluation of the form supplied to it.

2. The underlying Lisp trace and 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 original trace and untrace by exiting the ACL2 loop and invoking old-trace and old-untrace, respectively..

3. Trace output for trace$ and untrace$ can be redirected to a file. See open-trace-file and see close-trace-file. However, the backtrace printed by wet always goes to standard-co.

• CLOSE-TRACE-FILE -- stop redirecting trace output to a file

• OPEN-TRACE-FILE -- redirect trace output to a file

• TRACE$ -- trace the indicated functions

• UNTRACE$ -- untrace functions

• WET -- evaluate a form and print subsequent error trace

• WITH-ERROR-TRACE -- evaluate a form and print subsequent error trace