This is documentation for ACL2 Version 3.0
Copyright (C) 2006  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

UNTRACE$    untrace functions

     Examples:
     (untrace$)         ; untrace all traced functions
     (untrace$ foo bar) ; untrace foo and bar

     General Forms:
     (untrace$)                 ; untrace all traced functions
     (untrace$ fn1 fn2 ... fnk) ; untrace the indicated functions

where the fni are defined or even constrained functions.

Untrace$ undoes the effect of trace$.  See TRACE$.  Untrace
returns nil

WET    evaluate a form and print subsequent error 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) nil)        ; as above, but avoid hiding the structure of bar
     (wet (bar 3) (evisc-tuple 3 5 nil nil))
                              ; as above, but hiding the structure of bar up to
                              ; level 3 and length 5
     (wet (bar 3) :fns (f g)) ; as above but only include calls of f, g

     General Forms (all but the first argument may be omitted):
     (wet form
          evisc-tuple ; optional, and evaluated
          :fns  (f1 f2 ... fk)
          :omit (g1 g2 ... gk))

where form is an arbitrary ACL2 form and the fi are function symbols
whose calls are to appear in the backtrace if the evaluation of form
aborts.  Generally, wet will hide parts of large structures that it
prints out, but this can be avoided by supplying a value of nil for
evisc-tuple.

More generally, the evisc-tuple argument, which is evaluated, can be
supplied to specify the print-level and print-length for the resulting
backtrace; see LD-EVISC-TUPLE.

If the value of :fns is 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 by wet.

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

With-error-trace is the same as wet; see WET.