This is documentation for ACL2 Version 3.3
Copyright (C) 2007  University of Texas at Austin

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

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

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

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

NOTE-3-0-1(R)    ACL2 Version  3.0.1(r) (August, 2006) Notes

No significant changes have been made since Version  3.0 for support of
non-standard analysis in particular.

Please also see NOTE-3-0-1 for changes to Version  3.0.1 of
ACL2.

NOTE-3-0-2    ACL2 Version  3.0.2 (December, 2006) Notes

NOTE!  New users can ignore these release notes, because the
documentation has been updated to reflect all changes that are recorded
here.

Fixed soundness bugs in the handling of primitive function pkg-witness,
and improved its documentation.  (The executable counterpart returned an
incorrect default value, and the axiom
symbol-package-name-pkg-witness-name needed pkg-name to be other than
"" in order to avoid the default value of "ACL2".)  As fallout, a new
built-in :forward-chaining rule,
symbol-package-name-of-symbol-is-not-empty-string, now asserts that the
symbol-package-name of a symbol is never "".  Thanks to Mike Gordon for
bringing these soundness bugs to our attention by attempting to prove
translations of ACL2 axioms in HOL4.

Fixed a soundness bug in linear arithmetic, due to incomplete tracking
of forced assumptions while deriving inequalities.  Thanks to Robert
Krug for providing a fix and a proof of nil before the fix.

