WET

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

The acronym ``wet'' stands for ``with-error-trace''. Wet provides a convenient way to obtain a backtrace when evaluation causes a guard violation or other error.

The basic idea is that (wet form) evaluates form and, if there is an error, shows a backtrace of calls that led to that error. Note however that by default only calls of user-defined (not built-in) functions ``supporting'' form in the following sense will show up in the backtrace: those that occur in the macroexpansion of form or (recursively) support any of those functions. So for example, since (make-event form) macroexpands to (make-event-fn (quote form) ...), calls of functions occurring in form will likely not show up in the backtrace by default. The option :fns all overrides this default, with potential loss of speed; more on this below.

The following example explains the use of wet. First, submit the following three definitions: 

(defun foo (x) (declare (xargs :guard (consp x))) (car x))
(defun bar (x) (foo (cdr x)))
(defun g (x) (bar (cdr x)))
Now imagine you have obtained the following guard violation: 
ACL2 !>(g '(3 4))


ACL2 Error in TOP-LEVEL:  The guard for the function call (FOO X),
which is (CONSP X), is violated by the arguments in the call (FOO NIL).
To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.  See
:DOC set-guard-checking for information about suppressing this check
with (set-guard-checking :none), as recommended for new users.

ACL2 !>
With wet, you can get a backtrace of user-defined functions. The package prefixes shown below, ACL2_*1*_, indicate that the executable (logical) counterparts of the corresponding raw Lisp functions are being called; see guard. Don't forget to start with (include-book "misc/wet" :dir :system). 
ACL2 !>(wet (g '(3 4)))
; Fast loading /projects/acl2/devel/books/misc/wet.fasl

TTAG NOTE: Adding ttag :TRACE! from the top level loop.


ACL2 Error in WET:  The guard for the function call (FOO X), which
is (CONSP X), is violated by the arguments in the call (FOO NIL). 
To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.  See
:DOC set-guard-checking for information about suppressing this check
with (set-guard-checking :none), as recommended for new users.


Backtrace stack:
----------------
1. (ACL2_*1*_ACL2::FOO NIL)
2. (ACL2_*1*_ACL2::BAR (4))
3. (ACL2_*1*_ACL2::G (3 4))

ACL2 !>
By default, large structures are hidden during the printing of the backtrace stack. But you can supply a value for keyword argument :evisc-tuple to modify the printing: nil to avoid hiding, else a suitable evisc-tuple, as shown below (see evisc-tuple). 
ACL2 !>(wet (g '(3 4)) :evisc-tuple (evisc-tuple 1 1 nil nil))
; Fast loading /projects/acl2/devel/books/misc/wet.fasl

TTAG NOTE: Adding ttag :TRACE! from the top level loop.


ACL2 Error in WET:  The guard for the function call (FOO X), which
is (CONSP X), is violated by the arguments in the call (FOO NIL). 
To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.  See
:DOC set-guard-checking for information about suppressing this check
with (set-guard-checking :none), as recommended for new users.


Backtrace stack:
----------------
1. (ACL2_*1*_ACL2::FOO ...)
2. (ACL2_*1*_ACL2::BAR ...)
3. (ACL2_*1*_ACL2::G ...)

ACL2 !>
For a backtrace as a data object, evaluate the form (@ wet-stack). But note that this object may not be a legal ACL2 value, for example because of the ``*1*'' symbols shown above. 

General Form:
(wet form           ; an arbitrary form
     :book bk-form  ; optional, not evaluated
     ;;; the rest are optional and evaluated:
     :evisc-tuple e ; an evisc-tuple
     :fns fns       ; :all, or a list of functions to show in a backtrace
     :compile c     ; :same, t, or nil; default :same (nil if :fns supplied)

Form is evaluated. If there is an error, a backtrace stack is printed to the standard output (*standard-co*), containing (by default) the user-defined function calls made before the error. Such printing is controlled by the :evisc-tuple if supplied; otherwise, hiding of large structures will occur. (Technical detail: by default the global abbrev-evisc-tuple is used, if bound; see set-evisc-tuple.

The :fns option. As mentioned above, by default the wet backtrace shows user-defined functions that syntactically ``support'' the form being evaluated. This default can be overridden by supplying an explicit list, fns, of functions, using option :fns fns; these will then be the functions whose calls are eligible for inclusion in the backtrace. The special value :fns :all will allow all user-defined function calls in the backtrace. This value can be useful when using oracle-apply, for example, since the function being applied isn't typically included as a syntactic supporter of the form being evaluated.

The :compile option. Wet uses the trace$ utility to modify the definitions of affected functions so that they can record information for the backtrace. As described above, these affected functions are those that syntactically ``support'' the form unless specified by the :fns option. As is the case for trace$ -- see trace$ -- the new definitions of these affected functions may or may not be compiled. For trace$ and for wet, the default is to compile the new definition if and only if the original definition was compiled, except: For wet, if option :fns :all is provided, then the default is not to compile the affected definitions. And for trace$ and wet, the :compile option overrides the default, to specify what will be compiled: value :same to compile each affected function if and only if its original definition was compiled, value t to compile all affected functions, and value nil to skip compilation.

The :book option. Wet actually works by temporarily including a community book, 

(include-book "misc/wet" :dir :system)
and then passing its arguments to macro wet!, defined in that book. The keyword argument :book allows you to specify a different book that defines a macro wet! to which to pass its arguments. If the value of :book is a string, then the book named by that string is temporarily included using include-book: (include-book "bk"). Otherwise :book should be a list of arguments, to be provided (unevaluated) to include-book, for example ("my-wet" :dir :my-utils). Thus you can experiment by copying community book books/misc/wet.lisp to your own directory and making modifications to the copy. If you make changes, we invite you to share them with the ACL2 community (see books). Note that you can also supply :book nil, in which case the definition of wet! in your current session will be used without including a book.

Also see trace$ for a general tracing utility. As mentioned above, wet is implemented using trace$. Wet actually first applies untrace$; upon completion, wet then applies trace$ to re-trace any functions that it had untraced, using their original trace specs.