This is documentation for ACL2 Version 6.0
Copyright (C) 2012  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of Version 2 of the GNU General Public License as
published by the Free Software Foundation.

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.

SET-PROVER-STEP-LIMIT    sets the step-limit used by the ACL2 prover at the top level only

This event provides a way to limit the number of so-called "prover
steps" permitted for an event.  See WITH-PROVER-STEP-LIMIT for
a way to specify the limit on prover steps for a single event, rather
than globally (and without the restriction mentioned above, pertaining
to the top level).  For a related utility based on time instead of
prover steps, see WITH-PROVER-TIME-LIMIT.  For examples of how
step limits work, see the community book
books/misc/misc2/step-limits.lisp.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

     Example Forms:
     (set-prover-step-limit *default-step-limit*) ; no limit on prover steps
     (set-prover-step-limit nil)   ; abbreviation for the form just above
     (set-prover-step-limit 10000) ; allow at most 10,000 prover steps per event

     General Form:
     (set-prover-step-limit expr)

where expr evaluates either to nil or else to a natural number not
exceeding the value of *default-step-limit*.  If that value is nil or
the value of *default-step-limit*, then no default limit is placed on
the number of prover "steps" (see below) during processing of an event.
Otherwise, that value is the maximum number of prover steps permitted
before an error occurs.

This event specifies the limit on the number of "steps" counted by the
ACL2 prover during processing of an event.  Currently, a step is
counted for each call of the system functions rewrite and
expand-abbreviations.  However, the steps counted may change in future
releases of ACL2, so users would probably be well served by avoiding
the assumption that only the above two calls are counted as prover
steps.

Depending on the computer you are using, you may have only (very
roughly) a half-hour of time before the number of prover steps exceeds
the maximum step-limit, which is one less than the value of
*default-step-limit*.  Note however the exception stated above: if the
"limit" is nil or is the value of *default-step-limit*, then no limit
is imposed.

The limit is relevant for every event, to calls of thm and
certify-book, and more generally, to any form that creates a "summary
context" to print the usual event summary.  The limit is also put in
force when entering the proof-checker.  Below, at the end of this
documentation topic, we explain in detail when a call of
set-prover-step-limit is in force: in brief, it applies to all forms
that are either at the top level or are inside the same summary
contexts.

Note that the limit applies to each event, not just "atomic" events.
Consider the following example.

     (set-prover-step-limit 500)

     (encapsulate
       ()
       (defthm lemma-1 ; takes 380 steps
         (equal (append (append x y) z) (append x y z))
         :rule-classes nil)
       (defthm lemma-2 ; would take 319 steps
         (equal (len (append x y)) (+ (len x) (len y)))
         :rule-classes nil))

The first defthm event, lemma-1 takes 380 steps (as of this writing),
as shown in the summary:

     Prover steps counted:  380
     LEMMA-1

The second defthm event, lemma-2, takes 319 steps (as of this writing)
when evaluated at the top level.  However, in the context above, 380
steps of the available 500 steps (from the set-prover-step-limit event
above) have already been taken under the above encapsulate event.
Thus, when the number of steps would exceed 120, the proof of lemma-2 is
aborted:

     ACL2 Error in STEP-LIMIT:  The prover step-limit, which is 120 in the
     current context, has been exceeded.  See :DOC set-prover-step-limit.

The summary for lemma-2 reflects that situation:

     Prover steps counted:  More than 120

The  summary for the encapsulate events then indicates that the
available steps for that event have also been exceeded:

     Prover steps counted:  More than 500

The discussion above applies to any event that contains other events,
hence applies similarly to progn events.

