This is documentation for ACL2 Version 3.3
Copyright (C) 2007  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.

OPEN-TRACE-FILE    redirect trace output to a file

     Example:
     (open-trace-file "foo") ; trace output will go to file foo

     General Form:
     (open-trace-file filename) ; trace output will go to file filename

Output from trace$ normally goes to the screen, i.e., standard-co.  But
it can be redirected to a file as shown above.  See
CLOSE-TRACE-FILE for how to send trace output back to the screen.

Note that the backtrace printed by wet always goes to standard-co, even
after the use of open-trace-file.

TRACE!    trace the indicated functions after creating an active trust tag

     Example:
     (trace! (fact :entry (list 'tracing-mark (car arglist))))

     General Form:
     (trace! fn1 fn2 ... fnk)

where the fni are suitable arguments to the underlying Lisp trace.

Trace! is a version of trace$ that avoids the need for an
already-active trust tag (or "ttag"; see DEFTTAG), as explained
below.  If each fni is a symbol, you may prefer simply to use trace$.
Alternatively, you can use trace$ in raw Lisp, though evaluating forms
in raw Lisp should be viewed as a hack that invalidates any logical
claims made about that ACL2 session.

See UNTRACE$ for how to undo the effect of trace!.

Consider the following example, essentially suggested by Peter
Dillinger:

     (value-triple (trace$ (bar :entry (defun foo () 17))))

Clearly, a trace performed of bar can change the definition of an
existing defined function foo; and this can render ACL2 unsound!

Thus, if trace$ is given any argument that is not a symbol, then there
must be an active trust tag (see DEFTTAG).  A user who is
hacking may prefer to use a command that takes care of this issue
automatically, and trace!  is such a command.  The evaluation of a
trace! causes temporary creation of an active trust tag, :trace!,
followed by the corresponding trace$ form.  The trust tag will
disappear when the call to trace! completes.  Even though trace! will
remove its temporary ttag, it will still print a "TTAG NOTE", which
indicates that the session is suspect.  See DEFTTAG and see
TTAGS-SEEN for further remarks on this issue.

TRACE$    trace the indicated functions

     Example:
     (trace$ foo bar)

     General Form:
     (trace$ fn1 fn2 ... fnk)

where the fni are defined or even constrained functions.  More
generally, the fni may be any arguments allowed by the underlying Lisp
trace, but if any fni is not a symbol then you will probably want to use
trace! instead.

See UNTRACE$ for how to undo the effect of trace$.

Basically, trace$ calls on the underlying Lisp to trace the specified
functions as well as their executable-counterparts.  However, for GCL,
Allegro CL, and OpenMCL, the underlying Lisp trace routines are modified
before an image is saved in order to hide the ACL2 world and other
large data structures and provide slightly prettier output.

Recursive calls of functions whose guards have not been verified will
not generally be traced.  If you want to see traces for corresponding
evaluations in raw Lisp, which will generally show recursive calls
(except, in some Lisp implementations, for compiled tail recursive
functions), then you can quit into raw Lisp (:q) and execute your form
there.  Alternatively, you can avoid executable-counterpart functions
by using :set-raw-mode to enter a raw Lisp version of the ACL2 loop;
see SET-RAW-MODE and see SET-RAW-MODE-ON!.

Output from trace$ normally goes to the screen, i.e., standard-co.  But
it can be redirected to a file; see OPEN-TRACE-FILE.

Also see WET ("with-error-trace") for a different way that ACL2
takes advantage of the underlying Lisp, namely to provide a backtrace
when there is an error.

Note that from a logical perspective all trace printing is a fiction.
For a related fiction, see CW.  Trace$ returns nil.

The following example will give an idea of the options available other
than just (trace$ fn1 fn2 ... fnk).  It works about as shown in Allegro
CL and GCL, but in OpenMCL the recursive calls are omitted unless you
escape into raw Lisp and redefine fact with (declare (notinline fact)).

     ACL2 !>(defun fact (n)
              (declare (xargs :guard (natp n) :mode :program))
              (if (zp n)
                  1
                (* n (fact (1- n)))))

     Summary
     Form:  ( DEFUN FACT ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 !>(trace$ (fact :entry (car arglist) :exit values))
     NIL
     ACL2 !>(fact 5)
     1> (ACL2_*1*_ACL2::FACT . 5)
       2> (FACT . 5)
         3> (FACT . 4)
           4> (FACT . 3)
             5> (FACT . 2)
               6> (FACT . 1)
                 7> (FACT . 0)
                 <7 (FACT 1)
               <6 (FACT 1)
             <5 (FACT 2)
           <4 (FACT 6)
         <3 (FACT 24)
       <2 (FACT 120)
     <1 (ACL2_*1*_ACL2::FACT 120)
     120
     ACL2 !>

Here is another example.

     ACL2 !>(defun fact2 (n acc)
              (declare (xargs :guard (and (natp n) (natp acc))))
              (if (zp n)
                  (mv acc (* 2 acc))
                (fact2 (1- n) (* n acc))))

     The admission of FACT2 is trivial, using the relation O< (which is
     known to be well-founded on the domain recognized by O-P) and the measure
     (ACL2-COUNT N).  We observe that the type of FACT2 is described by
     the theorem (AND (CONSP (FACT2 N ACC)) (TRUE-LISTP (FACT2 N ACC))).
     We used primitive type reasoning.

     (FACT2 * *) => (MV * *).

     The guard conjecture for FACT2 is trivial to prove.  FACT2 is compliant
     with Common Lisp.

     Summary
     Form:  ( DEFUN FACT2 ...)
     Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
             (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
             (:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT2
     ACL2 !>(trace$ (fact2 :entry (list 'my-entry (car arglist))
                           :exit (list 'my-second-value (cadr values))))
     NIL
     ACL2 !>(fact2 6 1)

       1> (ACL2_*1*_ACL2::FACT2 MY-ENTRY 6)>
         2> (FACT2 MY-ENTRY 6)>
           3> (FACT2 MY-ENTRY 5)>
             4> (FACT2 MY-ENTRY 4)>
               5> (FACT2 MY-ENTRY 3)>
                 6> (FACT2 MY-ENTRY 2)>
                   7> (FACT2 MY-ENTRY 1)>
                     8> (FACT2 MY-ENTRY 0)>
                     <8 (FACT2 MY-SECOND-VALUE 1440)>
                   <7 (FACT2 MY-SECOND-VALUE 1440)>
                 <6 (FACT2 MY-SECOND-VALUE 1440)>
               <5 (FACT2 MY-SECOND-VALUE 1440)>
             <4 (FACT2 MY-SECOND-VALUE 1440)>
           <3 (FACT2 MY-SECOND-VALUE 1440)>
         <2 (FACT2 MY-SECOND-VALUE 1440)>
       <1 (ACL2_*1*_ACL2::FACT2 MY-SECOND-VALUE 1440)>
     (720 1440)
     ACL2 !>(trace$ (fact2 :entry (list 'my-args-reversed
                                        (list (cadr arglist) (car arglist)))
                           :exit (list 'values-reversed
                                       (cadr values) (car values))))
     NIL
     ACL2 !>(fact2 6 1)

       1> (ACL2_*1*_ACL2::FACT2 MY-ARGS-REVERSED (1 6))>
         2> (FACT2 MY-ARGS-REVERSED (1 6))>
           3> (FACT2 MY-ARGS-REVERSED (6 5))>
             4> (FACT2 MY-ARGS-REVERSED (30 4))>
               5> (FACT2 MY-ARGS-REVERSED (120 3))>
                 6> (FACT2 MY-ARGS-REVERSED (360 2))>
                   7> (FACT2 MY-ARGS-REVERSED (720 1))>
                     8> (FACT2 MY-ARGS-REVERSED (720 0))>
                     <8 (FACT2 VALUES-REVERSED 1440 720)>
                   <7 (FACT2 VALUES-REVERSED 1440 720)>
                 <6 (FACT2 VALUES-REVERSED 1440 720)>
               <5 (FACT2 VALUES-REVERSED 1440 720)>
             <4 (FACT2 VALUES-REVERSED 1440 720)>
           <3 (FACT2 VALUES-REVERSED 1440 720)>
         <2 (FACT2 VALUES-REVERSED 1440 720)>
       <1 (ACL2_*1*_ACL2::FACT2 VALUES-REVERSED 1440 720)>
     (720 1440)
     ACL2 !>

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 only available if you are using GCL, Allegro CL,
OpenMCL, 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.