Fixed a soundness bug in the redundancy criterion for defun events,
which has been modified; see REDUNDANT-EVENTS.  This bug is
illustrated below.  Thanks to Peter Dillinger and Jared Davis for
contributions to an email thread that led us to discover this bug.  The
solution is that for a definition to be redundant with an earlier
definition, ACL2 no longer ignores :measure xargs except when skipping
proofs (e.g., during include-book).  However, a new "measure", (:? v1
... vk), is supported, for specifying a measured subset of the set of
formals, i.e., a set of formals that serves as the set of parameters
for some valid measure.

     (encapsulate
      ()

      (local (defun foo (x y)
               (declare (xargs :measure (acl2-count y)))
               (if (and (consp x) (consp y))
                   (foo (cons x x) (cdr y))
                 y)))

     ; So the following is redundant -- but it guesses a measure
     ; of (acl2-count x), which isn't right!
      (defun foo (x y)
        (if (and (consp x) (consp y))
            (foo (cons x x) (cdr y))
          y)))

     ; end of encapsulate

     ; Now we prove a non-theorem by exploiting the bug above,
     ; erroneously replacing formal y by a constant in the induction
     ; scheme hinted below.  (This should not be allowed, as y should be
     ; labeled as a measured formal.)

     (defthm bad
       (atom x)
       :rule-classes nil
       :hints (("Goal" :induct (foo x '(3)))))

     ; It's easy to get a contradiction by instantiating the
     ; non-theorem just above.
     (defthm contradiction
       nil
       :rule-classes nil
       :hints (("Goal" :use ((:instance bad (x '(7)))))))

Fixed a bug in :pl and the proof-checker's show-rewrites (sr) command
that was causing a Lisp break.  For :pl, also improved the display of
unifying substitutions, modified output to take binding hypotheses
(equal var term) into account properly, and arranged for inclusion of
meta rules that modify the given term.  Thanks to Eric Smith for
bringing these issues to our attention.

Introduced new utilities for undoing commands, :ubu and :ubu!, which
are analogous to :ubt and :ubt!  (respectively) except that they only
undo back up to, but not including, the indicated command.

Fixed a performance bug, pointed out by Eric Smith, that was negating
efforts made for the preceding release to avoid computation for
disabled warnings.

Added time$ and value-triple to *acl2-exports*.  Thanks to Bob Boyer
and Erik Reeber (respectively) for bringing these issues to our
attention.

Improved the automatic proclaiming of function types for GCL and
OpenMCL, specifically to use an output format consistent with the
Common Lisp spec.  Thanks to Bob Boyer for bringing this issue to our
attention.

Added books/misc/transfinite.lisp, which deals with transfinite
induction in ACL2.  Thanks to Eric Smith for contributing this book.

Added books/misc/process-book-readme.lisp to the distribution.  Thanks
to Sandip Ray for pointing out its omission.

Added contributions books/concurrent-programs/bakery/ and
books/concurrent-programs/german-protocol/.  These contributions can be
used as tutorials, especially by new ACL2 users, for learning how to
model concurrent protocols in ACL2 and the steps involved in reasoning
about their correctness.  Thanks to Sandip Ray for these contributions.
See the Readme.lsp files in these directories.

Theory invariants may now involve the variable ENS instead of the
variable THEORY.  The practical effect of this change is that any
expression of the form (MEMBER-EQUAL rune THEORY) occurring in a
theory-invariant expression should be replaced by (ACTIVE-RUNEP rune).
See THEORY-INVARIANT.  Thanks to Eric Smith and Dave Greve for
pointing out an inefficiency in the handling of theory invariants that
led to this change, which can speed up their handling by orders of
magnitude on large examples, and to Eric for testing this change and
pointing out problems with an early implementation of it.

Theory invariants (see THEORY-INVARIANT) are no longer checked
on theories defined by deftheory events.  After all, one can define a
theory with deftheory that is not intended to be used as the current
theory, but rather is intended to be combined with other theories (see
THEORY-FUNCTIONS).  Thanks to Eric Smith for bringing this
issue to our attention.

Theory-invariant errors had been reported with very little detail when
warnings were inhibited.  This problem has been fixed; thanks to Eric
Smith for bringing it to our attention and providing an example.  We
have also improved the handling of redundancy for theory-invariant
events.

The macro defun-sk now has a new optional keyword, rewrite, that can be
used to change the form of the :rewrite rule generated when the
quantifier is forall.  Thanks to Eric Smith and Sandip Ray for useful
discussions on this topic.  We have also slightly modified the hints
for the defthm event underneath a defun-sk in order to make the proof
more reliably efficient.

A new event, reset-prehistory, allows setting of a barrier before which
undoing is illegal.  An argument to this macro allows the barrier to be
made permanent; otherwise, it can be removed with :ubt-prehistory.
Thanks to Peter Dillinger for useful conversations leading to the
addition of reset-prehistory.

A new query, (wormhole-p state), allows users to determine whether or
not they are in a wormhole.  Thanks to Peter Dillinger for providing
this utility.

Value-triple no longer evaluates its form during include-book, and in
raw Lisp its calls trivially macroexpand to nil, without any
consideration of its argument.  This change avoids errors and warnings
when stobj names occur in the argument.

We fixed what could be considered a soundness hole that could occur by
exploiting redefinition in a particular way.  Thanks to Peter Dillinger
for raising a question that led to discovery of this hole.

A bug has been fixed in handling of illegal theory expressions.  Thanks
to Eric Smith, who reported this problem and provided the example
(in-theory '((:definition natp) (:rewrite doesntexist))) to show how a
hard error could occur.

Improved error reporting by certify-book when the certification world
contains inadmissible forms.

Modified defchoose to add two new keyword arguments.  There is now a
:doc keyword argument; previously, an optional documentation string
(see DOC-STRING) was to be placed just before the body, without
a keyword.  There is also a :strengthen argument that strengthens the
axiom added, which allows for the definition of "fixing" functions for
equivalence relations that choose canonical representatives of
equivalence classes.  See DEFCHOOSE.  Thanks for Dave Greve for
useful discussions that led us to this :strengthen enhancement.

Added books/misc/bash.lisp, which provides utilities for simplifying a
goal into a list of subgoals (as documented at the top of that file).
Thanks to Dave Greve for requesting this utility and suggesting
refinements to its functionality, which have been incorporated.

(For Emacs users only) The command meta-x new-shell provided by file
emacs/emacs-acl2.el now puts you in shell-mode, which for example
supports directory tracking.  Thanks to Jared Davis for suggesting this
change.

Fixed some mishandling of stobjs by make-event expansion.

Introduced a new event, defttag, that introduces a "trust tag" ("ttag")
allowing for extensions of ACL2 and for the use of generally unsafe
ACL2 constructs.  Thanks to Peter Dillinger, Sandip Ray, and Erik
Reeber for useful discussions on defttag and the following related
items.

     A new event, remove-untouchable, can be used to give users access
     to system functions and data structures.  We also fixed a bug in
     push-untouchable; and, it no longer is a no-op in :program mode.
     Thanks to Peter Dillinger for proposing remove-untouchable and
     suggesting that it and push-untouchable be functional in :program
     mode.

     Raw-mode (see SET-RAW-MODE) no longer disables
     certify-book.  However, set-raw-mode is now disallowed unless
     there is an active ttag (see DEFTTAG).  If you want to
     execute (set-raw-mode t) and there is no active ttag, consider
     executing (set-raw-mode-on!)  instead.

     Redefinition of system functions is disallowed unless there is an
     active ttag.  However, redef! now introduces (defttag :redef!) in
     order to allow redefinition of system functions.

     A new event, progn!, is a legal embedded event form that can go in
     books and both encapsulate and progn forms (see
     EMBEDDED-EVENT-FORM), and is similar to progn except that it
     allows arbitrary forms.  Thus, a progn! form is potentially
     dangerous and can only be evaluated if there is an active ttag.

     See TTAGS-SEEN for information about how to find the ttags
     known in the current ACL2 world, and for related caveats.

     A new book created with Peter Dillinger, books/misc/hacker.lisp,
     uses progn! to define utiliities with-raw-mode and
     with-redef-allowed, which respectively allow raw Lisp evaluation
     and redefinition to take place within a certifiable book (!).

Macro with-output is no longer allowed in function bodies because it
does not have (and has never had) any effect in raw Lisp.  See
WITH-OUTPUT for a workaround.

Fixed a bug in redundancy of defstobj in raw Lisp, which caused an
error when certifying a book with a redundant defstobj event whose
stobj had already been modified.  Here is an example:

     (defstobj st fld)
     (update-fld 3 st)
     (certify-book "foo" 1) ; where foo.lisp contains (defstobj st fld)

New books illustrating make-event have been contributed in directory
books/make-event/: dotimes.lisp (David Rager), stobj-test.lisp, and
logical-tangent.lisp (Peter Dillinger).

Modified print-object$ (see IO) so that it no longer prints an
extra space at the end.

Replaced the "draconian restriction to avoid capture" that had prevented
some :functional-instance hints from being legal.  The corresponding
check now only requires that no variable free in the functional
substitution is captured by a let or mv-let (or lambda) binding.  See
LEMMA-INSTANCE.

Added new extended metafunction, mfc-rw+, which is equivalent to mfc-rw
except that it takes an alist argument, which may be useful for
efficiency.  See EXTENDED-METAFUNCTIONS.  Thanks to Robert Krug
for suggesting this more efficient variant of mfc-rw.

Added support for the ignorable declare form.

We now cause an error on a call of open-input-channel (see IO)
with an argument string whose first character is the | character.
Thanks to Bob Boyer for providing an example (several months ago)
showing the danger of such calls, namely that the following command
would log you out and kill all of your processes when running on top of
GCL in Linux:
(open-input-channel "|kill -9 -1" :object state)

Restricted the use of make-event to contexts in which it can be tracked
properly, under legal events (see EMBEDDED-EVENT-FORM).  Thanks
to Peter Dillinger for bringing an example to our attention that led to
this fix.

Fixed a bug that was avoiding guard-checking for the functions
compress1 and compress2.  Thanks to David Rager for bringing this bug
to our attention.

Added an error message when a defun or mutual-recursion event fails, to
clarify whether failure is for the measure conjecture or for the guard
conjecture.  Thanks to David Rager for requesting clarification for
such failures.

Fixed a bug in reporting of guard violations (hard Lisp error) when
certain macros (for example, cond) are used in the guard.  Thanks to
Jared Davis for bringing this problem to our attention and providing
assistance with the solution, in particular by providing a helpful
example.

Grant Passmore has contributed a resolution/paramodulation prover
written in ACL2, in directory books/deduction/passmore/.  Thanks, Grant.

Improved the error message when illegal theories are encountered.

Improved the suppression of output for inhibit-output arguments of
routines in the book books/misc/expander.lisp.  Thanks to Qiang Zhang
for pointing out the possibility for improvement here.

Added a new directory books/arithmetic-3/extra/ that extends
books/arithmetic-3 with additional rules, contributed by Alex
Spiridonov with guidance from Robert Krug.  WARNING: This directory is
under development.  It may undergo large changes in future releases, so
please consider it experimental and subject to change.  Feedback is
welcomed.

As part of the work mentioned just above, Robert Krug and Alex
Spiridonov contributed improvements to books/arithmetic-3/:

     o A new rule |(* (/ x) (/ (expt x n)))| in bind-free/collect.lisp,
     which is important for reducing collect-* expressions though it
     slowed down one proof (see comment above this rule in
     bind-free/collect.lisp).

     o Slight improvements of rules integerp-mod and rationalp-mod in
     floor-mod/floor-mod.lisp.

     o To avoid conflict with books/rtl/rel6/arithmetic/, renamed rule
     mod-minus to mod-neg in floor-mod/floor-mod.lisp, and renamed
     integerp-+-reduce-leading-constant to
     integerp-+-reduce-leading-rational-constant in
     bind-free/integerp.lisp.

(GCL on Windows only) Made a low-level change to avoid multiplying
stacks for GCL on Windows, since GCL 2.6.6 broke while doing this.

Fixed bugs in linear arithmetic (rarely evidenced, it seems) involving
using < to compare complex rational constants.  Thanks to Robert Krug
for helping with the fixes.

Added a new event, assert-event, for checking that forms evaluate to
non-nil values.  Thanks to Peter Dillinger for suggesting and
collaborating on this addition.

NOTE-3-1    ACL2 Version  3.1 (December, 2006) Notes

NOTE!  New users can ignore these release notes, because the
documentation has been updated to reflect all changes that are recorded
here.

Please see NOTE-3-0-2 for a description of changes since
Version  3.0.1, and also see NOTE-3-0-1 for additional changes
since Version  3.0.

NOTE-3-1(R)    ACL2 Version  3.1(r) (December, 2006) Notes

No significant changes have been made since Version  3.0 for support of
non-standard analysis in particular.

Please also see NOTE-3-1 for changes to Version  3.1 of ACL2.

NOTE-3-2    ACL2 Version  3.2 (April, 2007) Notes

NOTE!  New users can ignore these release notes, because the
documentation has been updated to reflect all changes that are recorded
here.

Before this release, a raw Lisp error could put the ACL2 user into the
debugger of the host Common Lisp.  Now, such cases will generally put
the user back at the top-level loop after an informative message.  For
details, see SET-DEBUGGER-ENABLE; also see BREAK$.

Fixed a soundness bug that was allowing unknown packages to sneak into
a book and wreak havoc.  Thanks to Peter Dillinger for sending an
interesting example that led us to an exploration resulting in finding
this bug.  (A comment in the source code for note-3-2 shows such an
example.)  That example led us to fix a couple of other bugs related to
packages.  See HIDDEN-DEATH-PACKAGE if you are generally
interested in such issues, and for associated examples, see comments in
note-3-2 in the ACL2 source code.

Fixed subtle soundness bugs related to :meta rules by restricting
evaluators (see DEFEVALUATOR), as discussed in a new
documentation topic: see EVALUATOR-RESTRICTIONS.

Fixed a soundness bug that was allowing redefinition from :logic to
:program mode.  This prohibition had been in ACL2 for awhile but was
accidentally removed in the preceding version.

Fixed a soundness bug related to trace$.  Thanks to Peter Dillinger for
bringing it to our attention and for useful discussions, and providing a
proof of nil, the essence of which is illustrated as follows:

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

Thus, trace$ could be used to cause destructive raw Lisp behavior.
Now, trace$ fails unless it is either given a list of symbols or else
there is an active trust tag (see DEFTTAG); otherwise, consider
using trace! instead.

Closed a loophole that could be viewed as compromising soundness.  It
was possible to write files during book certification by exploiting
make-event expansion, but that is no longer the case by default.  A new
function open-output-channel! is identical as a function to
open-output-channel, except that the new function may be called even
during make-event expansion and clause-processor hints, but requires
that there is an active trust tag (see DEFTTAG).  Thanks to
Peter Dillinger for producing a convincing example (forging a
certificate during book certification; see
OPEN-OUTPUT-CHANNEL!) and to him, Sandip Ray, and Jared Davis for
useful discussions on the topic.

Added book books/defexec/reflexive/reflexive.lisp to illustrate
reflexive functions.

ACL2 now generate scripts that invoke the saved image with exec.
(Previously this was only done for GCL and CLISP.)  The benefit of this
change can be to avoid the lingering of ACL2 processes after enclosing
processes have exited.  Thanks to Peter Dillinger for pointing out this
issue.

ACL2 has a better implementation of (good-bye) (hence of synonyms
(quit) and (exit)).  As a result, you should now be able to exit ACL2
and Lisp from within the ACL2 read-eval-print loop with any of the
above; formerly, this was not supported for some Lisp implementations,
and was slow in OpenMCL.  Thanks to SBCL developer Harald Hanche-Olsen
for useful advice.

Fixed a bug in raw-mode (see SET-RAW-MODE) that was causing
hard errors when evaluating calls of er-progn, or of macros expanding
to such calls.

Fixed a few Makefile dependencies, necessary only for parallel make.

A new book, misc/defpun-exec-domain-example.lisp, provides an example
showing how partial functions which return a unique value for arguments
in a specified domain can be efficiently executed with ACL2.  Execution
is achieved using the mbe construct.  Thanks to Sandip Ray for providing
this example.

Existing function mod-expt computes (mod (expt base exp) mod) with
great efficiency in GCL, but not in other Lisps.  Now, the book
arithmetic-3/floor-mod/mod-expt-fast.lisp defines a function
mod-expt-fast that should provide significantly improved performance for
such expressions in other Lisps as well, though still probably not as
fast as when using mod-expt in GCL.  Thanks to Warren Hunt, with
contributions from Robert Krug, for providing this book,

Modified macro break-on-error to print of an error message before
entering a break, and to cause a hard error if the underlying Lisp
cannot handle it (formerly, a raw Lisp break would occur).  Thanks to
Bob Boyer for bringing these issues to our attention.

The book books/misc/defpun.lisp, as well as other books related to the
defpun macro, has been modified to avoid namespace collisions by
prefixing function symbol names with "DEFPUN-"; for example base has
been replaced by defpun-base.  Thanks to Dave Greve for providing a
first version of this update to defpun.lisp.

A theory, base, in books/arithmetic-3/bind-free/top.lisp, has been
renamed arithmetic-3-bind-free-base, to avoid potential name conflicts.

Fixed books/arithmetic-3/bind-free/banner.lisp to print (as before) a
message about how to turn on non-linear arithmetic, by modifying the
call of value-triple to use :on-skip-proofs t.  Thanks to Robert Krug
for bringing this issue to our attention.

Modified books/Makefile-subdirs and books/Makefile-psubdirs so that
they can be used with books/Makefile-generic.  Thus, one can set things
up so that make can be used to certify books both in the current
directory and subdirectories, for example as follows.

       ACL2 = ../../saved_acl2

       arith-top: top all
       all: top

       DIRS = pass1 bind-free floor-mod
       include ../Makefile-subdirs
       include ../Makefile-generic

       top.cert: top.lisp
       top.cert: bind-free/top.cert
       top.cert: floor-mod/floor-mod.cert
       top.cert: floor-mod/mod-expt-fast.cert

An experimental extension of ACL2 is under development by Bob Boyer and
Warren Hunt to support function memoization, hash conses, and an
applicative version of hash tables.  The default build of ACL2 does not
include this extension, other than simple logic definitions of
functions in new source file hons.lisp.  Future versions of ACL2 may
fully incorporate this experimental extension.

The defevaluator event macro has been modified primarily by adding a
new constraint as follows, where evl is the evaluator.  The idea is that
for the evaluation of a function call, one may replace each argument by
the quotation of its evaluation and then also replace the alist
environment with nil.

     (DEFTHMD UNHIDE-evl-CONSTRAINT-0
       (IMPLIES (AND (CONSP X)
                     (SYNTAXP (NOT (EQUAL A ''NIL)))
                     (NOT (EQUAL (CAR X) 'QUOTE)))
                (EQUAL (evl X A)
                       (evl (CONS (CAR X)
                                  (KWOTE-LST (UNHIDE-evl-LIST (CDR X) A)))
                            NIL))))

In order to support this change, there is another change: an evaluator
maps nil to nil (note (AND X (CDR (ASSOC-EQ X A))) in place of (CDR
(ASSOC-EQ X A)) below).

     (DEFTHM UNHIDE-evl-CONSTRAINT-1
       (IMPLIES (SYMBOLP X)
                (EQUAL (UNHIDE-evl X A)
                       (AND X (CDR (ASSOC-EQ X A))))))

With the new defevaluator, Dave Greve has been able to do a proof about
beta reduction that seemed impossible before (see
books/misc/beta-reduce.lisp).  Thanks to Dave for suggesting an initial
version of this change.

Explicit compilation is now avoided for OpenMCL, resulting in fewer
files to manage (no more files resulting from compilation) and,
according to some tests, slightly faster run times.  See
COMPILATION.  Thanks to Bob Boyer and Warren Hunt for suggesting this
possibility.

Now, the term-evisc-tuple (see LD-EVISC-TUPLE) is overridden by
state global user-term-evisc-tuple in all cases.  Formerly, this was
only the case when term-evisc-tuple was called with non-nil first
argument.

Symbols with the dot (.) character are generally no longer printed with
vertical bars.  For example, before this change:

       ACL2 !>'ab.c
       |AB.C|
       ACL2 !>

After this change:

       ACL2 !>'ab.c
       AB.C
       ACL2 !>

Thanks to Jared Davis for suggesting this improvement.

Fixed bugs in guard verification for theorems.  The following examples
illustrate these bugs.  If either theorem's body is executed in raw Lisp
there is likely to be a hard Lisp error, even though verify-guards was
supposed to ensure against that behavior.

     ; Example: Verify-guards failed to check that all functions in the theorem
     ; had already been guard-verified.
     (defun my-car (x) (car x))
     (defthm my-car-compute-example (equal (my-car 3) (my-car 3)))
     (verify-guards my-car-compute-example)

     ; Example: Verify guards of a theorem whose body uses state improperly.
     (defthm bad-state-handler
       (if (state-p state)
           (equal (car state) (car state))
         t)
       :rule-classes nil)
     (verify-guards bad-state-handler)

See GCL for an example, developed with Warren Hunt and Serita
Nelesen, that shows how to get fast fixnum (small integer) arithmetic
operations in GCL.

Fixnum declarations are now realized as (signed-byte 30) and
(unsigned-byte 29) instead of what was generally (signed-byte 29) and
(unsigned-byte 28).  MCL users may thus find better performance if they
switch to OpenMCL.  Note that some definitions have changed
correspondingly; for example, zpf now declares its argument to be of
type (unsigned-byte 29) instead of (unsigned-byte 28).  A few books may
thus need to be adjusted; for example, changes were made to books in
books/data-structures/memories/.

ACL2's rewriter now avoids removing certain true hypotheses and false
conclusions.  When a hypothesis rewrites to true or a conclusion
rewrites to false, ACL2 formerly removed that hypothesis or conclusion.
Now, it only does such removal when the hypothesis or conclusion is
either a call of equal or an equivalence relation (see
EQUIVALENCE), or else is sufficiently trivial (roughly, either
redundant with another hypothesis or conclusion or else trivially true
without considering the rest of the goal).  A specific example may be
found in source file simplify.lisp; search for "; But we need to do
even more work".  Thanks to Robert Krug for providing the idea for this
improvement and its initial implementation.  As is common with
heuristic changes, you may find it necessary on occasion to rename some
subgoals in your hints.  And in this case, you might also find it
necessary on rare occasions to add :do-not '(generalize) hints.

A new function, mfc-relieve-hyp, allows (for example) for more powerful
bind-free hypotheses, by providing an interface to the rewriter's
routine for relieving hypotheses.  See EXTENDED-METAFUNCTIONS.
Thanks to Robert Krug for providing the idea for this feature and its
initial implementation.

Two improvements have been made to non-linear arithmetic (see
NON-LINEAR-ARITHMETIC).  One allows for deducing strict inequality
(<) for the result of certain polynomial multiplications, where
previously only non-strict inequality (<=) was deduced.  A second allows
the use of the product of two polynomials when at least one of them is
known to be rational.  We had previously restricted the use of the
product to the case where both were known to be rational.  Thanks to
Robert Krug for these improvements.

(OpenMCL and Allegro CL only) Fixed ACL2's redefinitions of raw Lisp
trace and untrace in OpenMCL and Allegro CL so that when given no
arguments, they return the list of traced functions.  For trace, this is
an ANSI spec requirement.  Note that trace$ and untrace$ continue to
return nil in the ACL2 loop.

Fixed a bug that was allowing the symbol &whole to appear in other than
the first argument position for a defmacro event, in violation of the
Common Lisp spec (and leading to potentially surprising behavior).
Thanks to Peter Dillinger for bringing this bug to our attention.

It had been illegal to use make-event under some calls of ld.  This has
been fixed.  Thanks to Jared Davis for bringing this issue to our
attention with a simple example, in essence:

     (ld '((defmacro my-defun (&rest args) `(make-event '(defun ,@args)))
           (my-defun f (x) x)))

ACL2 no longer prohibits certain make-event forms when including
uncertified books.  Thanks to Peter Dillinger for first bringing this
issue to our attention.

Hard errors arose when using break-rewrite stack display commands, in
particular :path and :frame, from inside the proof-checker.  This has
been fixed.

Fixed a bug that could cause functions that call system built-ins
f-put-global, f-get-global, or f-boundp-global to cause a raw Lisp
error even when proving theorems.  Thanks to Peter Dillinger, for
reporting such a failure for the form (thm (w '(1 2 3))).

Renamed the formal parameters of function set-equal in distributed book
books/arithmetic-3/bind-free/normalize.lisp so that more distributed
books can be included together in the same session.  In particular books
books/data-structures/set-theory and books/arithmetic-3/extra/top-ext
can now be included together.  Thanks to Carl Eastlund for bringing this
problem to our attention and to Robert Krug for suggesting the formals
renaming as a fix.

Metafunctions must now be executable.  See META.

New utilities allow for user-defined simplifiers at the goal level, both
verified and unverified ("trusted"), where the latter can even be
defined by programs outside ACL2.  See CLAUSE-PROCESSOR, which
points to a new directory books/clause-processors/ that contains
examples of these new utilities, including for example a system
("SULFA") contributed by Erik Reeber that implements a decision
procedure (thanks, Erik).  Also see PROOF-CHECKER-COMMANDS for
the new proof-checker command clause-processor (or for short, cl-proc).

The rewriter has been tweaked to run faster in some cases involving very
large terms.  Thanks to Eric Smith and Jared Davis for providing a
helpful example that helped us locate the source of this inefficiency.

Added books/make-event/defspec.lisp.  This book shows how one can mimic
certain limited forms of higher-order statements in ACL2 by use of
macros, make-event, and table events.

A new release of the RTL library, books/rtl/rel7/, replaces the previous
version, books/rtl/rel6/.  Thanks to Hanbing Liu and David Russinoff for
providing this new version.

We thank David Russinoff for providing a proof of the law of quadratic
reciprocity.  See books/quadratic-reciprocity/Readme.lsp.

Eliminated a slow array warning (see SLOW-ARRAY-WARNING) that
could occur when exiting a wormhole after executing an in-theory event
in that wormhole.  Thanks to Dave Greve for bringing this problem to
our attention.

A new accessor, (mfc-rdepth mfc), provides a new field, the remaining
rewrite stack depth, which has been added to metafunction context
structures; see EXTENDED-METAFUNCTIONS.  Thanks to Eric Smith
for suggesting this addition.

The algorithms were modified for collecting up rule names and other
information used in proofs, into so-called "tag trees".  Tag trees are
now free of duplicate objects, and this change can dramatically speed
up some proofs that involve many different rules.  Thanks to Eric Smith
for doing some profiling that brought this issue to our attention, and
for reporting that this change reduced proof time on an example by
about 47% (from 3681.46 reported seconds down to 1954.69).

All legal xargs keywords may now be used in verify-termination events.
In particular, this is the case for :normalize.

(SBCL and CMUCL only) Fixed a problem with stobj array resizing
functions that was causing a hard error in ACL2 images built on SBCL or
CMUCL.

A new table, evisc-table, allows you to introduce print abbreviations,
for example for large constants.  Moreover, a new reader macro --#, --
makes it convenient to reference constants even inside a quote.  See
EVISC-TABLE.  Thanks to Bob Boyer and Warren Hunt for useful
discussions leading to this feature.

The macros in books/misc/expander.lisp now have a new keyword argument,
:simplify-hyps-p.  The default behavior is as before, but now case
splitting from hypothesis simplification can be avoided.  For details,
evaluate (include-book "misc/expander" :dir :system) and then :doc!
defthm? and :doc! symsym.  Thanks to Daron Vroon for sending a question
that prompted this additional functionality.

ACL2 failed to apply :restrict hints to rules of class :definition,
except for the simplest sorts (see SIMPLE).  This has been
fixed.  Thanks to Jared Davis for pointing out this bug by sending a
small example.

Added a new :msg argument to assert-event; see ASSERT-EVENT.
The implementation of value-triple has been modified to support this
change.

Fixed a bug in macro io? that now allows the commentp argument to be t.
This provides a way other than cw to print without modifying state,
for example as follows.  (Warning: Certain errors may leave you in a
wormhole, in which case use #. to abort.)

     ACL2 !>(prog2$ (io? event t state
                         ()
                         (fms "Howdy~%" nil *standard-co* state nil))
                    (+ 3 4))

     Howdy
     7
     ACL2 !>:set-inhibit-output-lst (proof-tree event)
      (PROOF-TREE EVENT)
     ACL2 !>(prog2$ (io? event t state
                         ()
                         (fms "Howdy~%" nil *standard-co* state nil))
                    (+ 3 4))
     7
     ACL2 !>

ACL2 now disallows calls of progn! inside function bodies, just as it
already disallowed such calls of progn, since in both cases the Common
Lisp meaning differs from the ACL2 meaning.

Redefinition of system functions now always requires an active trust tag
(see DEFTTAG).  This restriction was intended before, but there
was a hole that allowed a second redefinition without an active trust
tag.  Thanks to Peter Dillinger for pointing out this bug.

Verify-termination has been disabled for a few more built-in functions
that are in :program mode.  (If you are curious about which ones they
are, evaluate (f-get-global 'built-in-program-mode-fns state).)
Moreover, such functions now will execute only their raw Lisp code, so
for example they cannot be called during macroexpansion.  Thanks to
Peter Dillinger and Sandip Ray for useful discussions on details of the
implementation of this restriction.

New untouchable state global variables, temp-touchable-vars and
temp-touchable-fns, can control the enforcement of untouchability.  See
REMOVE-UNTOUCHABLE.  Thanks to Peter Dillinger for suggesting
these features.

The "TTAG NOTE" string was being printed by encapsulate events whenever
an active trust tag was already in effect (see DEFTTAG), even if
the encapsulate event contained no defttag event.  This has been fixed.
Thanks to Peter Dillinger for a query leading to this fix.

Fixed a bug in progn! that could leave the user in raw-mode (see
SET-RAW-MODE).  This could occur when certifying a book with a
compile-flg value of t (see CERTIFY-BOOK), when that book
contained a progn! event setting raw-mode to t without setting raw-mode
back to nil:

     (progn! (set-raw-mode t) ...)

NOTE-3-2(R)    ACL2 Version  3.2(r) (April, 2007) Notes

Changed the default distributed books directory for ACL2(r) from books/
to books/nonstd/.  See INCLUDE-BOOK, in particular the
discussion of "Distributed Books Directory".

Added directory books/arithmetic-3/ and its subdirectories to
books/nonstd/.  (But a chunk of theorems from
arithmetic-3/extra/ext.lisp are "commented out" using
#-:non-standard-analysis because they depend on books/rtl/rel7/, which
is not yet in books/nonstd/; feel free to volunteer to remedy this!)

Incorporated changes from Ruben Gamboa to some (linear and non-linear)
arithmetic routines in the theorem prover, to comprehend the reals
rather than only the rationals.

Please also see NOTE-3-2 for changes to Version  3.2 of ACL2.

NOTE-3-2-1    ACL2 Version  3.2.1 (June, 2007) Notes

NOTE!  New users can ignore these release notes, because the
documentation has been updated to reflect all changes that are recorded
here.

(OpenMCL and multi-threaded SBCL only) Fixed a soundness bug in the
evaluation of mbe forms in the presence of Lisp feature
:acl2-mv-as-values.  Thanks to Sol Swords for reporting this problem and
sending a simple proof of nil (which can be found in a comment in the
ACL2 sources, in (deflabel note-3-2-1 ...)).

Added a new utility, dmr (Dynamicaly Monitor Rewrites), for watching
the activity of the rewriter and some other proof processes.  See
DMR.  We thank Robert Krug for useful contributions.

Fixed a bug in evaluation of calls of with-prover-time-limit.

Fixed the writing of executable scripts when building ACL2, so that the
build-time value of environment variable ACL2_SYSTEM_BOOKS is no longer
written there.  Thanks to Dave Greve for discussing this change.

Fixed bugs in :pl (which are similarly present in the proof-checker's
sr (show-rewrites) command.  The first bug was evident from the
following forms sent by Robert Krug, which caused an error.

     (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system)
     :pl (mod (+ 1 x) n)

The second bug was due to a failure to take note of which rules are
disabled, and could be seen by executing the following (very slow!).

     (defstub modulus () t)
     (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system)
     :pl (mod (+ x y) (modulus))

Modified certify-book so that by default, all executable-counterpart
functions (sometimes called "*1* functions") are compiled.  This is the
behavior that was already supported with a compile-flg argument of
:all; the change is that argument t now has this behavior as well (and
:all is supported only for legacy purposes).  A new value for
compile-flg, :raw, gives the behavior formerly produced by value t,
namely where executable-counterpart functions are not compiled.  The
above changes are irrelevant if compilation is suppressed; see
COMPILATION.  Finally, if environment variable ACL2_COMPILE_FLG is
set, then after converting to upper-case this environment variable's
value of "T", "NIL", or ":RAW" will determine the value of the optional
compile-flg argument to be t, nil, or :raw, respectively, when this
argument is not explicitly supplied.

Modified include-book so that :comp argument now acts like :comp!,
i.e., compiling a file that includes the file together with all
executable counterpart (so-called "*1*") functions.  A new argument,
:comp-raw, has the behavior that :comp had formerly, i.e., compiling
the actual book only.

The function nonnegative-integer-quotient is now computed in raw Lisp
by calling floor on its arguments.  This change was suggested by Peter
Dillinger, in order to avoid stack overflows such as reported by Daron
Vroon.  A new book, books/misc/misc2/misc.lisp, contains a proof of
equivalence of nonnegative-integer-quotient and floor, and serves as a
repository for other miscellaeous proofs, including those justifying
ACL2 modifications such as this one.

Enhanced accumulated-persistence to break down results by useful vs.
useless rule applications.  In particular, this provides information
about which rules were ever applied successfully, as requested by Bill
Young.

Added coverage of :meta rules to the accumulated-persistence statistics.

Fixed a bug that was causing a :clause-processor hint to fire on a
subgoal of the goal to which it was attached, when the original
application didn't change the clause.  Thanks to Dave Greve for
pointing out this bug and providing a useful example.

Fixed a bug in handling of computed hints related to the
stable-under-simplificationp parameter (see COMPUTED-HINTS).
There were actually two bugs.  A minor but confusing bug was that the
same goal was printed twice upon application of such a hint.  The major
bug was that :use hints (as well as other "top" hints: :by, :cases, and
:clause-processor) were not being applied properly.  Thanks to Jared
Davis for sending an example some time ago that showed the duplicate
printing, and to Dave Greve for sending an example showing
mis-application of :clause-processor hints.  Note that you may find
that existing computed hints using the stable-under-simplificationp
parameter no longer have the same behavior; see a comment about
computed hints in note-3-2-1, ACL2 source file ld.lisp, for an example
of how you might want to fix such computed hints.

David Russinoff has contributed an updated version of
books/quadratic-reciprocity/ including minor modifications of the
treatment of prime numbers and a proof that there exist infinitely many
primes.  Thanks to David for contributing this work, and to Jose Luis
Ruiz-Reina for posing the challenge.

Reduced the sizes of some certificate (.cert) files by relaxing the
test that allows original defpkg events to be placed there, rather than
evaluating the import list term into an explicit list of symbols.

Improved execution efficiency slightly for function rcdp in file
books/misc/records.lisp, by using mbe to introduce a tail-recursive
body.

The executable script generated by save-exec (and by the normal build
process) now includes a time stamp as a comment.  Thanks to Jared Davis
for suggesting this change in order to support his use of omake.  In the
process, we also arranged that the startup banner for an executable
created by save-exec shows all of the build (save) times, not just the
one for the original image.

Sped up most redundant defpkg events by avoiding evaluation and sorting
of the imports list in the case of identical event forms.  And, for
defpkg events that are not redundant, sped up their processing in
Allegro CL (and perhaps other Lisps, but apparently not GCL) by using
our own import function.

Modified add-include-book-dir so that it refuses to associate a keyword
with a different directory string than one it is already bound to.  See
DELETE-INCLUDE-BOOK-DIR for how to remove the existing binding
first.  Thanks to Robert Krug for pointing out that without this
change, one can find it difficult to debug a failure due to rebinding a
keyword with add-include-book-dir.

Added a new value for the :do-not-induct hint (see HINTS),
:otf-flg-override, which causes ACL2 to ignore the :otf-flg when
considering whether to abort the proof because of a :do-not-induct
hint.  Thanks to Daron Vroon for suggesting such an addition.

Modified the printing of messages for entering and exiting raw mode
(see SET-RAW-MODE), so that in particular they are inhibited
during include-book or whenever observations are inhibited (see
SET-INHIBIT-OUTPUT-LST).  Thanks to Peter Dillinger for suggesting
such a change.

(For system hackers only.)  The handling of events of the form (progn!
(state-global-let* ...)) had a bug that was causing bindings to be
evaluated twice.  Moreover, the use of system function
state-global-let* is suspect in raw Lisp.  We have eliminated special
treatment of state-global-let* by progn! in favor of a new keyword
argument, state-global-bindings, that provides the intended
functionality.  See PROGN!.  Moreover, special handling that
allowed make-event forms under state-global-let* has been removed; the
desired effect can be obtained using (progn! :state-global-bindings
...).  Thanks to Peter Dillinger for pointing out the above bug and
collaborating on these changes.

Incorporated backward-compatible enhancements to
books/misc/expander.lisp from Daron Vroon (documented near the top of
that file).

The specification of :backchain-limit-lst had required that only a
single (:rewrite, :linear, or :meta) rule be generated.  We have
weakened this restriction to allow more than one rule provided that
each rule has the same list of hypotheses.  For example, the rule class
(:rewrite :backchain-limit-lst 1) is now legal for the corollary
formula (implies (f x) (and (g x) (h x))), where this was not formerly
the case.  Thanks to Dave Greve for bringing this issue to our
attention.

NOTE-3-2-1(R)    ACL2 Version  3.2.1(r) (June, 2007) Notes

Please also see NOTE-3-2-1 for changes to Version  3.2.1 of
ACL2.