For those who use make-event, we note that prover steps in the
expansion phase similarly contribute to the total number of steps
counted.  For example, suppose that the limit is 500 prover steps as
above, and you submit (make-event EXPR), where 300 prover steps take
place during evaluation of EXPR, producing event EV.  Then evaluation
of EV will cause an error if it takes more than 200 prover steps.  This
observation actually can be used to count prover steps for sequences of
forms that are not all legal events (see EMBEDDED-EVENT-FORM),
such as calls of thm.  For example, a small built-in ACL2 test suite
that includes thm forms can be run by evaluating the form
(mini-proveall), and the steps can be counted as shown below.  (Here we
assume a fresh ACL2 session; an error would occur if first, we evaluate
the event (set-prover-step-limit 500) displayed above.)

     ACL2 !>(make-event (er-progn (mini-proveall) (value '(value-triple nil))))
     [[... output omitted here ...]]
     Summary
     Form:  ( MAKE-EVENT (ER-PROGN ...))
     Rules: NIL
     Warnings:  Double-rewrite, Equiv, Subsume and Non-rec
     Time:  0.38 seconds (prove: 0.04, print: 0.29, other: 0.05)
     Prover steps counted:  41090
      NIL
     ACL2 !>

Technical Remark.  For a call of mfc-rw or any mfc- function (see
EXTENDED-METAFUNCTIONS), the steps taken during that call are
forgotten when returning from that call.

Finally, we discuss in some detail with a set-prover-step-limit event is
in force: it applies to a subsequent form that is either at the top
level or at the same level as the set-prover-step-limit form, in the
following sense.  Let us say that a "summary context" is any context
for which the usual ACL2 summary will ultimately be printed (if summary
printing is not inhibited).  Every event -- a call of defun or defthm,
or more generally, every embedded event form (see
EMBEDDED-EVENT-FORM) -- establishes a summary context, as do certain
other top-level forms such as calls of thm and certify-book.  (But a
call of ld does not establish a summary context.)  Here, we consider
two forms to be at the same level if they are in the same summary
contexts.  Thus, if set-prover-step-limit is called at the top level,
then this call is not in force for events under a call of certify-book,
encapsulate, progn, make-event, or (more generally) under any form that
establishes a summary context.  Also, if set-prover-step-limit is
called inside a summary context, then it does not apply above that
summary context except, if it is not local to some event, at the very
top level.

SET-RAW-MODE    enter or exit "raw mode," a raw Lisp environment

Below we discuss raw-mode.  In brief: The simplest way to turn raw-mode
on is :SET-RAW-MODE-ON!, and to turn it off, :SET-RAW-MODE NIL.  Also
see SET-RAW-MODE-ON!.

ACL2 users often find its careful syntax checking to be helpful during
code development.  Sometimes it is even useful to do code development in
:logic mode, where ACL2 can be used to check termination of (mutually)
recursive functions, verify guards, or even prove properties of the
functions.

However, loading code using include-book is much slower than using
Common Lisp load in raw Lisp, and in this sense ACL2 can get in the way
of efficient execution.  Unfortunately, it is error-prone to use ACL2
sources (or their compilations) in raw Lisp, primarily because a number
of ACL2 primitives will not let you do so.  Perhaps you have seen this
error message when trying to do so:

     HARD ACL2 ERROR in ACL2-UNWIND-PROTECT:  Apparently you have tried
     to execute a form in raw Lisp that is only intended to be executed
     inside the ACL2 loop.

Even without this problem it is important to enter the ACL2 loop (see
LP), for example in order to set the cbd and (to get more
technical) the readtable.

ACL2 provides a "raw mode" for execution of raw Lisp forms.  In this
mode, include-book reduces essentially to a Common Lisp load.  More
generally, the ACL2 logical world is not routinely extended in raw mode
(some sneaky tricks are probably required to make that happen).  To
turn raw mode off or on:

     :set-raw-mode t   ; turn raw mode on
     :set-raw-mode nil ; turn raw mode off

The way you can tell that you are in raw mode is by looking at the
prompt (see DEFAULT-PRINT-PROMPT), which uses a capital "P"
(suggesting something like program mode, but more so).

     ACL2 P>

Typical benefits of raw mode are fast loading of source and compiled
files and the capability to hack arbitrary Common Lisp code in an
environment with the ACL2 sources loaded (and hence with ACL2
primitives available).  In addition, ACL2 hard errors will put you into
the Lisp debugger, rather than returning you to the ACL2 loop, and this
may be helpful for debugging; see HARD-ERROR and see
ILLEGAL, but also see BREAK-ON-ERROR.  However, it probably
is generally best to avoid raw mode unless these advantages seem
important.  We expect the main benefit of raw mode to be in deployment
of applications, where load time is much faster than the time required
for a full-blown include-book, although in certain cases the fast
loading of books and treatment of hard errors discussed above may be
useful during development.

Raw mode is also useful for those who want to build extensions of ACL2.
For example, the following form can be put into a certifiable book to
load an arbitrary Common Lisp source or compiled file.

     (progn (defttag my-application)
            (progn! (set-raw-mode t)
                    (load "some-file")))

Also see with-raw-mode defined in community book
books/hacking/hacker.lisp, see DEFTTAG, and see PROGN!.

Below are several disadvantages to raw mode.  These should discourage
users from using it for general code development, as :program mode is
generally preferable.

     -- Forms are in essence executed in raw Lisp.  Hence:
        -- Syntax checking is turned off; and
        -- Guard checking is completely disabled.
     -- Table events, including logic, are ignored, as are many
        other events, including defthm and comp.
     -- Soundness claims are weakened for any ACL2 session in which raw
        mode was ever entered; see DEFTTAG.
     -- The normal undoing mechanism (see UBT) is not supported.
     -- Unexpected behavior may occur when you return from raw-mode.
        For example, if you redefine a :logic mode function whose guards
        have not been verified, you will not see the change inside the
        ACL2 loop because there, the raw Common Lisp definition is only
        executed after guards have been verified; see GUARDS-AND-EVALUATION
        and see GUARD-EVALUATION-TABLE.

We conclude with some details.

_Printing results_.  The rules for printing results are unchanged for
raw mode, with one exception.  If the value to be printed would contain
any Lisp object that is not a legal ACL2 object, then the print routine
is used from the host Lisp, rather than the usual ACL2 printing
routine.  The following example illustrates the printing used when an
illegal ACL2 object needs to be printed.  Notice how that "command
conventions" are observed (see LD-POST-EVAL-PRINT); the "[Note"
occurs one space over in the second example, and no result is printed
in the third example.

     ACL2 P>(find-package "ACL2")
     [Note:  Printing non-ACL2 result.]
     #<The ACL2 package>
     ACL2 P>(mv nil (find-package "ACL2") state)
      [Note:  Printing non-ACL2 result.]
     #<The ACL2 package>
     ACL2 P>(mv t (find-package "ACL2") state)
     ACL2 P>(mv 3 (find-package "ACL2"))
     [Note:  Printing non-ACL2 result.]
     (3 #<The ACL2 package>)
     ACL2 P>

If you have trouble with large structures being printed out, you might
want to execute appropriate Common Lisp forms in raw mode, for example,
(setq *print-length* 5) and (setq *print-level* 5).

_Include-book_.  The events add-include-book-dir and
delete-include-book-dir have been designed to work with raw mode.
However, if you enter raw mode and then evaluate such forms, then the
effects of these forms will disappear when you exit raw mode, in which
case you can expect to see a suitable warning.  Regarding
_include-book_ itself: it should work in raw mode as you might expect,
at least if a compiled file or expansion file was created when the book
was certified; see CERTIFY-BOOK.

_Packages_.  Raw mode disallows the use of defpkg.  If you want to
create a new package, first exit raw mode with :set-raw-mode nil; you
can subsequently re-enter raw mode with :set-raw-mode t if you wish.

ADD-RAW-ARITY    add arity information for raw mode

Technical note: This macro is a no-op, and is not necessary, when ACL2
is built with #-acl2-mv-as-values.

Users of raw mode (see SET-RAW-MODE) can use arbitrary raw Lisp
functions that are not known inside the usual ACL2 loop.  In such
cases, ACL2 may not know how to display a multiple value returned by
ACL2's mv macro.  The following example should make this clear.

     ACL2 P>(defun foo (x y) (mv y x))
     FOO
     ACL2 P>(foo 3 4)

     Note: Unable to compute number of values returned by this evaluation
     because function FOO is not known in the ACL2 logical world.  Presumably
     it was defined in raw Lisp or in raw mode.  Returning the first (perhaps
     only) value for calls of FOO.
     4
     ACL2 P>(add-raw-arity foo 2)
      RAW-ARITY-ALIST
     ACL2 P>(foo 3 4)
     (4 3)
     ACL2 P>

The first argument of add-raw-arity should be a symbol, representing the
name of a function, macro, or special form, and the second argument
should either be a non-negative integer (denoting the number of values
returned by ACL2) or else the symbol :LAST, meaning that the number of
values returned by the call is the number of values returned by the last
argument.

The current arity assignments can be seen by evaluating (@
raw-arity-alist).  See REMOVE-RAW-ARITY for how to undo a call
of add-raw-arity.

REMOVE-RAW-ARITY    remove arity information for raw mode

Technical note: This macro is a no-op, and is not necessary, when ACL2
is built with #-acl2-mv-as-values.

The form (remove-raw-arity fn) undoes the effect of an earlier
(remove-raw-arity fn val).  See ADD-RAW-ARITY.

SET-RAW-MODE-ON!    enter "raw mode," a raw Lisp environment

This is the same as (set-raw-mode t) except that it first introduces a
so-called "trust tag" ("ttag") so that set-raw-mode will be legal.  See
DEFTTAG for a discussion of ttags and how they affect
certify-book and include-book.

See SET-RAW-MODE for a discussion of raw-mode.

SET-RAW-PROOF-FORMAT    print runes as lists in proof output from simplification

     General Forms:
     (set-raw-proof-format t)
     :set-raw-proof-format t
     (set-raw-proof-format nil)
     :set-raw-proof-format nil

This command affects output from the theorem prover only when 'prove
output is not inhibited (see SET-INHIBIT-OUTPUT-LST) and
gag-mode is off (see SET-GAG-MODE).  Calling this macro with
value t as shown above will cause simplification steps from proof
output, including steps from preprocess (see SIMPLE), to print
the list of runes used in a list format, rather than in the English
proof commentary.  This "raw" format can be handy when you want to use
that list as a basis for hints that you construct for a subsequent
proof attempt.

SET-REWRITE-STACK-LIMIT    Sets the rewrite stack depth used by the rewriter

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

     Example Forms:
     (set-rewrite-stack-limit 30)                            ; set to small limit
     :set-rewrite-stack-limit 30                             ; same as above
     (set-rewrite-stack-limit *default-rewrite-stack-limit*) ; the default
     :set-rewrite-stack-limit (1- (expt 2 28))               ; maximum legal limit
     :set-rewrite-stack-limit nil         ; same as above -- essentially, no limit

This event sets the maximum stack depth for calls of certain functions
that implement the ACL2 rewriter; see REWRITE-STACK-LIMIT.  It
must be a non-negative integer less than 2^28.  A call
(set-rewrite-stack-limit limit) is equivalent to:

     (table acl2-defaults-table :rewrite-stack-limit limit).

The use of acl2-defaults-table ensures that this event's effect is
implicitly local to the book or encapsulate form in which it occurs.

For a different but somewhat related concept, see
BACKCHAIN-LIMIT.

SET-RULER-EXTENDERS    See RULER-EXTENDERS.

SET-RW-CACHE-STATE    set the default rw-cache-state

The ACL2 rewriter uses a data structure, called the rw-cache (rewriter
cache), to save failed attempts to apply conditional rewrite rules.  The
regression suite has taken approximately 11% less time with this
mechanism.  The rw-cache is active by default but this event allows it
to be turned off or modified.  Note that this event is local to its
context (from encapsulate or include-book).  For a non-local version,
use set-rw-cache-state!.

     Example forms:
     (set-rw-cache-state :atom)     ; default: rw-cache cleared for each literal
                                    ;   (i.e., hypothesis or conclusion of a goal)
     (set-rw-cache-state nil)       ; rw-cache is inactive
     (set-rw-cache-state t)         ; rw-cache persists beyond each literal
     (set-rw-cache-state :disabled) ; rw-cache is inactive, but the rw-cache-state
                                    ;   transitions to state t after
                                    ;   simplification takes place

     General Form:
     (set-rw-cache-state val)

where val evaluates to one of the four values shown in "Example forms"
above.  The default is :atom, which enables the rw-cache but clears it
before rewriting a hypothesis or conclusion of any goal.  The value t is
provides more aggresive use of the rw-cache, basically preserving the
rw-cache when there is a single subgoal.  The value :disabled is the
same as t, except that the rw-cache is initially inactive and only
becomes active when some simplification has taken place.  We have seen
a few cases where value t will make a proof fail but :disabled does not.

The following example illustrates the rw-cache in action.  You will see
a break during evaluation of the thm form.  Type :eval and you will see
a failed rewriting attempt.  Type :go to continue, and at the next
break type :eval again.  This time you will see the same failed
rewriting attempt, but this time labeled with a notation saying that
the failure was cached earlier, which indicates that this time the
rewriter did not even attempt to prove the hypothesis of the rewrite
rule f1->f2.

     (defstub f1 (x) t)
     (defstub f2 (x) t)
     (defaxiom f1->f2
              (implies (f1 x) (equal (f2 x) t)))
     :brr t
     :monitor (:rewrite f1->f2) t
     (thm (equal (car (f2 a)) (cdr (f2 a))))

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.  It is
local to the book or encapsulate form in which it occurs (see
SET-RW-CACHE-STATE! for a corresponding non-local event).

We also note that rw-cache-state changes may also be caused at the
subgoal level; see HINTS.

We welcome you to experiment with different rw-cache states.  If the
more aggressive values of t and :disabled cause proofs to fail, then you
can revert to the default of :atom or even turn off the rw-cache using
(set-rw-cache-state nil).  We don't expect users to need a deep
knowledge of the rw-cache in order to do such experiments, but readers
interested in details of the rw-cache implementation are invited to
read the "Essay on Rw-cache" in the ACL2 source code.

SET-RW-CACHE-STATE!    set the default rw-cache-state non-locally

Please see SET-RW-CACHE-STATE, which is the same as
set-rw-cache-state!  except that the latter is not local to the
encapsulate or the book in which it occurs.

SET-SAVED-OUTPUT    save proof output for later display with :pso or :pso!

     Examples:
     (set-saved-output t t)    ; save proof output for later, but inhibit it now
     (set-saved-output t :all) ; save proof output for later, but inhibit all
                               ;   output (except WARNING!, for critical warnings,
                               ;   and ERROR, unless these are already inhibited)
     :set-saved-output t :all  ; same as the line above
     (set-saved-output t nil)  ; save proof output for later, but print it now too
     (set-saved-output nil t)  ; do not save proof output, and inhibit it
     (set-saved-output nil nil); do not save proof output or inhibit output
     (set-saved-output nil :same), (set-saved-output t :same)
                               ; save proof output or not, as indicated, but do
                               ;   not change which output is inhibited
     (set-saved-output nil :normal)
                               ; the behavior when ACL2 first starts up: do not
                               ;   save output, and only inhibit proof-tree output
     (set-saved-output t '(warning observation proof-tree prove))
                               ; save proof output for later, and inhibit the
                               ;   indicated kinds of output

     General Form:
     (set-saved-output save-flg inhibit-flg)

Parameter save-flg is t to cause output to be saved for later display
using pso or pso!; see PSO and see PSO!, and see the
documentation for proof-checker commands of the same names.  Set
save-flg to nil to turn off this feature; except, it always stays on in
proof-checker sessions entered with verify.  The other argument,
inhibit-flg, controls whether output should be inhibited when it is
created (normally, during a proof attempt).  So a common combination is
to set both arguments to t, to indicate that output should be
suppressed for now but saved for printing with pso or pso!.  The
examples above give a good summary of the functionality for the second
argument.

Saved output is cleared at the start of every event, and also at the
start of every proof-checker commands that invoke the prover.  Note that
interactive proof-checker commands, that is, from a proof-checker
session entered with verify, are always run with output saved.

Also see SET-GAG-MODE; and see SET-PRINT-CLAUSE-IDS,
which causes subgoal numbers to be printed during proof attempts when
output is inhibited.

See SET-INHIBIT-OUTPUT-LST if you want to inhibit certain
output from the prover but not other output (e.g., not the summary),
and you don't want to save any output.

SET-STATE-OK    allow the use of STATE as a formal parameter

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

In brief:  The variable symbol STATE has an unusual status in ACL2.  In
order to use it, you either need to issue :set-state-ok t, as we
explain below, or you need to declare it to be a stobj, as explained
elsewhere (see DECLARE-STOBJS).  Now we explain in more detail.

Because the variable symbol STATE denotes the "current ACL2 state,"
ACL2 treats the symbol very restrictively when it occurs as a formal
parameter of a defined function.  The novice user, who is unlikely to
be aware of the special status of that symbol, is likely to be confused
when error messages about STATE are printed in response to the innocent
choice of that symbol as a formal variable.  Therefore the top-level
ACL2 loop can operate in a mode in which STATE is simply disallowed as
a formal parameter.

For a discussion of STATE, See STATE and see STOBJ.
Roughly speaking, at the top-level, the "current ACL2 state" is denoted
by the variable symbol STATE.  Only the current state may be passed
into a function expecting a state as an argument.  Furthermore, the
name of the formal parameter into which the current state is passed
must be STATE and nothing but the current state may be passed into a
formal of that name.  Therefore, only certain access and change
functions can use that formal -- namely those with a STATE formal --
and if any such function produces a new state it becomes the "current
state" and must be passed along in the STATE position thereafter.
Thus, ACL2 requires that the state be single-threaded.  This, in turn,
allows us to represent only one state at a time and to produce new
states from it destructively in a von Neumaneque fashion.  The
syntactic restrictions on the variable STATE are enforced by the
translate mechanism (see TRANS and see TERM) when terms
are read.

To prevent the novice user from seeing messages prohibiting certain
uses of the variable symbol STATE ACL2 has a mode in which it simply
disallows the use of that symbol as a formal parameter.  Use of the
symbol causes a simple error message.  The system is initially in that
mode.

To get out of that mode, execute:

     :set-state-ok t ;;; or, (set-state-ok t)

It is not recommended that you do this until you have read the
documentation of STATE.

To enter the mode in which use of state is prohibited as a formal
parameter, do:

     :set-state-ok nil

The mode is stored in the defaults table, See
ACL2-DEFAULTS-TABLE.  Thus, the mode may be set locally in books.

SET-TAU-AUTO-MODE    turn on or off automatic ("greedy") generation of :tau-system rules

     Examples:
     (set-tau-auto-mode t)      ; select automatic (``greedy'') mode
     (set-tau-auto-mode nil)    ; select manual mode

This event is equivalent to (table acl2-defaults-table :tau-auto-modep
<t-or-nil>), and hence is local to any books and encapsulate events in
which it occurs; see ACL2-DEFAULTS-TABLE.  See
INTRODUCTION-TO-THE-TAU-SYSTEM for background details.

The tau system gathers rules for its database in one of two ways:
greedily or only at the explicit command of the user.  "Greedy" mode is
officially called "automatic mode" and is the default.  The other mode
is called "manual mode."

In automatic mode, all rules processed by ACL2 are also considered for
inclusion in the tau database: if the :corollary of some proved theorem
happens to fit into one of the forms described in :tau-system, that
rule is quietly added to the tau database regardless of what
:rule-classes the user named for the :corollary.  Of course, such rules
are also stored in the ways named by the user.  See the Design
Philosophy section of introduction-to-the-tau-system for a discussion
of why the tau system is greedy by default.  More details are given on
automatic mode after we explain manual mode.

To more tightly control the rules available to the tau system, the user
may select manual mode by executing (set-tau-auto-mode nil).  In manual
mode, the only events that create :tau-system rules are defthm events
explicitly specifying the :tau-system rule class in the :rule-classes
argument.  Of course, for a :tau-system rule to be created from a
proved formula (or its specified :corollary), the formula must be of
the appropriate shape (syntactic form). See TAU-SYSTEM.  In
manual mode, if the :tau-system rule class is specified but the formula
is not of an appropriate form an error is signalled.  (Note: even in
manual mode, monadic functions that are recognized as Boolean are
classified as tau predicates; but no rules are created for them.)

Returning to our discussion of automatic mode, a :tau-system rule may
be created by any of the events below, provided the definition or
formula proved is of an appropriate shape:

(1) defun events introducing "big switch" or "mv-nth synonyms,"

(2) defun events creating type-prescription rules that may be also
represented as "signature rules" of form 1, and

(3) any defthm event with a non-nil :rule-classes argument if no
:tau-system rule is among the rule classes and the formula proved is in
 the shape of any tau-system rule.

Of course, events such as defstobj and defevaluator may also add rules
to the tau database when they execute the defun and defthm events
implicit in their descriptions.  See TAU-SYSTEM for a
description of the various shapes mentioned above.

Note that any rule (of any rule class) created when the tau system is in
manual mode is also created in automatic mode.  For example, if an event
would create a :DEFINITION, :TYPE-PRESCRIPTION, FORWARD-CHAINING, or
:REWRITE rule when the tau system is in manual mode, then the event
will create that same rule when the tau system is in automatic mode.
Automatic mode just means that some additional :tau-system rules may be
created.

Of course, if a defthm event explicitly specifies a :tau-system rule
class, then even if the tau system is in automatic mode, that tau rule
is created from the proved formula (or the specified :corollary) or
else an error is caused.  But if the tau system is in automatic mode
and a defthm event doesn't explicitly specify a :tau-system rule class,
then the system quietly checks each specified :corollary -- or, in the
absence of any :corollary, it checks the proved formula -- for whether
it can be stored as a tau rule.  If so, then the system stores a tau
rule, in addition to storing the specified rule.  Of course, no error
is signalled if a proved formula of some non-:tau-system rule class
fails to be of an appropriate shape for the tau system.

In automatic mode, if the :rule-classes specified for defthm included
several corollaries and any one of them is of class :tau-system then the
only tau system rules created are those explicitly classed as
:tau-system rules.  For example, suppose a defthm has one :corollary
stored as a :rewrite rule and another :corollary stored as a :tau-system
rule.  But suppose the :rewrite rule happens to also to fit the form of
a :tau-system rule.  Is it added to the tau database or not?  The answer
is no.  If you have taken the trouble to specify :tau-system corollaries
for an event, then those corollaries are the only ones stored as tau
sytem rules from that event.  Note that had both corollaries been
classed as :rewrite rules (and been of acceptable :tau-system form)
both would have also been made :tau-system rules.  This also allows you
be in automatic mode and state a :rewrite or other non-:tau-system rule
and prevent it from being also made a tau system rule:  just add a
frivolous :tau-system :corollary like (booleanp (integerp x)).

Recall that the use of tau rules is controlled by the rune
(:EXECUTABLE-COUNTERPART TAU-SYSTEM).  When that rune is disabled, no
tau rules are used in proofs.  However, the tau system continues to
collect tau rules if the system is in automatic mode.  Thus, if and
when the tau system is re-enabled, rules automatically generated while
the tau system was disabled will be used as usual by the tau system.

Finally, note that defthm events with :rule-classes nil do not create
:tau-system rules even if the formula proved is of an appropriate
shape, regardless of whether the tau system is in automatic or manual
mode.

The macro tau-status provides a convenient way to enable/disable the
:executable-counterpart of tau-system and/or to switch between manual
and automatic modes.  It may also be used to determine the current
settings of those two flags.

SET-TOTAL-PARALLELISM-WORK-LIMIT    for ACL2(p): set thread limit for parallelism primitives

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.
While the most common use of the limit described below is in parallel
proof (see PARALLEL-PROOF), it also applies to all parallelism
primitives (see PARALLEL-PROGRAMMING) except spec-mv-let --
though we expect that rather few programming applications will encouter
this limit.

     General Forms:
     (set-total-parallelism-work-limit :none)     ; disable the limit
     (set-total-parallelism-work-limit <integer>) ; set limit to <integer>

See PARALLELISM-TUTORIAL, Section "Another Granularity Issue
Related to Thread Limitations", for an explanation of how the host Lisp
can run out of threads.  Also see
SET-TOTAL-PARALLELISM-WORK-LIMIT-ERROR.

If the underlying runtime system (the Operating System, the host Lisp,
etc.)  is unable to provide enough threads to finish executing the
parallelism work given to it, the runtime system can crash in a very
unpleasant manner (ranging from a Lisp error to completely freezing the
machine).  To avoid this unpleasantness, ACL2(p) will attempt to avoid
creating so much parallelism that the runtime system crashes.

ACL2 initially uses a conservative estimate to limit the number of
threads.  To tell ACL2(p) to use a different limit, call
set-total-parallelism-work-limit with the new limit.  For example, if
the current default limit is 10,000, then to allow 13,000 threads to
exist, issue the following form at the top level.

     (set-total-parallelism-work-limit 13000)

To disable this limit altogether, evaluate the following form:

     (set-total-parallelism-work-limit :none)

The default value of total-parallelism-work-limit can be found by
calling function default-total-parallelism-work-limit.  If the default
value is too high for your system please notify the ACL2 maintainers
with a limit that does work for your system, as they might then lower
the default limit.

SET-TOTAL-PARALLELISM-WORK-LIMIT-ERROR    for ACL2(p): control the action taken when the thread limit is exceeded

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

     General Forms:
     (set-total-parallelism-work-limit-error t)   ; cause error (default)
     (set-total-parallelism-work-limit-error nil) ; disable error and
                                                  ; continue serially

See PARALLELISM-TUTORIAL, Section "Another Granularity Issue
Related to Thread Limitations", for an explanation of how the host Lisp
can run out of threads.  See SET-TOTAL-PARALLELISM-WORK-LIMIT
for further details, including an explanation of how to manage the
limit that triggers this error.

The value of state global total-parallelism-work-limit-error dictates
what occurs when the underlying runtime system runs reaches a limit on
the number of threads for parallel computation.  By default, when this
limit is reached, the ACL2(p) user will receive an error and
computation will halt.  At this point, the ACL2(p) user has the
following options.

(1) Remove the limit by evaluating the following form.

     (set-total-parallelism-work-limit :none)

(2) Disable the error so that execution continues serially once the
available thread resources have been exhausted.

     (set-total-parallelism-work-limit-error nil)

(3) Increase the limit on number of threads that ACL2(p) is willing to
create, in spite of potential risk (see
SET-TOTAL-PARALLELISM-WORK-LIMIT).  In this case, the following query
returns the current limit.

     (f-get-global 'total-parallelism-work-limit)

Then to increase that limit, evaluate the following form:

     (set-total-parallelism-work-limit <new-integer-value>)

For example, suppose that the value of total-parallelism-work-limit was
originally 10,000.  Then evaluation of the following form increases that
limit to 13,000.

     (set-total-parallelism-work-limit 13000)

SET-VERIFY-GUARDS-EAGERNESS    the eagerness with which guard verification is tried.

     Example Forms:                        try guard verification?
     (set-verify-guards-eagerness 0) ; no, unless :verify-guards t
     (set-verify-guards-eagerness 1) ; yes if a :guard is supplied
     (set-verify-guards-eagerness 2) ; yes, unless :verify-guards nil

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

     General Form:
     (set-verify-guards-eagerness n)

where n is a variable-free term that evaluates to 0, 1, or 2.  This
macro is essentially equivalent to

     (table acl2-defaults-table :verify-guards-eagerness n)

and hence is local to any books and encapsulate events in which it
occurs; see ACL2-DEFAULTS-TABLE.  However, unlike the above
simple call of the table event function (see TABLE), no output
results from a set-verify-guards-eagerness event.

Set-verify-guards-eagerness may be thought of as an event that merely
sets a flag to 0, 1, or 2.  The flag is used by certain defun events to
determine whether guard verification is tried.  The flag is irrelevant
to those defun events in :program mode and to those defun events in
which an explicit :verify-guards setting is provided among the xargs.
In the former case, guard verification is not done because it can only
be done when logical functions are being defined.  In the latter case,
the explicit :verify-guards setting determines whether guard
verification is tried.  So consider a :logic mode defun in which no
:verify-guards setting is provided.  Is guard verification tried?  The
answer depends on the eagerness setting as follows.  If the eagerness
is 0, guard verification is not tried.  If the eagerness is 1, it is
tried iff a :guard is explicitly provided in the defun.  If the
eagerness is 2, guard verification is tried.

The default behavior of the system is as though the
:verify-guards-eagerness is 1.  The current behavior can be ascertained
by evaluating the form (default-verify-guards-eagerness (w state)).

SET-WATERFALL-PARALLELISM    for ACL2(p): configuring the parallel execution of the waterfall

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

     General Forms:
     (set-waterfall-parallelism nil)        ; never parallelize (serial execution)
     (set-waterfall-parallelism :full)      ; always parallelize
     (set-waterfall-parallelism :top-level) ; parallelize top-level subgoals
     (set-waterfall-parallelism             ; parallelize if sufficient resources
       :resource-based)                     ;   (recommended setting)
     (set-waterfall-parallelism t)          ; alias for :resource-based
     (set-waterfall-parallelism             ; parallelize if sufficient resources
       :resource-and-timing-based           ;   and suggested by prior attempts
     (set-waterfall-parallelism             ; never parallelize but use parallel
       :pseudo-parallel)                    ;   code base (a debug mode)

Set-waterfall-parallelism evaluates its argument, which specifies the
enabling or disabling of the parallel execution of ACL2's main proof
process, the waterfall.

It also sets state global waterfall-printing to an appropriate value.
See SET-WATERFALL-PRINTING.

Note that not all ACL2 features are supported when
waterfall-parallelism is set to non-nil (see
UNSUPPORTED-WATERFALL-PARALLELISM-FEATURES).

A value of t is treated the same as a value of :resource-based and is
provided for user convenience.

:Resource-based waterfall parallelism typically achieves the best
performance in ACL2(p), while maintaining system stability, so
:resource-based (or equivalently, t) is the recommended value.

A value of nil indicates that ACL2(p) should never prove subgoals in
parallel.

A value of :full indicates that ACL2(p) should always prove independent
subgoals in parallel.

A value of :top-level indicates that ACL2(p) should prove each of the
top-level subgoals in parallel but otherwise prove subgoals in a serial
manner.  This mode is useful when the user knows that there are enough
top-level subgoals, many of which take a non-trivial amount of time to
be proved, such that proving them in parallel will result in a useful
reduction in overall proof time.

A value of :resource-based (or equivalently, t) indicates that ACL2(p)
should use its built-in heuristics to determine whether CPU core
resources are available for parallel execution.  Note that ACL2(p) does
not hook into the operating system to determine the workload on the
machine.  ACL2(p) works off the assumption that it is the only process
using significant CPU resources, and it optimizes the amount of
parallelism based on the number of CPU cores in the system.  (Note that
ACL2(p) knows how to obtain the number of CPU cores from the operating
system in CCL, but that, in SBCL and in Lispworks, a constant is used
instead).

During the first proof attempt of a given conjecture, a value of
:resource-and-timing-based results in the same behavior as with
:resource-based.  However, on subsequent proof attempts, the time it
took to prove each subgoal will be considered when deciding whether to
parallelize execution.  If a particular theorem's proof is already
achieving satisfactory speedup via :resource-based parallelism, there
is no reason to try this setting.  However, if the user wishes to
experiment, the :resource-and-timing-based setting may improve
performance.  Note that since the initial run does not have the subgoal
proof times available, this mode will never be better than the
:resource-based setting for non-interactive theorem proving.

A value of :pseudo-parallel results in using the parallel waterfall
code, but with serial execution.  This setting is useful for debugging
the code base that supports parallel execution of the waterfall.  For
example, you may wish to use this mode if you are an "ACL2 Hacker" who
would like to see comprehensible output from tracing (see
TRACE$) the @par versions of the waterfall functions.

The following remark pertains to those using the `HONS' experimental
extension of ACL2 (see HONS-AND-MEMOIZATION; in particular, see
MEMOIZE).  Since memoization is not supported when waterfall
parallelism is enabled (see
UNSUPPORTED-WATERFALL-PARALLELISM-FEATURES), then when
set-waterfall-parallelism is called with a non-nil value, all memoized
functions are unmemoized.  When set-waterfall-parallelism is again
called with a nil value, those memoization settings are restored.

Set-waterfall-parallelism is an embedded event form.  However, a call of
this macro will not affect waterfall-parallelism when including a
certified book that contains that call.  For such an effect, you may
use the following make-event form.

     (make-event (er-progn (set-waterfall-parallelism :full)
                           (value '(value-triple nil)))
                 :check-expansion t)

SET-WATERFALL-PARALLELISM-HACKS-ENABLED    for ACL2(p): enable waterfall-parallelism hacks

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

     General Forms:
     (set-waterfall-parallelism-hacks-enabled t)
     (set-waterfall-parallelism-hacks-enabled nil)

Some features (e.g., override-hints and clause-processors) of serial
ACL2 are by default not available in ACL2(p) with waterfall parallelism
enabled, because they offer a mechanism to modify state that is
unsound.  To allow or (once again) disallow the use the these features
in ACL2(p), call set-waterfall-parallelism-hacks-enabled with argument t
or nil, respectively.

Set-waterfall-parallelism-hacks-enabled requires the use of a trust tag
(see DEFTTAG).  One can call
set-waterfall-parallelism-hacks-enabled!  instead, which will
automatically install a trust tag named :waterfall-parallelism-hacks.

See ERROR-TRIPLES-AND-PARALLELISM for further related
discussion.

SET-WATERFALL-PARALLELISM-HACKS-ENABLED!    for ACL2(p): enabling waterfall parallelism hacks

See SET-WATERFALL-PARALLELISM-HACKS-ENABLED.

SET-WATERFALL-PRINTING    for ACL2(p): configuring the printing that occurs within the parallelized waterfall

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see PARALLELISM.

     General Forms:
     (set-waterfall-printing :full)    ; print everything
     (set-waterfall-printing :limited) ; print a subset that's thought to be useful
     (set-waterfall-printing :very-limited) ; print an even smaller subset

Set-waterfall-printing evaluates its argument, which indicates how much
printing should occur when executing ACL2 with the parallelized version
of the waterfall.  It only affects the printing that occurs when
parallelism mode is enabled for the waterfall (see
SET-WATERFALL-PARALLELISM).

A value of :full is intended to print the same output as in serial mode.
This output will be interleaved unless the waterfall-parallelism mode
is one of nil or :pseudo-parallel.

A value of :limited omits most of the output that occurs in the serial
version of the waterfall.  Instead, the proof attempt prints key
checkpoints (see ACL2P-KEY-CHECKPOINTS).  The value of :limited
also prints messages that indicate which subgoal is currently being
proved, along with the wall-clock time elapsed since the theorem began
its proof; and if state global 'waterfall-printing-when-finished has a
non-nil value, then such a message will also be printed at the
completion of each subgoal.  The function print-clause-id-okp may
receive an attachment to limit such printing; see
SET-PRINT-CLAUSE-IDS.  Naturally, these subgoal numbers can appear
out of order, because the subgoals can be proved in parallel.

A value of :very-limited is treated the same as :limited, except that
instead of printing subgoal numbers, the proof attempt prints a period
(`.') each time it starts a new subgoal.

Note that this form cannot be used at the top level of a book, or of a
progn or encapsulate event.  Here is a workaround for use in such
contexts; of course, you may replace :very-limited with any other legal
argument for set-waterfall-printing.

     (make-event (er-progn (set-waterfall-printing :very-limited)
                           (value '(value-triple nil))))

(For more about event contexts and the use of make-event, see
MAKE-EVENT, in particular the section "Restriction to Event
Contexts.")

The following form has the effect described above, except that it will
affect waterfall-printing even when including a certified book that
contains it.

     (make-event (er-progn (set-waterfall-printing :very-limited)
                           (value '(value-triple nil)))
                 :check-expansion t)

Note that set-waterfall-printing is automatically called by
set-waterfall-parallelism.

To enable the printing of information when a subgoal is finished,
assign a non-nil value to global waterfall-printing-when-finished.
This can be accomplished by entering the following at the top level:

     (f-put-global 'waterfall-printing-when-finished t state)

SET-WELL-FOUNDED-RELATION    set the default well-founded relation

     Examples:
     (set-well-founded-relation lex2)

provided lex2 has been proved to be a well-founded relation (see
WELL-FOUNDED-RELATION).  Note: This is an event!  It does not print
the usual event summary but nevertheless changes the ACL2 logical world
and is so recorded.

     General Form:
     (set-well-founded-relation rel)

where rel has been proved to be a well-founded relation on objects
satisfying some predicate, mp; see WELL-FOUNDED-RELATION.  This
macro is equivalent to (table acl2-defaults-table
:well-founded-relation 'rel), and hence is local to any books and
encapsulate events in which it occurs; see ACL2-DEFAULTS-TABLE.

This event sets the default well-founded relation to be that imposed on
mp-measures by the relation rel.  Subsequently, if a recursively
defined function is submitted to defun with no explicitly given
:well-founded-relation argument, defun uses the default relation, rel,
and the associated domain predicate mp used in its well-foundedness
theorem.  That is, the termination conditions generated will require
proving that the measure used by the defun is an mp-measure and that in
every recursive call the measure of the arguments decreases according
to rel.

SET-WRITE-ACL2X    cause certify-book to write out a .acl2x file

     Example Forms:
     (set-write-acl2x nil state)
     (set-write-acl2x t state)
     (set-write-acl2x '(nil) state) ; same as just above, but allow inclusion of
                                    ; uncertified books during certify-book
     (set-write-acl2x '(t) state)
     (set-write-acl2x '(include-book-with-locals) state)

     General Form:
     (set-write-acl2x val state)

where val evaluates to t, nil, or a one-element list whose element is a
legal value for the global 'ld-skip-proofsp; see
LD-SKIP-PROOFSP.  The value returned is an error triple, which in the
non-error case is (mv nil v state), where v is the value of val and
state is the result of updating the input state by assigning state
global 'write-acl2x the value v.

The command (set-write-acl2x val state) assigns the value of val to the
state global variable 'write-acl2x, affecting whether or not
certify-book writes out a file with extension acl2x, called a ".acl2x
file" and pronounced "dot-acl2x file".  Such a file is read or written
by certify-book when it is supplied with keyword argument :acl2x t.  By
default, such a call of certify-book reads a .acl2x file; but if the
value of state global variable 'write-acl2x is not nil, then
certify-book writes a .acl2x file (in which case it is illegal to
specify a non-nil value for certify-book keyword argument :pcert).
Consider for example (certify-book "foo" 0 nil :acl2x t).  By default,
this command reads file foo.acl2x, which supplies replacements for some
forms in foo.lisp, as described later below.  But if the value of state
global 'write-acl2x is not nil, then instead, this certify-book command
writes such a file foo.acl2x.

Before we discuss the function of .acl2x files, we first explain more
about how a non-nil value of state global 'write-acl2x affects the
behavior of a command (certify-book ... :acl2x t ...).  A significant
effect on the behavior is that after processing events in the given
book, ACL2 writes out a .acl2x file and then returns, skipping the other
subsequent actions typically performed by certify-book: a
local-incompatibility check, writing of a certificate file, and
possibly compilation.  Another effect is that proofs may be skipped when
processing events assuming that the the certify-book command does not
explicitly specify :skip-proofs-okp nil, as we now explain.  A non-nil
value of 'write-acl2x should either be t or a one-element list (x),
where x is a legal value for the state global 'ld-skip-proofsp (see
LD-SKIP-PROOFSP).  In both cases, certify-book will process
events to write out a .acl2x file as described above.  But in the
latter (list) case, event processing will take place according to the
value of x: in particular, proofs will be skipped when x is not nil,
and if moreover x is the symbol include-book-with-locals, then only one
pass will be made through each encapsulate form.  A third effect of a
non-nil value of 'write-acl2x, which is restricted to the list case, is
that include-book events encountered during event processing are
allowed to succeed on uncertified books, something that is prohibited
during most calls of certify-book.

When certify-book is used to write out a .acl2x file, there is
typically a subsequent run of certify-book that reads that file.
Consider how this can work with a book foo.lisp.  In the first call of
certify-book, a file foo.acl2x is written that contains all make-event
expansions, but foo.cert is not written.  In the second call of
certify-book, no make-event expansion typically takes place, because
foo.acl2x supplies the expansions.  The command (set-write-acl2x t
state) should be evaluated before the first certification (though
another legal non-nil value may be used in place of t), setting the
value of state global 'write-acl2x to t, to enable writing of
foo.acl2x; and the command (set-write-acl2x nil state) may be evaluated
before the second run (though this is not necessary in a fresh ACL2
session) in order to complete the certification (writing out foo.cert)
using foo.acl2x to supply the make-event expansions.

When Certify-book is supplied with keyword argument :acl2x t it will
read or write the book's .acl2x file; when supplied with :acl2x nil, it
will not read or write that .acl2x file.  The value of :acl2x is nil by
default.  The interaction of certify-book with the corresponding .acl2x
file is as follows.

     o If :acl2x is t, then:
       - If set-write-acl2x has been (most recently) called with a
         value of t for its first argument, then ACL2 writes the
         corresponding .acl2x file.
       - If set-write-acl2x has been (most recently) called with a
         value of nil for its first argument, or not called at all,
         then ACL2 insists on a corresponding .acl2x file that is at
         least as recent as the corresponding .lisp file, causing an
         error otherwise.
     o If :acl2x is nil, then:
       - If set-write-acl2x has been (most recently) called with a
         value t for its first argument, or if argument :ttagsx
         is supplied, then an error occurs.
       - If the .acl2x file exists, then regardless of whether or how
         set-write-acl2x has been called, ACL2 ignores the .acl2x
         file but issues a warning about it.

Suppose you use the two-runs approach: first write a .acl2x file, then
certify using (reading) that .acl2x file.  Then with scripts such as
makefiles, then you may wish to provide a single certify-book command
to use for both runs.  For that purpose, certify-book supports the
keyword argument :ttagsx.  If this argument is supplied and write-acl2x
is true, then this argument is treated as the :ttags argument,
overriding a :ttags argument if present.  That is, for the two runs,
:ttagsx may be used to specify the trust tags used in the first
certification while :ttags specifies the trust tags, if any (else
:ttags may be omitted), used in the second certification.  Note: If the
argument :ttagsx is not supplied, then its value defaults to the
(explicit or default) value of the :ttags argument.

The built-in ACL2 Makefile support automatically generates suitable
dependencies if you create a .acl2 file with a certify-book call
matching the following regular expression, case-independent:

       (certify-book[^;]*:acl2x t

See BOOK-MAKEFILES, and for an example .acl2 file with a
certify-book call matching the above pattern, see community books file
books/make-event/double-cert-test-1.acl2.

Note that include-book is generally not affected by set-write-acl2x,
other than through the indirect effect on certify-book.  More
precisely: All expansions are stored in the certificate file, so when
include-book is applied to a certified book, the .acl2x file is not
consulted.

An example of how to put this all together may be found in community
book books/make-event/double-cert-test-1.lisp.  There, we see the
following form.

     (make-event
      (progn (defttag :my-ttag)
             (progn! (let ((val (sys-call "pwd" nil)))
                       (value (list 'defun 'foo () val))))))

Imagine that in place of the binding computed using sys-call, which by
the way requires a trust tag, is some computation of your choice (such
as reading forms from a file) that is used to construct your own event,
in place of the defun event constructed above.  The Makefile in that
directory contains the following added dependency, so that file
double-cert-test-1.acl2x will be created:

     double-cert-test-1.cert: double-cert-test-1.acl2x

There is also the file double-cert-test-1.acl2 in that directory, which
contains a single form as follows.

     (certify-book "double-cert-test-1" ? t :ttagsx :all :ttags nil)

Thus, a call of make first creates file double-cert-test-1.acl2x, which
uses the above :ttagsx argument in order to support the use of defttag
during make-event expansion.  Then, make goes on to cause a second
certification in which no trust tags are involved.  As a result, the
parent book double-cert-test.lisp is ultimately certified without
requiring any trust tags.

The discussion above is probably sufficient for most users of the
two-run approach it describes.  We conclude with further details for
those who want more information.  Those who wish to see a yet
lower-level explanation of how all this works are invited to read the
comment in the ACL2 source code entitled "Essay on .acl2x Files (Double
Certification).

Consider the .acl2x file produced by the first run as described above.
It contains a single expression, which is an association list whose
keys are all positive integers, which occur in increasing order.  When
the .acl2x file is present and at least as recent as the corresponding
.lisp file, then for a subsequent certify-book with argument :acl2x t
and the (default) value of nil for state global 'write-acl2x, that
association list will be applied to the top-level events in the book, as
follows.  Suppose the entry (n . ev) belongs to the association list in
the .acl2x file.  Then n is a positive integer, and the nth top-level
event in the book -- where the 0th event is the initial in-package form
-- will be replaced by ev.  In practice, ev is the make-event expansion
created during certification for the nth top-level event in the book;
and this will always be the case if the .acl2x file is created by
certify-book after execution of the form (set-write-acl2x t state).
However, you are welcome to associate indices manually with any events
you wish into the alist stored in the .acl2x file.

Note: Also see the community book make-event/acl2x-help.lisp for a
useful utility that can be used to skip proofs during the writing of
.acl2x files.

TAU-STATUS    query or set tau system status

     Examples:
     (tau-status)
     (tau-status :system t)
     (tau-status :auto-mode nil)
     (tau-status :system t :auto-mode nil)

     General Form:
     (tau-status :system a :auto-mode b)

where a and b are Booleans.  Both keyword arguments are optional and
they may be presented in either order.  Value a controls whether the
tau-system is used during subsequent proofs.  Value b controls whether
tau system rules are added automatically ("greedily") when rules of
other rule-classes are added.  If no arguments are supplied, this is
not an event and just returns an error-triple (see
ERROR-TRIPLES) indicating the current settings.  See
INTRODUCTION-TO-THE-TAU-SYSTEM for background details.

The two flags are independent.  For example, the tau system may be
disabled in proof attempts even though it is automatically (and
silently) extending its database as rules of other classes are added.

Flag (a) is actually toggled by enabling or disabling the
:executable-counterpart of tau-system.  Flag (b) is toggled with the
function set-tau-auto-mode, which manipulates the acl2-defaults-table.

This macro expands into zero, one, or two events, as required by the
supplied values of flags a and b.

If no arguments are supplied the form is not an event and simply
returns (as an error triple (mv nil ans state); see
ERROR-TRIPLES) the current settings of the two flags.  For example:

     ACL2 !>(tau-system)
      ((:SYSTEM NIL) (:AUTO-MODE T))

intended to be self-explanatory.

TERM-TABLE    a table used to validate meta rules

     Example:
     (table term-table t '((binary-+ x y) '3 'nil (car x)))

See TABLE for a general discussion of tables and the table
event used to manipulate tables.

The "term-table" is used at the time a meta rule is checked for
syntactic correctness.  Each proposed metafunction is run on each term
in this table, and the result in each case is checked to make sure that
it is a termp in the current world.  In each case where this test
fails, a warning is printed.

Whenever a metafunction is run in support of the application of a meta
rule, the result must be a term in the current world.  When the result
is not a term, a hard error arises.  The term-table is simply a means
for providing feedback to the user at the time a meta rule is
submitted, warning of the definite possibility that such a hard error
will occur at some point in the future.

The key used in term-table is arbitrary.  The top-most value is always
the one that is used; it is the entire list of terms to be considered.
Each must be a termp in the current ACL2 world.

UNTRANS-TABLE    associates a function symbol with a macro for printing user-level terms

     Examples:
     ACL2 !>(untrans-table (w state))
     ((BINARY-+ + . T)
      (BINARY-* * . T)
      (BINARY-APPEND APPEND . T)
      (BINARY-LOGAND LOGAND . T)
      (BINARY-LOGIOR LOGIOR . T)
      (BINARY-LOGXOR LOGXOR . T)
      (BINARY-LOGEQV LOGEQV . T)
      (BINARY-POR POR . T)
      (BINARY-PAND PAND . T))

See TABLE for a general discussion of tables.

See ADD-MACRO-FN for a more general discussion of this table
and for a way to associate a macro name with a function name in theory
events.

USER-DEFINED-FUNCTIONS-TABLE    an advanced table used to replace certain system functions

     Examples:
     (table user-defined-functions-table 'untranslate-preprocess 'my-preprocess)
     (table user-defined-functions-table 'untranslate 'my-untranslate)

This feature should perhaps only be used by advanced users who have a
thorough understanding of the system functions being replaced.  There
are currently two ways a user can affect the way ACL2 prints terms.

The first example associates the user-defined function symbol
my-preprocess with untranslate-preprocess.  As a result, when ACL2
prints a term, say during a proof, using its so-called "untranslate"
process the first thing it does is to call my-preprocess on two
arguments: that term and the current ACL2 logical world.  If the call
produces a non-nil result, then that result is passed to the untranslate
process.

The second example associates the user-defined function symbol
my-untranslate with the built-in function symbol untranslate.  As a
result, the code for my-untranslate will be run whenever the untranslate
process is run.  The formals of the two functions must agree and must
not contain any stobj names.  Note that these overrides fail to occur
upon guard violations and some other evaluation errors.

The untranslate-preprocess approach may suffice for most cases in which
a user wants to modify the way output is produced by the theorem
prover.  We present an example immediately below, but see community book
books/misc/untranslate-patterns.lisp for a more elaborate example.  If
the untranslate-preprocess approach does not seem sufficient for your
purposes, you are invited to look at community book
books/misc/rtl-untranslate.lisp for an example of user-defined
untranslate (i.e., following the second example displayed above).

Suppose you have a large constant that you would prefer not to see in
proofs.  For example, you may have submitted the following definition
(but imagine a much larger constant, say, a list of length 1,000,000).

     (defconst *a* '(a b c d))

If you submit the following (silly) theorem

     (thm (equal (cons x *a*) (car (cons yyy zzz))))

then you will see the following output:

     (EQUAL (CONS X '(A B C D)) YYY).

If *a* had represented a much larger structure, we would wish we could
see the following instead.

     (EQUAL (CONS X *A*) YYY)

That can be accomplished as follows.  First we make the following
definition.

     (defun my-preprocess (term wrld)
       (declare (ignore wrld))
       (if (equal term (list 'quote *a*))
           '*a*
         nil))

Now we submit the following table event.

     (table user-defined-functions-table
            'untranslate-preprocess
            'my-preprocess)

This will install my-preprocess as a preprocessor before the normal
untranslation routine is applied to printing a term.  When the
untranslation routine encounters the constant (QUOTE (A B C D)), it
will replace it with *a*, and the usual untranlation routine will print
this as *A*.

VERIFY-GUARDS-EAGERNESS    See SET-VERIFY-GUARDS-EAGERNESS.

WITH-GUARD-CHECKING    suppressing or enable guard-checking for a form

     Example:

     ; Turn off all guard-checking for the indicated calls of append and car:
     (with-guard-checking :none
                          (car (append 3 4)))

     General Form:
     (with-guard-checking val form)

where val evaluates to a legal guard-checking value (see
SET-GUARD-CHECKING, or evaluate *guard-checking-values* to see the
list of such values), and form is a form to be evaluated as though we
had first executed (set-guard-checking val).  Of course, this
gaurd-checking setting is active only during evaluation of form, and is
ignored once evaluation passes into raw Lisp functions (see
GUARDS-AND-EVALUATION).

WITH-OUTPUT    suppressing or turning on specified output for an event

     Examples:

     ; Turn off all output during evaluation of the indicated thm form.
     (with-output
      :off :all
      :gag-mode nil
      (thm (equal (app (app x y) z) (app x (app y z)))))

     ; Prove the indicated theorem with the event summary turned off and
     ; using the :goals setting for gag-mode.
     (with-output
        :off summary
        :gag-mode :goals
        (defthm app-assoc (equal (app (app x y) z) (app x (app y z)))))

     ; Same effect as just above:
     (with-output
        :on summary
        :summary :all ; equivalently, the value (a list) of *summary-types*
        :gag-mode :goals
        (defthm app-assoc (equal (app (app x y) z) (app x (app y z)))))

     ; Same as just above, but turn off only the indicated parts of the summary.
     (with-output
        :on summary
        :summary (time rules)
        :gag-mode :goals  ; use gag-mode, with goal names printed
        (defthm app-assoc (equal (app (app x y) z) (app x (app y z)))))

     ; Same as specifying :off :all, but showing all output types:
     (with-output
      :off (error warning warning! observation prove proof-checker event expansion
                  summary proof-tree)
      :gag-mode nil
      (thm (equal (app (app x y) z) (app x (app y z)))))

     ; Same as above, but :stack :push says to save the current
     ; inhibit-output-lst, which can be restored in a subsidiary with-output call
     ; that specifies :stack :pop.
     (with-output
      :stack :push
      :off :all
      :gag-mode nil
      (thm (equal (app (app x y) z) (app x (app y z)))))

     General Form:
     (with-output :key1 val1 ... :keyk valk form)

where each :keyi is either :off, :on, :stack, :summary, or :gag-mode,
and vali is as follows.  If :keyi is :off or :on, then vali can be
:all, and otherwise is a symbol or non-empty list of symbols
representing output types that can be inhibited; see
SET-INHIBIT-OUTPUT-LST.  If :keyi is :gag-mode, then vali is one of
the legal values for :set-gag-mode.  If :keyi is :summary, then vali is
either :all or a true-list of symbols each of which belongs to the list
*summary-types*.  Otherwise :keyi is :stack, in which case :vali is
:push or :pop; for now assume that :stack is not specified (we'll
return to it below).  The result of evaluating the General Form above
is to evaluate form, but in an environment where output occurs as
follows.  If :on :all is specified, then every output type is turned on
except as inhibited by :off; else if :off :all is specified, then every
output type is inhibited except as specified by :on; and otherwise, the
currently-inhibited output types are reduced as specified by :on and
then extended as specified by :off.  But if :gag-mode is specified, then
before modifying how output is inhibited, gag-mode is set for the
evaluation of form as specified by the value of :gag-mode; see
SET-GAG-MODE.  If summary is among the output types that are turned
on (not inhibited), then if :summary is specified, the only parts of the
summary to be printed will be those specified by the value of :summary.
The correspondence should be clear, except perhaps that header refers to
the line containing only the word Summary, and value refers to the
value of the form printed during evaluation of sequences of events as
for progn and encapsulate.

Note that the handling of the :stack argument pays no attention to the
:summary argument.

Note: When the scope of with-output is exited, then all modifications
are undone, reverting gag-mode and the state of output inhibition to
those which were present before the with-output call was entered.

The :stack keyword's effect is illustrated by the following example,
where "(encapsulate nil)" may replaced by "(progn" without any change
to the output that is printed.

     (with-output
      :stack :push :off :all
      (encapsulate ()
        (defun f1 (x) x)
        (with-output :stack :pop (defun f2 (x) x))
        (defun f3 (x) x)
        (with-output :stack :pop :off warning (in-theory nil))
        (defun f4 (x) x)))

The outer with-output call saves the current output settings (as may
have been modified by earlier calls of set-inhibit-output-lst), by
pushing them onto a stack, and then turns off all output.  Each inner
with-output call temporarily pops that stack, restoring the starting
output settings, until it completes and undoes the effects of that pop.
Unless event output was inhibited at the top level (see
SET-INHIBIT-OUTPUT-LST), the following output is shown:

     Since F2 is non-recursive, its admission is trivial.  We observe that
     the type of F2 is described by the theorem (EQUAL (F2 X) X).

And then, if summary output was not inhibited at the top level, we get
the rest of this output:

     Summary
     Form:  ( DEFUN F2 ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

     Summary
     Form:  ( IN-THEORY NIL)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Note that the use of :off warning supresses a "Theory" warning for the
(in-theory nil) event, and that in no case will output be printed for
definitions of f1, f3, or f4, or for the encapsulate event itself.

The following more detailed explanation of :stack is intended only for
advanced users.  After :gag-mode is handled (if present) but before :on
or :off is handled, the value of :stack is handled as follows.  If the
value is :push, then state global inhibit-output-lst-stack is modified
by pushing the value of state global inhibit-output-lst onto the value
of state global inhibit-output-lst-stack, which is nil at the top
level.  If the value is :pop, then state global
inhibit-output-lst-stack is modified only if non-nil, in which case its
top element is popped and becomes the value of of state global
inhibit-output-lst.

Warning: With-output has no effect in raw Lisp, and hence is disallowed
in function bodies.  However, you can probably get the effect you want
as illustrated below, where <form> must return an error triple (mv erp
val state); see LD and see ERROR-TRIPLES.

     Examples avoiding with-output, for use in function definitions:

     ; Inhibit all output:
     (state-global-let*
      ((inhibit-output-lst *valid-output-names*))
      <form>)

     ; Inhibit all warning output:
     (state-global-let*
      ((inhibit-output-lst
        (union-eq (f-get-global 'inhibit-output-lst state)
                  '(warning warning!))))
      <form>)

Note that with-output is allowed in books.  See
EMBEDDED-EVENT-FORM.

THEORIES    sets of runes to enable/disable in concert

     Example: '((:definition app) ; or (:d app)
                (:executable-counterpart app)
                (:i app)
                rv
                (rv)
                assoc-of-app)

See:

Related topics other than immediate subtopics:

A theory is a list of "runic designators" as described below.  Each
runic designator denotes a set of "runes" (see RUNE) and by
unioning together the runes denoted by each member of a theory we
define the set of runes corresponding to a theory.  Theories are used
to control which rules are "enabled," i.e., available for automatic
application by the theorem prover.  There is always a "current" theory.
A rule is enabled precisely if its rune is an element of the set of
runes corresponding to the current theory.  At the top-level, the
current theory is the theory selected by the most recent in-theory
event, extended with the rule names introduced since then.  Inside the
theorem prover, the :in-theory hint (see HINTS) can be used to
select a particular theory as current during the proof attempt for a
particular goal.

Theories are generally constructed by "theory expressions."  Formally, a
theory expression is any term, containing at most the single free
variable world, that when evaluated with world bound to the current ACL2
world (see WORLD) produces a theory.  ACL2 provides various
functions for the convenient construction and manipulation of theories.
These are called "theory functions"(see THEORY-FUNCTIONS).  For
example, the theory function union-theories takes two theories and
produces their union.  The theory function universal-theory returns the
theory containing all known rule names as of the introduction of a
given logical name.  But a theory expression can contain constants,
e.g.,

     '(len (len) (:rewrite car-cons) car-cdr-elim)

and user-defined functions.  The only important criterion is that a
theory expression mention no variable freely except world and evaluate
to a theory.

More often than not, theory expressions typed by the user do not
mention the variable world.  This is because user-typed theory
expressions are generally composed of applications of ACL2's theory
functions.  These "functions" are actually macros that expand into
terms in which world is used freely and appropriately.  Thus, the
technical definition of "theory expression" should not mislead you into
thinking that interestng theory expressions must mention world; they
probably do and you just didn't know it!

One aspect of this arrangement is that theory expressions cannot
generally be evaluated at the top-level of ACL2, because world is not
bound.  To see the value of a theory expression, expr, at the
top-level, type

     ACL2 !>(LET ((WORLD (W STATE))) expr).

However, because the built-in theories are quite long, you may be sorry
you printed the value of a theory expression!

A theory is a true list of runic designators and to each theory there
corresponds a set of runes, obtained by unioning together the sets of
runes denoted by each runic designator.  For example, the theory
constant

        '(len (len) (:e nth) (:rewrite car-cons) car-cdr-elim)

corresponds to the set of runes

        {(:definition len)
         (:induction len)
         (:executable-counterpart len)
         (:executable-counterpart nth)
         (:elim car-cdr-elim)
         (:rewrite car-cons)} .

Observe that the theory contains five elements but its runic
correspondent contains six.  That is because runic designators can
denote sets of several runes, as is the case for the first designator,
len.  If the above theory were selected as current then the six rules
named in its runic counterpart would be enabled and all other rules
would be disabled.

We now precisely define the runic designators and the set of runes
denoted by each.  When we refer below to the "macro-aliases dereference
of" a symbol, symb, we mean the (function) symbol corresponding symb in
the macro-aliases-table if there is such a symbol, else symb itself;
see MACRO-ALIASES-TABLE.  For example, the macro-aliases
dereference of append is binary-append, and the macro-aliases
dereference of nth is nth.

     o A rune is a runic designator and denotes the singleton set
     containing that rune.

     o Suppose that symb is a symbol and symb' is the macro-aliases
     dereference of symb, where symb' is a function symbol introduced
     with a defun (or defuns) event.  Then symb is a runic designator
     and denotes the set containing the runes (:definition symb') and
     (:induction symb'), omitting the latter if no such induction rune
     exists (presumably because the definition of symb' is not singly
     recursive).

     o Suppose that symb is a symbol and symb' is the macro-aliases
     dereference of symb, where symb' is a function symbol introduced
     with a defun (or defuns) event.  Then (symb) is a runic designator
     and denotes the singleton set containing the rune
     (:executable-counterpart symb').

     o If symb is the name of a defthm (or defaxiom) event that
     introduced at least one rule, then symb is a runic designator and
     denotes the set of the names of all rules introduced by the named
     event.

     o If str is the string naming some defpkg event and symb is the
     symbol returned by (intern str "ACL2"), then symb is a runic
     designator and denotes the singleton set containing (:rewrite
     symb), which is the name of the rule stating the conditions under
     which the symbol-package-name of (intern x str) is str.

     o If symb is the name of a deftheory event, then symb is a runic
     designator and denotes the runic theory corresponding to symb.

     o Finally, suppose that symb is a symbol and symb' is the
     macro-aliases dereference of symb.  Then (:KWD symb . rest) is a
     runic designator if (:KWD' symb' . rest) is a rune, where :KWD is
     one of :d, :e, :i, or :t, and correspondingly :KWD' is
     :definition, :executable-counterpart, :induction, or
     :type-prescription, respectively.  In this case, (:KWD symb . rest)
     denotes the runic theory corresponding to the rune (:KWD' symb' .
     rest).

Note that including a function name, e.g., len, in the current theory
enables that function but does not enable the executable counterpart.
Similarly, including (len) or (:e len) enables the executable
counterpart but not the symbolic definition.  And including the name of
a proved lemma enables all of the rules added by the event.  Of course,
one can include explicitly the runes naming the rules in question and
so can avoid entirely the use of non-runic elements in theories.

Because a rune is a runic designator denoting the set containing that
rune, a list of runes is a theory and denotes itself.  We call such
theories "runic theories."  To every theory there corresponds a runic
theory obtained by unioning together the sets denoted by each
designator in the theory.  When a theory is selected as "current" it is
actually its runic correspondent that is effectively used.  That is, a
rune is enabled iff it is a member of the runic correspondent of the
current theory.  The value of a theory defined with deftheory is the
runic correspondent of the theory computed by the defining theory
expression.  The theory manipulation functions, e.g., union-theories,
actually convert their theory arguments to their runic correspondents
before performing the required set operation.  The manipulation
functions always return runic theories.  Thus, it is sometimes
convenient to think of (non-runic) theories as merely abbreviations for
their runic correspondents, abbreviations which are "expanded" at the
first opportunity by theory manipulation functions and the "theory
consumer" functions such as in-theory and deftheory.

ACTIVE-RUNEP    check that a rune exists and is enabled

     Example:
     (active-runep '(:rewrite left-to-right))

     General Form:
     (active-runep rune)

where rune has the shape of a rune.  This macro expands to an
expression using the variables ens and state, and returns non-nil when
the given rune exists and is enabled (according to the given "enabled
structure," ens, and the current logical world of the given state).
See THEORY-INVARIANT for how this macro can be of use.

CURRENT-THEORY    currently enabled rules as of logical name

     Examples:
     (current-theory :here)
     (current-theory 'lemma3)

See LOGICAL-NAME.

     General Form:
     (current-theory logical-name)

Returns the current theory as it existed immediately after the
introduction of logical-name provided it is evaluated in an environment
in which the variable symbol WORLD is bound to the current ACL2 logical
world, (w state).  Thus,

     ACL2 !>(current-theory :here)

will cause an (unbound variable) error while

     ACL2 !>(let ((world (w state))) (current-theory :here))

will return the current theory in world.

See THEORIES and see LOGICAL-NAME for a discussion of
theories in general and why the commonly used "theory functions" such
as current-theory are really macros that expand into terms involving
the variable world.

The theory returned by current-theory is in fact the theory selected by
the in-theory event most recently preceding logical name, extended by
the rules introduced up through logical-name.

You may experience a fencepost problem in deciding which logical name
to use.  Deflabel can always be used to mark unambiguously for future
reference a particular point in the development of your theory.  The
order of events in the vicinity of an encapsulate is confusing.  See
ENCAPSULATE.

This "function" is actually a macro that expands to a term mentioning
the single free variable world.  When theory expressions are evaluated
by in-theory or the :in-theory hint, world is bound to the current ACL2
world.

DISABLE    deletes names from current theory

     Example:
     (disable fact (fact) associativity-of-app)

     General Form:
     (disable name1 name2 ... namek)

where each namei is a runic designator; see THEORIES.  The
result is the theory that contains all the names in the current theory
except those listed.  Note that this is merely a function that returns
a theory.  The result is generally a very long list of runes and you
will probably regret printing it.

The standard way to "disable" a fixed set of names, is as follows; see
HINTS and see IN-THEORY.

     :in-theory (disable name1 name2 ... namek)    ; in a hint
     (in-theory (disable name1 name2 ... namek))   ; as an event
     (local ; often desirable, to avoid exporting from the current context
      (in-theory (disable name1 name2 ... namek)))

Note that all the names are implicitly quoted.  If you wish to disable
a computed list of names, lst, use the theory expression
(set-difference-theories (current-theory :here) lst).

E/D    enable/disable rules

The macro e/d creates theory expressions for use in in-theory hints and
events.  It provides a convenient way to enable and disable
simultaneously, without having to write arcane theory expressions.

     Examples:
     (e/d (lemma1 lemma2))          ; equivalent to (enable lemma1 lemma2)
     (e/d () (lemma))               ; equivalent to (disable lemma)
     (e/d (lemma1) (lemma2 lemma3)) ; Enable lemma1 then disable lemma2, lemma3.
     (e/d () (lemma1) (lemma2))     ; Disable lemma1 then enable lemma2.

     General Form:
     (e/d enables-0 disables-0 ... enables-n disables-n)

where each enables-i and disables-i is a list of runic designators; see
THEORIES, see ENABLE, and see DISABLE.

The e/d macro takes any number of lists suitable for the enable and
disable macros, and creates a theory that is equal to (current-theory
:here) after executing the following commands.

(in-theory (enable . enables-0)) (in-theory (disable . disables-0))
[etc.]  (in-theory (enable . enables-n)) (in-theory (disable .
disables-n))

ENABLE    adds names to current theory

     Example:
     (enable fact (fact) associativity-of-app)

     General Form:
     (enable name1 name2 ... namek)

where each namei is a runic designator; see THEORIES.  The
result is the theory that contains all the names in the current theory
plus those listed.  Note that this is merely a function that returns a
theory.  The result is generally a very long list of runes and you will
probably regret printing it.

The standard way to "enable" a fixed set of names, is as follows; see
HINTS and see IN-THEORY.

     :in-theory (enable name1 name2 ... namek)  ; in a hint
     (in-theory (enable name1 name2 ... namek)) ; as an event
     (local ; often desirable, to avoid exporting from the current context
      (in-theory (enable name1 name2 ... namek)))

Note that all the names are implicitly quoted.  If you wish to enable a
computed list of names, lst, use the theory expression (union-theories
(current-theory :here) lst).

EXECUTABLE-COUNTERPART-THEORY    executable counterpart rules as of logical name

     Examples:
     (executable-counterpart-theory :here)
     (executable-counterpart-theory 'lemma3)

See LOGICAL-NAME.

     General Form:
     (executable-counterpart-theory logical-name)

Returns the theory containing all the :executable-counterpart runes,
whether enabled or not, that existed immediately after logical-name was
introduced.  See the documentation for theories, logical-name,
executable-counterpart and function-theory.

You may experience a fencepost problem in deciding which logical name
to use.  Deflabel can always be used to mark unambiguously for future
reference a particular point in the development of your theory.  The
order of events in the vicinity of an encapsulate is confusing.  See
ENCAPSULATE.

This "function" is actually a macro that expands to a term mentioning
the single free variable world.  When theory expressions are evaluated
by in-theory or the :in-theory hint, world is bound to the current ACL2
world.

FUNCTION-THEORY    function symbol rules as of logical name

     Examples:
     (function-theory :here)
     (function-theory 'lemma3)

See LOGICAL-NAME.

     General Form:
     (function-theory logical-name)

Returns the theory containing all the :definition runes, whether
enabled or not, that existed immediately after logical-name was
introduced.  See the documentation for theories, logical-name and
executable-counterpart-theory.

You may experience a fencepost problem in deciding which logical name
to use.  Deflabel can always be used to mark unambiguously for future
reference a particular point in the development of your theory.  The
order of events in the vicinity of an encapsulate is confusing.  See
ENCAPSULATE.

This "function" is actually a macro that expands to a term mentioning
the single free variable world.  When theory expressions are evaluated
by in-theory or the :in-theory hint, world is bound to the current ACL2
world.

GROUND-ZERO    enabled rules in the startup theory

ACL2 concludes its initialization (boot-strapping) procedure by
defining the theory ground-zero; see THEORIES.  In fact, this
theory is just the theory defined by (current-theory :here) at the
conclusion of initialization; see CURRENT-THEORY.

Note that by evaluating the event

     (in-theory (current-theory 'ground-zero))

you can restore the current theory to its value at the time you started
up ACL2.

INCOMPATIBLE    declaring that two rules should not both be enabled

     Example:
     (theory-invariant (incompatible (:rewrite left-to-right)
                                     (:rewrite right-to-left)))

     General Form:
     (incompatible rune1 rune2)

where rune1 and rune2 are two specific runes.  The arguments are not
evaluated.  Invariant is just a macro that expands into a term that
checks that not both runes are enabled.  See THEORY-INVARIANT.

INTERSECTION-THEORIES    intersect two theories

     Example:
     (intersection-theories (current-theory :here)
                            (theory 'arith-patch))

     General Form:
     (intersection-theories th1 th2)

where th1 and th2 are theories (see THEORIES).  To each of the
arguments there corresponds a runic theory.  This function returns the
intersection of those two runic theories, represented as a list and
ordered chronologically.

This "function" is actually a macro that expands to a term mentioning
the single free variable world.  When theory expressions are evaluated
by in-theory or the :in-theory hint, world is bound to the current ACL2
world.

MINIMAL-THEORY    a minimal theory to enable

This theory (see THEORIES) enables only a few built-in
functions and executable counterparts.  It can be useful when you want
to formulate lemmas that rather immediately imply the theorem to be
proved, by way of a :use hint (see HINTS), for example as
follows.

     :use (lemma-1 lemma-2 lemma-3)
     :in-theory (union-theories '(f1 f2) (theory 'minimal-theory))

In this example, we expect the current goal to follow from lemmas
lemma-1, lemma-2, and lemma-3 together with rules f1 and f2 and some
obvious facts about built-in functions (such as the definition of
implies and the :executable-counterpart of car).  The :in-theory hint
above is intended to speed up the proof by turning off all inessential
rules.

RULE-NAMES    How rules are named.

     Examples:
     (:rewrite assoc-of-app)
     (:linear delta-aref . 2)
     (:definition length)
     (:executable-counterpart length)

See RUNE.

RUNE    a rule name

     Examples:
     (:rewrite assoc-of-app)
     (:linear delta-aref . 2)
     (:definition length)
     (:executable-counterpart length)

Background: The theorem prover is driven from a database of rules.  The
most common rules are :rewrite rules, which cause the simplifier to
replace one term with another.  Events introduce rules into the
database.  For example, a defun event may introduce runes for
symbolically replacing a function call by its instantiated body, for
evaluating the function on constants, for determining the type of a
call of the function, and for the induction scheme introduced upon
defining the function.  Defthm may introduce several rules, one for
each of the :rule-classes specified (where one rule class is specified
if :rule-classes is omitted, namely, :rewrite).

Every rule in the system has a name.  Each name is a structured object
called a "rune," which is short for "rule name".  Runes are always of
the form (:token symbol . x), where :token is some keyword symbol
indicating what kind of rule is named, symbol is the event name that
created the rule (and is called the "base symbol" of the rune), and x
is either nil or a natural number that makes the rule name distinct
from that of rules generated by other events or by other :rule-classes
within the same event.

For example, an event of the form

     (defthm name thm
       :rule-classes ((:REWRITE :COROLLARY term1)
                      (:REWRITE :COROLLARY term2)
                      (:ELIM    :COROLLARY term3)))

typically creates three rules, each with a unique rune.  The runes are

     (:REWRITE name . 1), (:REWRITE name . 2), and (:ELIM name).

However, a given formula may create more than one rule, and all rules
generated by the same :corollary formula will share the same rune.
Consider the following example.

     (defthm my-thm
       (and (equal (foo (bar x)) x)
            (equal (bar (foo x)) x)))

This is treated identically to the following.

     (defthm my-thm
       (and (equal (foo (bar x)) x)
            (equal (bar (foo x)) x))
       :rule-classes ((:rewrite
                       :corollary
                       (and (equal (foo (bar x)) x)
                            (equal (bar (foo x)) x)))))

In either case, two rules are created: one rewriting (foo (bar x)) to
x, and one rewriting (bar (foo x)) to x.  However, only a single rune
is created, (:REWRITE MY-THM), because there is only one rule class.
But now consider the following example.

     (defthm my-thm2
       (and (equal (foo (bar x)) x)
            (equal (bar (foo x)) x))
       :rule-classes ((:rewrite
                       :corollary
                       (and (equal (foo (bar x)) x)
                            (equal (bar (foo x)) x)))
                      (:rewrite
                       :corollary
                       (and (equal (foo (bar (foo x))) (foo x))
                            (equal (bar (foo (bar x))) (bar x))))))

This time there are four rules created.  The first two rules are as
before, and are assigned the rune (:REWRITE MY-THM . 1).  The other two
rules are similarly generated for the second :corollary, and are
assigned the rune (:REWRITE MY-THM . 2).

The function corollary will return the corollary term associated with a
given rune in a given world.  Example:

     (corollary '(:TYPE-PRESCRIPTION DIGIT-TO-CHAR) (w state))

However, the preferred way to see the corollary term associated with a
rune or a name is to use :pf; see PF.

The defun event creates as many as four rules.  (:definition fn) is the
rune given to the equality axiom defining the function, fn.
(:executable-counterpart fn) is the rune given to the rule for computing
fn on known arguments.  A type prescription rule may be created under
the name (:type-prescription fn), and an induction rule may be created
under the name (:induction fn).

Runes may be individually enabled and disabled, according to whether
they are included in the current theory.  See THEORIES.  Thus,
it is permitted to disable (:elim name), say, while enabling the other
rules derived from name.  Similarly, (:definition fn) may be disabled
while (:executable-counterpart fn) and the type prescriptions for fn
are enabled.

Associated with most runes is the formula justifying the rule named.
This is called the "corollary formula" of the rune and may be obtained
via the function corollary, which takes as its argument a rune and a
property list world.  Also see PF.  The corollary formula for
(:rewrite name . 1) after the defthm event above is term1.  The
corollary formulas for (:definition fn) and (:executable-counterpart
fn) are always identical: the defining axiom.  Some runes, e.g.,
(:definition car), do not have corollary formulas.  Corollary returns
nil on such runes.  In any case, the corollary formula of a rune, when
it is non-nil, is a theorem and may be used in the :use and :by hints.

Note: The system has many built in rules that, for regularity, ought to
have names but don't because they can never be disabled.  One such rule
is that implemented by the linear arithmetic package.  Because many of
our subroutines are required by their calling conventions to return the
justifying rune, we have invented the notion of "fake runes." Fake
runes always have the base symbol nil, use a keyword token that
includes the phrase "fake-rune", and are always enabled.  For example,
(:fake-rune-for-linear nil) is a fake rune.  Occasionally the system
will print a fake rune where a rune is expected.  For example, when the
linear arithmetic fake rune is reported among the rules used in a
proof, it is an indication that the linear arithmetic package was used.
However, fake runes are not allowed in theories, they cannot be enabled
or disabled, and they do not have associated corollary formulas.  In
short, despite the fact that the user may sometimes see fake runes
printed, they should never be typed.

SET-DIFFERENCE-THEORIES    difference of two theories

     Example:
     (set-difference-theories (current-theory :here)
                              '(fact (fact)))

     General Form:
     (set-difference-theories th1 th2)

where th1 and th2 are theories (see THEORIES).  To each of the
arguments there corresponds a runic theory.  This function returns the
set-difference of those two runic theories, represented as a list and
ordered chronologically.  That is, a rune is in the result iff it is in
the first runic theory but not in the second.

The standard way to "disable" a theory, lst, is: (in-theory
(set-difference-theories (current-theory :here) lst)).

This "function" is actually a macro that expands to a term mentioning
the single free variable world.  When theory expressions are evaluated
by in-theory or the :in-theory hint, world is bound to the current ACL2
world.

THEORY    retrieve named theory

     Example:
     (theory 'ground-zero)

In the example above, the theory returned is the one in force when ACL2
is started up (see GROUND-ZERO).

     General Form:
     (theory name)

where name is the name of a previously executed deftheory event
(otherwise a hard error occurs).  Returns the named theory.  See
THEORIES.

This "function" is actually a macro that expands to a term mentioning
the single free variable world.  When theory expressions are evaluated
by in-theory or the :in-theory hint, world is bound to the current ACL2
world.

THEORY-FUNCTIONS    functions for obtaining or producing theories

     Example Calls of Theory Functions:
     (universal-theory :here)
     (union-theories th1 th2)
     (set-difference-theories th1 th2)

The theory functions are documented individually:

Related topics other than immediate subtopics:

The functions (actually, macros) mentioned above are convenient ways to
produce theories.  (See THEORIES.) Some, like universal-theory,
take a logical name (see LOGICAL-NAME) as an argument and
return the relevant theory as of the time that name was introduced.
Others, like union-theories, take two theories and produce a new one.
See REDUNDANT-EVENTS for a caution about the use of logical
names in theory expressions.

Theory expressions are generally composed of applications of theory
functions.  Formally, theory expressions are expressions that involve,
at most, the free variable world and that when evaluated with world
bound to the current ACL2 world (see WORLD) return theories.
The "theory functions" are actually macros that expand into forms that
involve the free variable world.  Thus, for example (universal-theory
:here) actually expands to (universal-theory-fn :here world) and when
that form is evaluated with world bound to the current ACL2 world,
universal-theory-fn scans the ACL2 property lists and computes the
current universal theory.  Because the theory functions all implicitly
use world, the variable does not generally appear in anything the user
types.

UNION-THEORIES    union two theories

     Example:
     (union-theories (current-theory 'lemma3)
                     (theory 'arith-patch))

     General Form:
     (union-theories th1 th2)

where th1 and th2 are theories (see THEORIES).  To each of the
arguments there corresponds a runic theory.  This function returns the
union of those two runic theories, represented as a list and ordered
chronologically.

This "function" is actually a macro that expands to a term mentioning
the single free variable world.  When theory expressions are evaluated
by in-theory or the :in-theory hint, world is bound to the current ACL2
world.

UNIVERSAL-THEORY    all rules as of logical name

     Examples:
     (universal-theory :here)
     (universal-theory 'lemma3)

See LOGICAL-NAME.

     General Form:
     (universal-theory logical-name)

Returns the theory consisting of all the runes that existed immediately
after logical-name was introduced.  See THEORIES and see
LOGICAL-NAME.  The theory includes logical-name itself (if there is a
rule by that name).  (Note that since some events do not introduce
rules (e.g., defmacro, defconst or defthm with :rule-classes nil), the
universal-theory does not necessarily include a rune for every event
name.)  The universal-theory is very long and you will probably regret
printing it.

You may experience a fencepost problem in deciding which logical-name
to use.  Deflabel can always be used to mark unambiguously for future
reference a particular point in the development of your theory.  This
is convenient because deflabel does not introduce any rules and hence
it doesn't matter if you count it as being in the interval or not.  The
order of events in the vicinity of an encapsulate is confusing.  See
ENCAPSULATE.

This "function" is actually a macro that expands to a term mentioning
the single free variable world.  When theory expressions are evaluated
by in-theory or the :in-theory hint, world is bound to the current ACL2
world.

Also see CURRENT-THEORY.  Current-theory is much more commonly
used than universal-theory.  The former includes only the enabled runes
as of the given logical-name, which is probably what you want, while
the latter includes disabled ones as well.

TRACE    tracing functions in ACL2

ACL2 provides a trace utility, trace$, with corresponding reverse
operation untrace$.  These can be used without any dependence on the
underlying Lisp utility, and are the tracing utilities of choice in
ACL2; see TRACE$ and see UNTRACE$.

However, for advanced users we note that the underlying host Lisp may
also provide a trace utility, trace, and corresponding untrace.
Moreover, these have been modified in the case that the host Lisp is
GCL, Allegro CL, or CCL (OpenMCL), to provide limited support for
:entry, :exit, and perhaps :cond keywords, to hide certain large data
structures (world, enabled structure, rewrite constant), and to trace
executable counterparts.  See source files *-trace.lisp.  For the above
Lisps, you can invoke the original trace and untrace by invoking
old-trace and old-untrace, respectively, in raw Lisp rather than in the
normal ACL2 loop.

Related topics other than immediate subtopics:

BREAK-ON-ERROR    break when encountering a hard or soft error caused by ACL2

     General forms:
     (break-on-error t)    ; installs a trace causing a continuable error (break)
                           ;   when an error is invoked by ACL2.
     (break-on-error)      ; same as above
     (break-on-error :all) ; same as above, but even when inside the prover
     (break-on-error nil)  ; uninstall any above trace

(Break-on-error) generates a suitable trace of error functions.
Evaluate (trace$) after (break-on-error) if you want to see the
specific trace forms (which you can modify and then submit directly to
trace$, if you wish).  This trace should cause entry to the Lisp
debugger whenever ACL2 calls its error routines, except for certain
errors when inside the theorem prover, and also at those times if
option :all is supplied.

NOTE: For technical reasons, you may see some error messages more than
once.

Finally, note that you are welcome to define your own version of
break-on-error by modifying a copy of the source definition (search for
"(defmacro break-on-error" in ACL2 source file other-events.lisp).
Please feel free to send your version of break-on-error to the ACL2
implementors, for possible inclusion into ACL2.

Break-on-error is implmented using ACL2 trace$.  See TRACE! if
you want an explanation of the "TTAG NOTE" that is printed.

The argument, if supplied, is evaluated and must evaluate to t, nil, or
:all.

Also see SET-DEBUGGER-ENABLE for how to get raw-Lisp backtrace
information when an error occurs as a result of break-on-error, or even
of a raw Lisp error, by calling set-debugger-enable with argument :bt,
:bt-break, or :break-bt.  Note that for ACL2 errors (as opposed to raw
Lisp errors), i.e. errors affected by break-on-error, all three of
those keyword values are treated equivalently (and, all are ignored for
GCL; see SET-DEBUGGER-ENABLE).

CLOSE-TRACE-FILE    stop redirecting trace output to a file

     General Form:
     (close-trace-file) ; trace output is no longer redirected to a file

Output from trace$ normally goes to the screen, or more precisely,
standard-co.  It can be redirected to a file; see
OPEN-TRACE-FILE.  Use close-trace-file to redirect trace output to
standard-co.

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.

SET-TRACE-EVISC-TUPLE    set the trace evisc tuple

A trace evisc-tuple, which is set by this utility, provides a means to
restrict printing during tracing.  See EVISC-TUPLE for an
introduction to evisc-tuples; also see SET-EVISC-TUPLE and see
SET-IPRINT.

By default the ACL2 trace mechanism, trace$, automatically deals with
stobjs, the logical world, and certain other large structures.  See
TRACE$, in particular the documentation of trace$ option :hide.
However, even with that default behavior you may want to restrict what
is printed according to the print-level and print-length of an
evisc-tuple; see EVISC-TUPLE.

     Examples:

     ; Set trace evisc tuple to a standard value, using current Lisp *print-level*
     ; and *print-length* variables:
     (set-trace-evisc-tuple t state)

     ; Set trace evisc tuple back to its default:
     (set-trace-evisc-tuple nil state)

     ; Set trace evisc tuple to restrict print-level to 3 and print-length to 4,
     ; while hiding the logical world and suitably printing stobjs even if trace$
     ; option ``:hide nil'' is used.  (Note: calling trace-evisceration-alist
     ; directly requires removing this function as `untouchable', which requires a
     ; trust tag; see REMOVE-UNTOUCHABLE.)
     (set-trace-evisc-tuple
      (evisc-tuple 3 4 (trace-evisceration-alist state) nil)
      state)

     General Forms:

     (set-trace-evisc-tuple nil state) ; trace evisc-tuple set to standard value
     (set-trace-evisc-tuple   t state) ; trace evisc-tuple set to hide the logical
                                       ;   world and deal with stobjs even when
                                       ;   trace$ option ``:hide nil'' is supplied
     (set-trace-evisc-tuple evisc-tuple state)
                                       ; tracing set to use indicated evisc-tuple

See TRACE$ for a discussion of ACL2 tracing.  The evisc-tuple
used by that trace utility is the one last installed by
set-trace-evisc-tuple (or by set-evisc-tuple for the trace-evisc-tuple)
-- initially to the default of nil -- unless overriden by trace option
:evisc-tuple.

*Remark*.  If you use value t, then ACL2 will ensure that the logical
world and stobjs are kept up-to-date in the trace evisc-tuple.

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

     Example:
     (trace! (fact :native t :entry *foo*))

     General Form:
     (trace! spec1 ... specn)

where the fni are suitable arguments to trace$.

Trace! is a version of trace$ that avoids the need for an
already-active trust tag (or "ttag"; see DEFTTAG), as explained
below.  See TRACE$ for when a trust tag can be necessary.

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

The evaluation of a trace! form 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.

Because of the active trust tag, it is possible to do things with trace!
that are useful but without logical justification.  Below is an example
of how to use trace! to cause a function call to change state, even
though the function does not take state as a parameter.

     ACL2 !>(defun fact (n)
              (declare (xargs :guard (natp n) :verify-guards nil))
              (if (zp n)
                  1
                (* n (fact (1- n)))))

     The admission of FACT 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 FACT is described by the
     theorem (AND (INTEGERP (FACT N)) (< 0 (FACT N))).  We used the :compound-
     recognizer rule ZP-COMPOUND-RECOGNIZER and primitive type reasoning.

     Summary
     Form:  ( DEFUN FACT ...)
     Rules: ((: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)
      FACT
     ACL2 !>(defun update-foo (n value state)
              (declare (xargs :stobjs state :verify-guards nil))
              (assign foo (cons (cons n value) (@ foo))))

     Since UPDATE-FOO is non-recursive, its admission is trivial.  We observe
     that the type of UPDATE-FOO is described by the theorem
     (AND (CONSP (UPDATE-FOO N VALUE STATE))
          (TRUE-LISTP (UPDATE-FOO N VALUE STATE))).
     We used primitive type reasoning.

     (UPDATE-FOO * * STATE) => (MV * * STATE).

     Summary
     Form:  ( DEFUN UPDATE-FOO ...)
     Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      UPDATE-FOO
     ACL2 !>(trace! (fact :exit (update-foo n value state)))

     TTAG NOTE: Adding ttag :TRACE! from the top level loop.
      ((FACT :EXIT (UPDATE-FOO N VALUE STATE)))
     ACL2 !>(assign foo nil)
      NIL
     ACL2 !>(fact 7)
     1> (ACL2_*1*_ACL2::FACT 7)
       2> (ACL2_*1*_ACL2::FACT 6)
         3> (ACL2_*1*_ACL2::FACT 5)
           4> (ACL2_*1*_ACL2::FACT 4)
             5> (ACL2_*1*_ACL2::FACT 3)
               6> (ACL2_*1*_ACL2::FACT 2)
                 7> (ACL2_*1*_ACL2::FACT 1)
                   8> (ACL2_*1*_ACL2::FACT 0)
                   <8 NIL
                 <7 NIL
               <6 NIL
             <5 NIL
           <4 NIL
         <3 NIL
       <2 NIL
     <1 NIL
     5040
     ACL2 !>(@ foo)
     ((7 . 5040)
      (6 . 720)
      (5 . 120)
      (4 . 24)
      (3 . 6)
      (2 . 2)
      (1 . 1)
      (0 . 1))
     ACL2 !>(verify-guards fact)

     Computing the guard conjecture for FACT....

     The guard conjecture for FACT is trivial to prove, given the :compound-
     recognizer rules NATP-COMPOUND-RECOGNIZER and ZP-COMPOUND-RECOGNIZER,
     primitive type reasoning and the :type-prescription rule FACT.  FACT
     is compliant with Common Lisp.

     Summary
     Form:  ( VERIFY-GUARDS FACT)
     Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
             (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
             (:FAKE-RUNE-FOR-TYPE-SET NIL)
             (:TYPE-PRESCRIPTION FACT))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 !>(assign foo nil)
      NIL
     ACL2 !>(fact 7)
     1> (ACL2_*1*_ACL2::FACT 7)
       2> (FACT 7)
         3> (FACT 6)
           4> (FACT 5)
             5> (FACT 4)
               6> (FACT 3)
                 7> (FACT 2)
                   8> (FACT 1)
                     9> (FACT 0)
                     <9 NIL
                   <8 NIL
                 <7 NIL
               <6 NIL
             <5 NIL
           <4 NIL
         <3 NIL
       <2 NIL
     <1 NIL
     5040
     ACL2 !>(@ foo)
     ((7 . 5040)
      (7 . 5040)
      (6 . 720)
      (5 . 120)
      (4 . 24)
      (3 . 6)
      (2 . 2)
      (1 . 1)
      (0 . 1))
     ACL2 !>(trace! (fact :exit (progn (update-foo n value state)
                                       (cons traced-fn values))))

     TTAG NOTE: Adding ttag :TRACE! from the top level loop.
      ((FACT :EXIT (PROGN (UPDATE-FOO N VALUE STATE)
                          (CONS TRACED-FN VALUES))))
     ACL2 !>(assign foo nil)
      NIL
     ACL2 !>(fact 7)
     1> (ACL2_*1*_ACL2::FACT 7)
       2> (FACT 7)
         3> (FACT 6)
           4> (FACT 5)
             5> (FACT 4)
               6> (FACT 3)
                 7> (FACT 2)
                   8> (FACT 1)
                     9> (FACT 0)
                     <9 (FACT 1)
                   <8 (FACT 1)
                 <7 (FACT 2)
               <6 (FACT 6)
             <5 (FACT 24)
           <4 (FACT 120)
         <3 (FACT 720)
       <2 (FACT 5040)
     <1 (ACL2_*1*_ACL2::FACT 5040)
     5040
     ACL2 !>(@ foo)
     ((7 . 5040)
      (7 . 5040)
      (6 . 720)
      (5 . 120)
      (4 . 24)
      (3 . 6)
      (2 . 2)
      (1 . 1)
      (0 . 1))
     ACL2 !>

Finally, we remark that the use trace! can cause errors in situations
where tracing is automatically suspended and re-introduced.  This is
likely to be a rare occurrence, but consider the following example.

     (trace! (lexorder :native t :multiplicity 1))
     (certify-book "foo" 0 t)

If the certify-book causes compilation, you may see an error such as the
following.

     ACL2 Error in (CERTIFY-BOOK "foo" ...):  The keyword :NATIVE cannot
     be used in a trace spec unless there is an active trust tag.  The trace
     spec (LEXORDER :NATIVE T :MULTIPLICITY 1) is thus illegal.  Consider
     using trace! instead.  The complete list of keywords that require a
     trust tag for use in a trace spec is: (:NATIVE :DEF :MULTIPLICITY).

This error is harmless.  The function will appear, when calling
(trace$), to remain traced, but in fact there will be no tracing
behavior, so you may want to call untrace$ on the function symbol in
question.

TRACE$    trace function evaluations

     Examples:
     (trace$ foo bar)     ; trace foo and bar
     (trace$)             ; return current trace info (no new tracing specified)
     (trace$ (foo :entry  ; trace foo, printing first actual parameter upon entry
                  (car arglist)))
     (trace$ (foo :exit   ; trace foo, using fmt to print upon exit
                  (:fmt (msg "Exiting FOO with ~x0"
                             value))))
     (trace$ (foo :native t))

     General Forms:
     (trace$ spec1 spec2 ... specn) ; n >= 1
     (trace$)

where the speci are trace specs, as described below.

Trace$ installs alternate code for the indicated functions that prints
information upon entry to, and exit from, calls of the functions.  For
an alternate tracing utility used for educational purposes in ACL2s
(`http://acl2s.ccs.neu.edu/acl2s/doc/'), see community book
books/misc/trace-star.lisp.

From a logical perspective all trace printing is a fiction.  (But see
TRACE! for a way to get around this and modify state.)  For a
related fiction, see CW.  (Trace$) returns the list of
currently-active trace specs, while the application of trace$ to at
least one argument returns the list of its arguments that are
successfully acted on.

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

See UNTRACE$ for how to undo the effect of trace$.  Also see
TRACE for mention of modifications made to raw Lisp trace,
which is accessible (as described below) using the :native keyword.

Note that when trace$ is applied to a function without option :native,
that function's declarations and documentation are discarded.

Next, we introduce tracing with some examples.  After that, we provide
reference documentation for individual trace options allowed in a trace
spec.  Note that although our example focuses on user-defined
functions, trace$ can also be applied to built-in functions, though
perhaps only system hackers should take advantage of this observation.

We begin by illustrating the simplest sort of trace spec: a function
symbol.  For example, the form (trace$ foo bar) directs the tracing of
functions foo and bar by virtue of the two trace specs foo and bar.  We
can see tracing in action by first defining:

     (defun f (x)
       (cons x x))

     (defun g (x)
       (list (f x) 3))

The following log then illustrates tracing of these two functions.
Notice that before guards have been verified, the so-called "*1*"
functions (sometimes called "executable counterpart functions" or "logic
functions") are called but the corresponding raw Lisp functions are
not; but after guard verification of f, the raw Lisp counterpart of f is
indeed called.  (See GUARD and see
GUARD-EVALUATION-EXAMPLES-LOG.)

     ACL2 !>(trace$ f g)
      ((F) (G))
     ACL2 !>(g 7)
     1> (ACL2_*1*_ACL2::G 7)
       2> (ACL2_*1*_ACL2::F 7)
       <2 (ACL2_*1*_ACL2::F (7 . 7))
     <1 (ACL2_*1*_ACL2::G ((7 . 7) 3))
     ((7 . 7) 3)
     ACL2 !>(verify-guards f)

     Computing the guard conjecture for F....

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

     Summary
     Form:  ( VERIFY-GUARDS F)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      F
     ACL2 !>(g 7)
     1> (ACL2_*1*_ACL2::G 7)
       2> (ACL2_*1*_ACL2::F 7)
         3> (F 7)
         <3 (F (7 . 7))
       <2 (ACL2_*1*_ACL2::F (7 . 7))
     <1 (ACL2_*1*_ACL2::G ((7 . 7) 3))
     ((7 . 7) 3)
     ACL2 !>

The following example introduces trace specs other than function
symbols.  Consider the following definition.

     (defun fact (n)
       (declare (xargs :guard (natp n)))
       (if (zp n)
           1
         (* n (fact (1- n)))))

The following log illustrates the use of trace options :cond (condition
for entering trace), :entry (what to print on entry), and :exit (what
to print on exit).  The reason for two calls on argument 4 is that we
are seeing such calls for the executable counterpart of fact and also
its raw Lisp function.

     ACL2 !>(trace$ (fact :cond (evenp (car arglist))
                          :entry (cons 'factorial-call arglist)
                          :exit (car values)))
      ((FACT :COND (EVENP (CAR ARGLIST))
             :ENTRY (CONS 'FACTORIAL-CALL ARGLIST)
             :EXIT (CAR VALUES)))
     ACL2 !>(fact 4)
     1> (FACTORIAL-CALL 4)
       2> (FACTORIAL-CALL 4)
         3> (FACTORIAL-CALL 2)
           4> (FACTORIAL-CALL 0)
           <4 1
         <3 2
       <2 24
     <1 24
     24
     ACL2 !>

Notice that VALUES above is the list of all values returned, which is a
one-element list unless mv return is used, as illustrated in the
following example, after defining: (defun two-vals (x) (mv x 7)).

     ACL2 !>(trace$ two-vals)
      ((TWO-VALS))
     ACL2 !>(two-vals 3)
     1> (ACL2_*1*_ACL2::TWO-VALS 3)
     <1 (ACL2_*1*_ACL2::TWO-VALS 3 7)
     (3 7)
     ACL2 !>(verify-guards two-vals)

     Computing the guard conjecture for TWO-VALS....

     The guard conjecture for TWO-VALS is trivial to prove, given the :executable-
     counterpart of CONS.  TWO-VALS is compliant with Common Lisp.

     Summary
     Form:  ( VERIFY-GUARDS TWO-VALS)
     Rules: ((:EXECUTABLE-COUNTERPART CONS))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      TWO-VALS
     ACL2 !>(two-vals 3)
     1> (ACL2_*1*_ACL2::TWO-VALS 3)
       2> (TWO-VALS 3)
       <2 (TWO-VALS 3 7)
     <1 (ACL2_*1*_ACL2::TWO-VALS 3 7)
     (3 7)
     ACL2 !>

We now document all of the options that may appear in a trace spec.  A
trace spec with options is of the form

     (fn :kwd1 val1 :kwd2 val2 ... :kwdn valn)

and here we document each legal keyword :kwdi and corresponding expected
value vali.  Note that trace$ is intended primarily for functions
defined in the ACL2 command loop (see LP).  If you want to
trace a function that defined in raw Lisp, then you can use option
:native (see below), but then many other trace$ options will not be
available to you: all of them except :multiplicity and :native itself
will be passed directly to the trace utility of the underlying Common
Lisp.

:COND, :ENTRY, and :EXIT

*Introduction*.  For each of these three options, the value is a
(user-level) term, except that for :entry and :exit the value can be of
the form (:fmt u), where u is a user-level term.  We skip this latter
case for now and return to it later.  Then the indicated term is
evaluated as indicated in the next paragraph, and if the :cond term is
omitted or evaluates to non-nil, then the value of the :entry term is
printed on entry and the value of the :exit term is printed on exit.  By
default, where :entry is omitted or is specified as nil, the value
printed for :entry is the list obtained by consing the calling function
symbol onto the list of actual parameters: in the notation described
below, this is (cons TRACED-FN ARGLIST).  Similarly, the default for
printing at the exit of the function call, i.e. where :exit is omitted
or is specified as nil, is (cons TRACED-FN VALUES) where VALUES is the
list of values returned as described below.

In the evaluations of the term described below upon a call of fn, each
formal parameter of the definition of fn will be bound to the
corresponding actual of the call, the variable ARGLIST will be bound to
the list of actuals, and the variable TRACED-FN will be bound to the
function being called (either fn or its executable counterpart function;
see above).  Additionally in the case of :exit, the variable VALUES
will be bound to the multiple values returned (thus, a one-element list
if mv is not used in the return).  Also for :exit, we bind VALUE to the
logical value returned, i.e., to the suitable list of values returned
in the mv case and otherwise to the single value returned.  So in the
mv case, VALUE is the same as VALUES, and otherwise VALUE is (car
VALUES).  Other than these variables and STATE, no other variable may
occur in the term, whose value must be a single non-stobj value, unless
there is an active trust tag (see DEFTTAG).

Now suppose fn is called.  First: If :cond is supplied and the result
of evaluating the :cond term is nil, then no tracing is done.
Otherwise tracing proceeds as follows.  First the :entry form is
evaluated, and the result is printed.  Then the call of fn is evaluated.
Finally the :exit term is evaluated and the result is printed.  As
indicated above, the default for the :entry term if omitted or
explicitly nil is (cons TRACED-FN ARGLIST), and the default for the
:exit term if omitted or explicitly nil is (cons TRACED-FN VALUES).

Note that if the function has a formal named ARGLIST, then ARGLIST will
nevertheless refer to the entire list of formals, not the single formal
named ARGLIST; similarly for TRACED-FN, and additionally for VALUE and
VALUES in the case of :exit.

As mentioned above, for each of :entry and :exit, a value of nil
specifies the default behavior.  If you really want a value of nil, use
a non-nil form that evaluates to nil, for example (car nil) or 'nil.
However, for :cond a value of nil means what it says: do not evaluate
the :entry or :exit forms.

Finally we discuss the case that the :entry or :exit term is of the
form (:fmt u).  In these cases, the term u is evaluated as described
above to produce a value, say msg, but instead of printing msg
directly, ACL2 calls fmt1 using the string "~@0" and the alist that
binds just character #\0 to msg.  The following example illustrates
this point, where fact is defined as above.  Also see FMT.
Note that (msg string . vals) produces a value suitable for a "~@"
directive to the fmt family of print functions.

     ACL2 !>(trace$
             (fact
              :entry (:fmt (msg "Tracing ~x0 on ~x1" traced-fn arglist))
              :exit (car values)))
      ((FACT :ENTRY (:FMT (MSG "Tracing ~x0 on ~x1" TRACED-FN ARGLIST))
             :EXIT (CAR VALUES)))
     ACL2 !>(fact 3)
     1> Tracing ACL2_*1*_ACL2::FACT on (3)
       2> Tracing FACT on (3)
         3> Tracing FACT on (2)
           4> Tracing FACT on (1)
             5> Tracing FACT on (0)
             <5 1
           <4 1
         <3 2
       <2 6
     <1 6
     6
     ACL2 !>

*ADVANCED OPTIONS* (alphabetical list)

:COMPILE

The tracing of fn installs a substitute definition of fn that prints
trace information.  If the :compile option is omitted or has value
:same, then the new definition will be compiled if and only if the
existing definition is already compiled.  Otherwise, the new definition
will be compiled exactly when the value of :compile is not nil.

:DEF, :MULTIPLICITY

ACL2's trace$ mechanism often needs to know the number of outputs of a
traced function, in the sense of mv.  If you trace a function that was
not defined inside the ACL2 loop (hence you are using the :native
option), or if you provide an alternative definition using option :def
(see below) and the new definition changes the number of values
returned, then a natural number value for :multiplicity informs the
trace utility of the number of expected outputs of the function being
traced.  In the case that :native is supplied, the effect of a non-nil
:multiplicity value depends on the host Lisp.  In the case of Lisps for
which ACL2 uses the built-in Lisp mechanism for returning multiple
values (see MV), which are CCL and threaded SBCL as of June,
2010, :multiplicity is not needed and is ignored with :native t.  For
GCL and Allegro CL, :multiplicity is used to generate a suitable :exit
form if the :exit keyword was not already supplied.  For the other
Lisps, the :multiplicity value is treated essentially as 1 whether it
is supplied or not, because we do not know how to pass suitable
information based on this value to the host Lisp's built-in tracing
mechanism.

Note that even supplying a :multiplicity option does not change the
meaning of the variable values.  See the discussion of :native below.

A useful option can be to supply a definition as the value of :def.
(Again, note that if :native is used, then all options other than
:multiplicity are passed directly to the underlying Lisp; in particular,
:def will have no effect with :native except in the unlikely case that
the raw Lisp provides some sort of support for :def.)  Note that this
definition should be like a defun form, but without the leading defun
symbol; and it should define the function symbol being traced, with the
same formal parameter list.  However, tracing of the so-called
"executable counterpart" of a function (sometimes referred to as the
"*1* function", for evaluation in the ACL2 loop; see Guards for
related discussion) is not sensitive to the :def option; rather, if a
function has an executable counterpart then that executable counterpart
is traced.

:EVISC-TUPLE

The printing described above is, by default, done using the current
default trace evisc-tuple, which can be set using set-trace-evisc-tuple
(for the shape of this tuple, see EVISC-TUPLE); see
SET-TRACE-EVISC-TUPLE.  This tuple is based by default on the raw
Lisp variables *print-level* and *print-length*, and will hide the ACL2
world and handle stobjs appropriately.  You may override this default
by supplying an evisc tuple with the :evisc-tuple argument in your
trace spec.  Be careful to supply a valid evisc-tuple, or you may get a
raw Lisp error!

A special value, :print, is useful if you are doing system hacking that
can produce objects that are not valid ACL2 objects, such as raw Lisp
arrays or objects in supporting packages not visible in the ACL2
read-eval-print loop.  If you supply :evisc-tuple :print, then the
printing described above will be done with raw Lisp printing rather
than ACL2 printing: specifically, with (format *trace-output* "s%" x),
where x is the value to be printed.

A second special value for :evisc-tuple, :no-print, avoids printing the
values of the :entry and :exit forms (or their defaults, if not
specified).  This option is of use for side effects; for an example see
community book books/misc/wet.lisp.

Note that if :evisc-tuple X is supplied, then the form X will be
evaluated before the function body is entered.  You can thus pull some
tricks to print extra information before the :entry form is evaluated,
for example as follows for a factorial function, fact.

     ACL2 !>(trace$ (fact :evisc-tuple
                          (prog2$ (cw "~|**** HERE IS CW ****~|")
                                  nil)))
      ((FACT :EVISC-TUPLE (PROG2$ (CW "~|**** HERE IS CW ****~|")
                                  NIL)))
     ACL2 !>(fact 3)
     **** HERE IS CW ****
     1> (ACL2_*1*_ACL2::FACT 3)
     **** HERE IS CW ****
       2> (ACL2_*1*_ACL2::FACT 2)
     **** HERE IS CW ****
         3> (ACL2_*1*_ACL2::FACT 1)
     **** HERE IS CW ****
           4> (ACL2_*1*_ACL2::FACT 0)
           <4 (ACL2_*1*_ACL2::FACT 1)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 6)
     6
     ACL2 !>

:FORMALS

Normally ACL2 can figure out the formals for a given function.  This is
always the case for functions defined in the ACL2 command loop and when
option :def is supplied.  If neither of these cases applies then you can
still trace a function (even without using the :native option) by
supplying option :notinline :fncall, but you will still need to supply
the list of formal parameters.  The value of the :formals option should
be the list of formals in this case.

:HIDE

The default value for this advanced option is t, which causes stobjs
and the logical world to be printed as single symbols, along with
certain large structures of interest to developers (rewrite contants,
enabled structures, and event and command index structures).  If
however the value nil is supplied, then this default behavior is
defeated.  In that case, you can still arrange to print the logical
world as a symbol and to print stobjs without breaking the trace
printing: see SET-TRACE-EVISC-TUPLE for how to do this
globally, or similarly use the :evisc-tuple option to trace$ to do this
with a single trace spec.  Note however that with value nil specified
for :hide, such use of an evisc-tuple will not deal properly with local
stobjs (see WITH-LOCAL-STOBJ) or the aforementioned large
structures other than the logical world.

:NATIVE

If :native is supplied with a non-nil value, then the trace spec is
passed to the native Lisp trace (after removing the :native option).  A
trust tag (see DEFTTAG) is required in order to use this
option, because no syntactic check is made on the :cond, :entry, or
:exit forms - arbitrary raw Lisp may occur in them!

Note that by "native Lisp trace" we mean the currently installed trace.
As discussed briefly elsewhere (see TRACE), ACL2 has modified
that trace to be more useful if the underlying host Lisp is GCL,
Allegro CL, or CCL (OpenMCL).  If you need the original trace utility
supplied for those Lisps, quit the ACL2 loop with :q and call old-trace
and old-untrace in raw Lisp where you would otherwise call trace and
untrace.  Note that the original trace utility supplied with a given
Lisp will not hide the ACL2 logical world or give special treatment to
stobjs.

It is important to understand that if :native t is specified, then all
other options are interpreted by the native Lisp trace.  For example,
that trace probably has no understanding of the use of :fmt described
above for :entry or :exit.  Indeed, the native trace may not even accept
any of :cond, :entry or :exit, let alone any of the advanced options!
Moreover, if :native t is specified, then even a :multiplicity option
does not provide the meaning of the variable values that one might
desire.  In GCL for example, in the case of an mv return of a function
defined only in raw Lisp (not in ACL2), this variable will be bound to
a list containing only the first result.

:NOTINLINE

By default, a new definition installed by trace$ will include a
notinline declaration so that recursive calls will always be traced.  To
avoid this declaration, supply value nil.

A special value for :notinline, :fncall, will cause the traced function
to call its original definition.  Without this special value, the new
installed definition for the traced function will include the body of
the original definition.  This :fncall behavior is the default only in
the following cases:

     o for functions whose definitions are built into ACL2;

     o for functions that have been added (using a trust tag, an
     advanced feature, so most users can probably ignore this case) to
     either of the state global variables program-fns-with-raw-code or
     logic-fns-with-raw-code;

     o (`HONS' extension only; see HONS-AND-MEMOIZATION) for
     memoized functions.

The legal values for :notinline are t (the default for other than the
cases displayed above), nil, and :fncall.  (Except: For the 'HONS'
extension, only :fncall is legal.)

*Remarks*.

(1) If some of the given trace specs have errors, then trace$ will
generally print error messages for those but will still process those
that do not have errors.  The value returned will indicate the trace
specs that were processed successfully.

(2) If you certify or include a book that redundantly defines a
function that is currently traced, then tracing behavior may disappear
if a compiled definition is installed for the function or its
in-the-logic (so-called `*1*') counterpart.

(3) Some predefined functions are called during tracing.  In order to
avoid infinite loops, such calls of traced predefined functions will be
made using the original predefined functions, not using their code
installed by trace$.

UNTRACE$    untrace functions

     Examples:
     (untrace$)         ; untrace all functions previously
                        ; traced (e.g. with trace$ or trace!)
     (untrace$ foo bar) ; as above, except only untrace foo and bar

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

where the fni were previously traced (e.g. with trace$ or trace!).

Untrace$ undoes the effect of trace$.  See TRACE$.  The value
returned by untrace$ gives the list of functions for which tracing is
being removed.

WET    evaluate a form and print subsequent error 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.