WET

evaluate a form and print subsequent error trace 
Major Section:  TRACE

NOTE: This feature is onlyh available if you are using GCL, Allegro CL, or CLISP. 

Examples:
(wet (bar 3))            ; evaluate (bar 3) and print backtrace upon error
(wet (bar 3) :fns (f g)) ; as above but only include calls of f, g


General Forms:
(wet form)
(wet form :fns  (fn1 fn2 ... fnk))
(wet form :omit (fn1 fn2 ... fnk))
where form is an arbitrary ACL2 form and the fni are function symbols whose calls are to appear in the backtrace if the evaluation of form aborts. If fns are nil or not supplied, then calls of all functions appear in the backtrace, with the exception of built-in functions that are either in the main Lisp package or are in :program mode. (In particular, all user-defined functions appear.) The above description is modified if omit is supplied, in which case calls of the specified function symbols are removed from the backtrace.

The following example illustrates the use of wet, which stands for ``with-error-trace''. We omit uninteresting output from this example. 

ACL2 !>(defun foo (x) (car x))
 ...
 FOO
ACL2 !>(defun bar (x) (foo x))
 ...
 BAR
ACL2 !>(bar 3)



ACL2 Error in TOP-LEVEL:  The guard for the function symbol CAR, which
is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the
call (CAR 3).  To see a trace of calls leading up to this violation,
execute (wet <form>) where <form> is the form you submitted to the
ACL2 loop.  See :DOC wet for how to get an error backtrace.


ACL2 !>(wet (bar 3))



ACL2 Error in WITH-ERROR-TRACE:  The guard for the function symbol
CAR, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments
in the call (CAR 3).  (Backtrace is below.)


1> (ACL2_*1*_ACL2::BAR 3)
  2> (ACL2_*1*_ACL2::FOO 3)


ACL2 !>(wet (bar 3) :fns (foo))





ACL2 Error in WITH-ERROR-TRACE:  The guard for the function symbol
CAR, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments
in the call (CAR 3).  (Backtrace is below.)


1> (ACL2_*1*_ACL2::FOO 3)


ACL2 !>
Notice that because guards were not verified, the so-called executable-counterpart functions are evaluated for foo and bar. These can be identified with package names beginning with the string "ACL2_*1*_".

See trace$ for a general tracing utility.

NOTES:

1. Recursive calls of executable-counterpart functions will not generally be traced.

2. In the (probably rare) event of a hard Lisp error, you will have to exit the Lisp break before seeing the backtrace.

3. Wet always untraces all functions before it installs the traces it needs, and it leaves all functions untraced when it completes. If existing functions were traced then you will need to re-execute trace$ in order to re-install tracing on those functions after wet is called on any form.

4. Wet returns an error triple (mv error-p value state), where value is a print representation of the value returned by the form given to wet. Presumably value is not particularly important anyhow, as the intended use of wet is for the case that an error occurred in evaluation of a form.

5. As mentioned above, functions in the main Lisp package (i.e., those built into Common Lisp) will not be traced be wet.