WET

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


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 not in the main Lisp package appear in the backtrace. (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, other than any tracing it may do in support of creating its backtrace. 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. If no backtrace is produced then wet returns the value returned by evaluating its form, as an error triple (mv error-p value state). The details of just what value is are not particularly important, 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.