This is documentation for ACL2 Version 4.3
Copyright (C) 2011  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-2-7-SYSTEM    ACL2 Version  2.7 Notes on System-level Changes

ACL2 now runs (once again) under LispWorks, specifically, LispWorks
4.2.0.  However, we needed a patch, which presumably will be
unnecessary after 4.2.7.  From LispWorks support:

     Users with LispWorks4.2.7 should ask us at lisp-support@xanalys.com
     for the transform-if-node patch. It will be helpful if they quote
     (Lisp Support Call #11372) when doing so. Also, they must send a
     bug form generated from their LispWorks image: instructions at
     http://www.lispworks.com/support/bug-report.html.

File books/Makefile-generic has been improved so that failed attempts to
certify a book will cause the make to fail.  Previously, an existing
.cert file was left in place, and that sufficed for the make to be
considered a success.  Now, the old .cert file is first removed when
recertification is found to be necessary.

A change has been made to source file acl2.lisp to accommodate GCL
2.4.3.  (ACL2 Version  2.6 does not work with some versions of GCL
2.4.3.)

The error message has been improved when certain forms are typed to raw
Lisp and the ACL2 loop has never been entered (with (LP)).

The following symbols in the ACL2 package have been made untouchable,
meaning that they are not available to the user: ev-fncall, ev, ev-lst,
ev-acl2-unwind-protect, ev-fncall!, and user-stobj-alist-safe.  The
reason is that these functions can not be called safely except under
certain restrictions.  If you want to call the ACL2 evaluator, consider
using the built-in system functions trans-eval or
simple-translate-and-eval.

CLISP Version_2.30 implements a notion of "locking" the "LISP" package
that is incompatible with building ACL2.  (CLISP Version_2.27 does not
appear to have had this feature.)  We have gotten around this problem
by unlocking the "LISP" package in ACL2 images built on such CLISPs.

Automatic proclaiming for GCL, which has (for a long time) been done for
functions in compiled books, has been improved.  Formerly, the only
time a non-trivial output type (i.e., other than t) was inferred was
when macroexpansion produced an explicit call of the.  Now, if
expressions can also generate non-t output types.  Consider the
following example.

     (defmacro the-fixnum (n)
       (list 'the '(signed-byte 29) n))
     (defmacro 1+f (x)
       (list 'the-fixnum
             (list '1+ (list 'the-fixnum x))))
     (defun foo (x)
       (declare (type (unsigned-byte 27) x))
       (if (zp x)
           0
         (1+f (foo (1-f x)))))

Formerly, the proclaim forms for foo, before and after this
improvement, are as shown below.

     (PROCLAIM '(FTYPE (FUNCTION ((UNSIGNED-BYTE 27)) T) FOO))                ;old
     (PROCLAIM '(FTYPE (FUNCTION ((UNSIGNED-BYTE 27)) (SIGNED-BYTE 29)) FOO)) ;new

Compiler info messages sent to error stream were eliminated for CMUCL.

NOTE-2-7(R)    ACL2 Version  2.7(r) (November, 2002) Notes

In source file axioms.lisp, in order for proofs to succeed, (make
proofs), the definitions of acl2-count and explode-atom have been
modified slightly, and lemma standard-numberp-one [modified after
Version_3.4 to become standardp-one] has been given :rule-classes nil.

All skip-proofs forms have been eliminated from the nonstd books, thanks
to Ruben Gamboa.

The directory books/sqrt/, which was intended for ACL2(r), has been
moved to books/nonstd/sqrt/ and added as appropriate to
books/nonstd/Makefile.

Please see NOTE-2-7 for changes to Version_2.7 of ACL2.

NOTE-2-8    ACL2 Version  2.8 (March, 2004) Notes

BRIEF SUMMARY.

The Version_2.8 notes are divided into the indicated subtopics.  Here
we give only a brief summary of just a few of the major new features
and changes that seem most likely to impact existing proofs.  Not
included in this brief summary, but included in the subtopics, are
descriptions of many improvements (including bug fixes and new
functionality) that should not get in the way of existing proof
efforts.  In the description below we also omit discussion of changes
that will become clear by way of error messages if they affect you.

In particular, please see NOTE-2-8-NEW-FUNCTIONALITY for
discussion of a number of new features that you may find useful.

Acknowledgements and elaboration, as well as other changes, can be
found in the subtopics listed below.

o Some of the bug fixes (see NOTE-2-8-BUG-FIXES):

     + Some soundness bugs were fixed.

     + The handling of free variables in hypotheses (see
     FREE-VARIABLES) of rewrite and linear rules had a bug that
     prevented some proofs from going through.  Now that this bug has
     been fixed, you may find some proofs running much more slowly than
     before.  You can use accumulated-persistence and
     add-match-free-override to remedy this situation; see
     NOTE-2-8-BUG-FIXES for details.

     + The default-hints in the current logical world are no longer
     ignored by verify-guards.

     + Forms violating guard-checking such as (defconst *silly* (car
     3)) are now allowed in books.

o Some of the new functionality (see
NOTE-2-8-NEW-FUNCTIONALITY):

     + WARNING: You may find that control-d (in emacs, control-c
     control-d) can throw you completely out of Lisp where it had not
     formerly done so.

     + ACL2 now starts up inside the ACL2 loop -- that is, (LP) is
     executed automatically -- when built on CLISP or Allegro CL.  This
     was already the case for GCL and CMUCL, and it still is not true
     for LispWorks.

     + See NOTE-2-8-ORDINALS for a discussion of a significant
     change in ordinal represtation, and in particular, for how to
     preserve existing proofs that depend on the previous ordinal
     representation.

     + Macros mbe ("must be equal"), mbt ("must be true"), and defexec
     have been introduced, which allow the user to attach alternate
     executable definitions to functions.

     + The user can now control multiple matching for free variables in
     hypotheses for :forward-chaining rules, as has already been
     supported for :rewrite and :linear rules.

     + It is no longer necessary to specify (set-match-free-error nil)
     in order to avoid errors when a rule with free variables in its
     hypotheses is missing the :match-free field.

     + The form (break-on-error) causes, at least for most Lisps, entry
     into the Lisp debugger whenever ACL2 causes an error.

     + A new table has been provided so that advanced users can
     override the built-in untranslate functionality.  See
     USER-DEFINED-FUNCTIONS-TABLE.

     + The pstack (`process [prover] stack") mechanism, formerly denoted
     checkpoints, has been improved.  One of these improvements is to
     show actual parameters with (pstack t) rather than formals.

     + The defstobj event is now allowed to take an :inline argument,
     which can speed up execution.

     + Macro cw-gstack no longer takes arguments for the gstack or
     state.  To print terms in full rather than abbreviated: (cw-gstack
     :evisc-tuple nil).

     + The include-book event now has an additional (optional) keyword,
     :dir.  In particular, (include-book "foo/bar" :dir :system) will
     include the indicated book after prepending the path of the
     built-in books/ directory.  You will probably not find :dir
     :system to be useful if you move the executable image or
     distributed books; see INCLUDE-BOOK, in particular its
     "soundness warning".

     + The printing of results in raw mode (see SET-RAW-MODE)
     may now be partially controlled by the user:  see
     ADD-RAW-ARITY.

     + For those using Unix/Linux make:  A cert.acl2 file can contain
     forms to be evaluated before an appropriate certify-book command is
     invoked automatically (not included in cert.acl2).

o Some of the changes in the proof engine (see NOTE-2-8-PROOFS):

     + ACL2 now prevents certain rewriting loops; see
     REWRITE-STACK-LIMIT.

     + Small changes have been made to heuristics for controlling
     rewriting during proofs by induction and in handling certain
     "weak" compound-recognizer rules.

     + The handling of free variables in a hypothesis of a rewrite rule
     (see FREE-VARIABLES) has been improved in the case that
     the hypothesis is of the form (equiv x y), where equiv is a known
     equivalence relation (see EQUIVALENCE).

     + We have modified how the ACL2 simplifier handles the application
     of a defined function symbol to constant arguments, by avoiding
     the introduction of hide when evaluation fails if the term can be
     rewritten.

     + The generation of "Goal" for recursive (and mutually-recursive)
     definitions now uses the subsumption/replacement limitation
     (default 500).  See CASE-SPLIT-LIMITATIONS.

     + Default hints now apply to hints given in definitions, not just
     theorems.  See DEFAULT-HINTS.

     + Linear arithmetic now uses the conclusions of forward-chaining
     rules, and type-set now uses a small amount of linear reasoning
     when deciding inequalities.

o Some of the changes in rules, definitions, and constants (see
NOTE-2-8-RULES):

     + See the above doc topic.

o Guard-related changes are described in see NOTE-2-8-BUG-FIXES.

o Some of the proof-checker changes (see
NOTE-2-8-PROOF-CHECKER):

     + Added new proof-checker commands wrap1, wrap, and wrap-induct,
     to combine multiple conjuncts or goals.

     + The type-alist command now takes optional arguments that control
     whether or not the governors and/or conclusion are used in
     computing the context.

o Some of the system-level changes (see NOTE-2-8-SYSTEM):

     + ACL2 now runs on OpenMCL and on MCL 5.0.

o Some of the other changes (see NOTE-2-8-OTHER):

     + Emacs file emacs/emacs-acl2.el has been updated (see
     NOTE-2-8-OTHER for details).

     + When :pl is given a term other than a symbol, it will print all
     rewrite rules that match that term.

     + A new function, pkg-witness, returns a symbol in the given
     package.

     + The list constant *acl2-exports* has been extended.

     + A new release of the rtl library has been included:
     books/rtl/rel4/.  See the README file in that directory.

Again, please proceed to the subtopics for more thorough release notes.

NOTE-2-8-BUG-FIXES    ACL2 Version  2.8 Notes on Bug Fixes

We have fixed a soundness bug in the tautology checker's handling of
expressions of the form (not (not x)).  This bug has gone back at least
as far as Version_2.4.  All of the regression tests passed after the
fix, without modification.  So we hope that this bug has rarely bitten
anyone.  Thanks to Qiang Zhang for sending us a proof of nil that led
us to this fix: (thm (equal (and p q) (not (or (not p) (not q))))).
And thanks to Matyas Sustik for an observation that led to an
improvement of our initial fix.

The preceding version (2.7) introduced a soundness bug in handling of
ACL2 arrays, in which functions compress1 and compress2 were returning
the input alist rather than compressing it appropriately.  Here is a
proof of nil that no longer succeeds, based on a bug report from Warren
Hunt, who we thank for bringing this problem to our atttention.

     (defthm bad
       (not (let* ((ar2 (aset1 'my-array ar1 3 10))
                   (ar3 (compress1 'my-array ar2))
                   (ar4 (reverse (reverse ar2)))
                   (ar5 (compress1 'my-array ar4)))
              (and (equal ar2 ar4)
                   (not (equal ar3 ar5)))))
       :rule-classes nil)
     (defthm contradiction
       nil
       :rule-classes nil
       :hints (("Goal" :use
                ((:instance bad
                            (ar1 (compress1 'my-array
                                            '((3 . 5)
                                              (:HEADER :DIMENSIONS (5)
                                                       :MAXIMUM-LENGTH 6
                                                       :DEFAULT 0
                                                       :NAME MY-ARRAY)))))))))

On a related note, a new function flush-compress can be used for subtle
control of under-the-hood raw Lisp support for fast array access,
although we expect it to be very rare that users need this extra
support.

Previous versions have had two soundness bugs that can occur when using
the proof-checker:

     o The first bug pertains to the expand command, and hence x and
     x-dumb commands (which call expand); see
     PROOF-CHECKER-COMMANDS.  The bug can occur when applying the
     above commands when the current term is a call of a constrained
     function symbol for which there is a :definition rule.  Now, the
     expand command will succeed only when the function symbol of the
     current term is a defined function symbol, in which case the
     original definition is always used, in analogy to how the :expand
     hint works in the prover; see HINTS.  Thanks to John
     Erickson for sending an example that led us to wonder if there
     might be a soundness problem.

     o The second bug pertains to the s command (and commands that call
     it, e.g., s-prop).  The proof-checker forms a context out of the
     top-level hypotheses and the if-terms governing the current term.
     If there is a contradiction in the top-level hypotheses, the
     proof-checker can appropriately consider the goal to be proved,
     and it does so.  But formerly, the criterion was weaker:  the
     contradiction could involve the combination of the top-level
     hypotheses and if-term governors.  Thanks to Rob Sumners for
     noticing this bug.

A soundness bug could be provoked in some Lisps by applying defpkg to
the empty string.  This has been disallowed.

We fixed a soundness bug related to packages caused by a failure to
track axioms introduced locally on behalf of defpkg events.  See
HIDDEN-DEATH-PACKAGE.

We fixed a soundness bug caused by a failure to check that a
:type-prescription rule can be processed when proofs are skipped or
under a defequiv event.  The former case can occur when processing an
encapsulate or include-book event, where the rule could depend on a
local :compound-recognizer rule preceding the proposed
:type-prescription rule under the same encapsulate or include-book
event.  See LOCAL-INCOMPATIBILITY for such an example.

We fixed a potential soundness bug relating to reclassifying a :program
mode function to :logic mode (as done by verify-termination or the
submission of an appropriate "redundant" definition) without adequate
checking that stobj usage was identical.  Allegedly redundant
definitions must now preserve the stobjs declaration as well as the
formals, body, guard and type declarations.  We thank Vernon Austel for
pointing out this problem.

It was possible to get a raw Lisp error by introducing a locally defined
function with guard verification inhibited and then subsequently
introducing the same definition non-locally without that inhibition.
The following example will clarify.

     (encapsulate nil
       (local
         (defun foo (x) (declare (xargs :guard t :verify-guards nil)) (car x)))
       (defun foo (x) (declare (xargs :guard t)) (car x)))
     ; The following causes a raw lisp error because ACL2 runs the Common Lisp
     ; definition of foo, because it thinks that foo's guard of t was verified.
     (thm (equal (foo 3) xxx))

Thanks to Jared Davis for bringing this problem to our attention.  We
are particularly grateful to Jared because his example exploited this
bug by applying it to a function defined using mbe (introduced in this
same version, 2.8), in order to prove nil!

The sort of error message shown below can legitimately occur when
certifying a book in a certification world where there was an
include-book command with a relative pathname (see PATHNAME).
However, it was occurring more often than necessary.  This has been
fixed.

     ACL2 Error in (CERTIFY-BOOK "foo" ...): The certification world has
     include-book commands for book "bar" that correspond to different
     full pathnames, namely "/u/dir1/bar" and "/u/dir2/bar".  ACL2
     cannot currently certify a book in such a world.  To work around
     this problem, use an absolute pathname for at least one of these
     books (see :DOC pathname).

Bugs were fixed in with-output, in particular related to the use of
values :all.  Also, documentation for with-output has been improved.
Thanks to Vernon Austel for pointing out the bugs.

Fixed a lisp error occurring when bash proof-checker command was given
illegal syntax, e.g., (bash (("Goal" :in-theory (enable
binary-append)))) instead of (bash ("Goal" :in-theory (enable
binary-append))).

We added an appropriate guard to find-rules-of-rune, which will avoid
hard lisp errors when this function is called on non-rune arguments.
Thanks to Eric Smith for pointing out this issue.

It was possible for a redundant include-book form (see
REDUNDANT-EVENTS) to leave a command in the ACL2 logical world and to
cause (re-)loading of a compiled file.  These behaviors have been
fixed.  In particular, if book1 has already been included in the
current ACL2 world and (include-book "book1") occurs in book2, then the
compiled file for book1 will not be loaded again when book2 is
included.  Thanks to Dave Greve for bringing our attention to these
problems, and to Eric Smith for bringing up a special case earlier
(where "//" occurred in the book name).

The summary printed at the end of a proof had not listed :induction
rules used in a proof.  This has been corrected.

The use of proof trees in emacs redefined `control-c control-c' in such
a way that in telnet mode, the telnet session was interrupted and
perhaps could not be continued.  This has been fixed.

Source function load-theory-into-enabled-structure contained a
guard-violating call of compress1.  Thanks to Vernon Austel for
bringing this problem to our attention; even though this bug was benign
(as he pointed out), we like keeping the source code free of guard
violations.

A number of proof-checker atomic macros caused a hard error when all
goals have already been proved.  This has been fixed.  Thanks to John
Erickson for sending an example of the issue.

A bug has been fixed in add-match-free-override.  Formerly, a table
guard violation occurred when calling add-match-free-override more than
once with first argument other than :clear.

Defininitions of functions involving large constants could cause stack
overflows.  This has been fixed, at least in some of the most egregious
cases (by making a source function fn-count-evg tail-recursive).  Thanks
to Jared Davis for bringing this problem to our attention.

Evaluation of computed hints could cause stack overflows.  This has been
fixed.  Thanks to Eric Smith for bringing this problem to our attention.

Evaluation of :monitor on :definition runes is now fast even if the
specified function is part of a very large mutual-recursion nest.
Thanks to Eric Smith for sending an example showing that this wasn't
always the case.

Fixed a bug in books/bdd/cbf.lisp that was causing certification of
distributed bdd books to fail when the connected book directory (see
CBD) differs from the current working directory.  Thanks to
Scott Guthery for bringing this bug to our attention and supplying a
helpful log.

Duplicate rule names have been eliminated from warnings generated upon
the use of enabled :rewrite or :definition rules.  Thanks to Eric Smith
for pointing out this problem.

The trace utilities (see TRACE), as modified for GCL and
Allegro Common Lisp, had failed to show more than the first return
value for so-called "*1*" functions (essentially,
executable-counterpart functions) when they were returning multiple
values (via mv).  This has been fixed.  Thanks to Erik Reeber for
pointing out this problem.  Also, it is now possible to refer to
arglist in trace$ forms when ACL2 is built on GCL, not just when ACL2
is built on Allegro Common Lisp.

Uses of hide introduced during proofs by failed attempts to evaluate
constrained functions (see HIDE) are now tracked, so that the
rune (:DEFINITION HIDE) will show up in the summary.

The following bug, introduced back in Version  2.7, has been fixed.
The bug applied only to GCL and may well not have affected anyone.  But
the function proclamation computed by ACL2 for compilation usually had
an output type of nil where it should have been t.

The macro gc$ had a bug exhibited when it was supplied one or more
arguments.  This has been fixed.

The macro defabbrev broke when supplied a string and no documentation,
e.g., (defabbrev foo () "").  Thanks to Rob Sumners for noticing this
problem and providing a fix, which we have incorporated.

For ACL2 executables built on Allegro Common Lisp, a Lisp error
occurred when trace$ was called on other than a defined function
symbol.  Now ACL2 prints a more useful error message.

The proof-checker no longer accepts a (verify) command when some
function symbol in the original goal no longer exists in the current
ACL2 logical world.  Thanks to John Erickson for bringing this issue to
our attention.

The function ld-redefinition-action may now be called by the user.
Thanks to Vernon Austel for suggesting that we remove this symbol from
the list of so-called untouchables.

The handling of free variables in hypotheses (see
FREE-VARIABLES) of rewrite and linear rules had a bug that prevented
some proofs from going through.  Here is a simple example, essentially
provided by Diana Moisuc, who we thank for bringing this issue to our
attention.  The proof of the thm below had failed, but now will
succeed.  This particular bug prevented, for example, the :all behavior
from occurring when the first hypothesis of the rule does not have free
variables.  NOTE:  Now that this bug has been fixed, you may find some
proofs running much more slowly than before.  You can use
accumulated-persistence to locate rules that are slowing down your
proofs because of excessive attention to free variables, and then
execute add-match-free-override for those rules (or, just change the
rules themselves to specify :once in the :rule-classes).

     (defstub foo1 (* ) => *)
     (skip-proofs
      (defthm aux-foo1
        (implies (and (integerp a)
                      (integerp i)
                      (equal (foo1 0)  (list 0 i)))
                 (equal (foo1 a) (list 0 (+ a i))))
        :rule-classes ((:rewrite :match-free :all))))
     (thm
      (implies (and (integerp i)
                    (integerp a)
                    (equal (foo1 0) (list 0 i)))
               (equal (foo1 a) (list 0 (+ a i)))))

Formerly, creation of large arrays could cause an error in the
underlying Common Lisp implementation without helpful messages for the
user.  Now, we check Common Lisp restrictions on arrays and print a
helpful error message if they are violated, namely: each dimension must
be less than the value of Common Lisp constant array-dimension-limit,
and the product of the dimensions must be less than the value of Common
Lisp constant array-total-size-limit.  Thanks to Warren Hunt for
bringing this issue to our attention.  Note:  this change also removes
a former restriction of stobj array fields to size smaller than 2^28-1,
provided the underlying Lisp can support larger arrays.

The default-hints in the current logical world were ignored by
verify-guards.  This has been fixed.  Thanks to Jared Davis for
pointing out this bug and sending a helpful example.

The brr mechanism has been cleaned up in order to avoid hard errors and
infinite loops that can arrive when typing interrupts (control-c) or
end-of-files (control-d) inside the brr loop.  Thanks to Dave Greve,
Olga Matlin, Eric Smith, and Serita Van Groningen for bringing this
issue to our attention.  As a byproduct, if you type control-d (or if
inside emacs, control-c control-d), you may now quit entirely out of
ACL2 and lisp (see GOOD-BYE) in some cases where you formerly
would not have, for example when sitting at the ACL2 prompt (which
formerly, in Allegro Common Lisp for example, would merely take you
into raw Lisp rather than quitting everything).

We have eliminated structural flaws in the HTML documentation pages that
could make them unreadable in some browsers.  Thanks to Bill Young for
bringing this issue to our attention and to Joe Hendrix for diagnosing
the problem.

The proof-checker could run very slowly after many instructions in a
given session.  This has been fixed; thanks to Art Flatau for bringing
this problem to our attention.  (Implementation detail: We now keep
tag-trees duplicate-free when we accumulate them into state.  This
change could have minor speed advantages for some top-level proofs too,
not just in the proof-checker.)

The printing of accesses to stobjs using nth or update-nth has been done
using symbolic constants since ACL2 Version_2.6.  However, there was a
bug that prevented this feature from working for update-nth except at a
top-level call.  This has been fixed.  Thanks to Julien Schmaltz for
bringing this problem to our attention.  For example, consider these
events:

     (defstobj st field0 field1)
     (thm (equal (nth 1 (update-nth 0 17 st)) (car (cons xxx yyy)))
          :hints (("Goal" :in-theory (disable nth update-nth))))

Before the fix, the proof attempt of the above silly thm printed the
following.

     (NTH 1 (UPDATE-NTH *FIELD0* 17 ST))

After the fix, we instead see the following.

     (NTH *FIELD1* (UPDATE-NTH *FIELD0* 17 ST))

It is now possible to certify and subsequently include books that
require guard-checking to be off.  For example, the book can contain
the form (defconst *silly* (car 3)) even though 3 fails to satisfy the
guard of car.  Formerly, it was necessary to execute
:set-guard-checking nil before a certify-book or include-book in order
for such a form to be handled without error.  Thanks to Hanbing Liu for
bringing this problem to our attention.

Fixed a proof-checker bug that could cause probably cause strange error,
"Attempt to access the plist field".  Thanks to Bill Young for bringing
this problem to our attention.

Fixed a proof-checker bug that was failing to record applications of
rewrite rules using the proof-checker's :rewrite command, causing the
proof summary to omit mention of that rule (for example, when using the
proof-checker's :exit command to generate an :instructions hint).
Thanks to Bill Young for pointing out this bug.

Modernized some of the proof-tree emacs and infix printing stuff,
thanks to suggestions made by Camm Maguire.

NOTE-2-8-GUARDS    ACL2 Version  2.8 Notes on Guard-related Changes

All the guard-related changes may be found elsewhere; in particular,
see NOTE-2-8-BUG-FIXES.

NOTE-2-8-NEW-FUNCTIONALITY    ACL2 Version  2.8 Notes on New Functionality

WARNING: You may find that control-d (in emacs, control-c control-d)
can throw you completely out of Lisp where it had not formerly done so.

(CLISP and Allegro CL only) ACL2 now starts up inside the ACL2 loop --
that is, (LP) is executed automatically -- when built on CLISP or
Allegro CL.  This was already the case for GCL and CMUCL, and it still
is not true for LispWorks.  Thanks to Joe Corneli for bringing the CLISP
command-line option "-i" to our attention, which led to this CLISP
change and inspired reconsideration of how to do this for Allegro CL.

Pete Manolios and Daron Vroon have changed the representation of
ordinals in ACL2, defined algorithms for ordinal arithmetic, and
created a library of theorems to reason about ordinal arithmetic.  We
thank them for these nice contributions.  See NOTE-2-8-ORDINALS
for details, in particular, for how to preserve existing proofs that
depend on the previous ordinal representation.

Sometimes users create rules of class :rewrite that cause an infinite
loop in the ACL2 rewriter.  This has lead to Lisp stack overflows and
even segmentation faults.  Now, the depth of calls of functions in the
ACL2 rewriter is limited, and under user control.  See
REWRITE-STACK-LIMIT.

Macros mbe ("must be equal") and mbt ("must be true") have been
introduced, which allow the user to attach fast executable definitions
to (presumably slower) :logic mode functions.  Thanks to Vernon Austel
for a key idea.  Also provided is a macro defexec, which employs mbe
but enforces the requirement that the executable definition also
terminates.  Thanks to Jose Luis Ruiz Reina for collaborating in the
design and development of defexec, and for useful comments from a
number of others as well in the development of mbe including Joe
Hendrix and Rob Sumners.

Definitions have been added for functions rassoc-eq and rassoc-equal,
which are like rassoc but use different tests and have different
guards.  (Compare assoc-eq and assoc-equal, which are in similar
relation to assoc.)

The user can now control multiple matching for free variables in
hypotheses for :forward-chaining rules, as has already been supported
for :rewrite and :linear rules.  For :forward-chaining rules, "free
variables" are those in the hypotheses not bound by a given trigger
term.  As for :rewrite and :linear rules, free-variable matching may be
limited to the first successful attempt by specifying :match-free :once
with :forward-chaining in the :rule-classes, and
add-match-free-override may be used to modify the behavior of an
existing rule.  Thanks to Erik Reeber for most of the implementation of
these new capabilities, as well as significant assistance with a
corresponding new documentation topic (see
FREE-VARIABLES-EXAMPLES-FORWARD-CHAINING).

It is no longer necessary to specify (set-match-free-error nil) in order
to avoid errors when a rule with free variables in its hypotheses is
missing the :match-free field.  (This was already true during book
certification, but now it is the case in interactive sessions as well.)

The form (break-on-error) causes, at least for most Lisps, entry into
the Lisp debugger whenever ACL2 causes an error.  See
BREAK-ON-ERROR.  Thanks to John Erickson for providing encouragement
to provide this feature.

A new table has been provided so that advanced users can override the
built-in untranslate functionality.  See
USER-DEFINED-FUNCTIONS-TABLE.

The pstack mechanism (formerly denoted checkpoints) has been improved.
The "process [prover] stack," or pstack, is automatically printed when
proofs abort.  Evaluation of function calls on explicit arguments
during proofs is now tracked.  Actual parameters are shown with (pstack
t) rather than formals.  Thanks to Bill Legato for suggesting the first
two of these improvements and, in general, encouraging changes that
make ACL2 easier to use.

The defstobj event is now allowed to take an :inline argument, which
can speed up execution.  Thanks to Rob Sumners for suggesting and
implementing this new feature.

Macro assert$ has been added in order to make it easy to write
assertions in one's code.  Semantically, (assert$ test form) is the same
as form, but it causes a hard error (using illegal) if test evaluates
to nil.

Macro cw-gstack no longer takes arguments for the gstack or state.
However, it now takes a keyword argument (which is optional),
:evisc-tuple, that can be used to control how it prints terms.  In
particular, cw-gstack abbreviates large terms by default, but
(cw-gstack :evisc-tuple nil) causes terms to be printed in full.
Thanks to Robert Krug and Eric Smith for requesting this improvement.

The advanced user now has more control over the evisceration of terms.
See LD-EVISC-TUPLE, in particular the new paragraph on "The
printing of error messages and warnings."

The include-book event now has an additional (optional) keyword, :dir.
The value of :dir should be a keyword that is associated with an
absolute directory pathname to be used in place of the current book
directory (see CBD) for resolving the first argument of
include-book to an absolute pathname.  At start-up, the only such
keyword is :system, so that for example (include-book "arithmetic/top"
:dir :system) will include the book "arithmetic/top" under the "books/"
directory of your ACL2 installation.  But you can associate "projects"
with keywords using add-include-book-dir, e.g., (add-include-book-dir
:my-project "/u/smith/project0/").  See ADD-INCLUDE-BOOK-DIR
and also see DELETE-INCLUDE-BOOK-DIR and see
INCLUDE-BOOK.  Note: You will probably not find :dir :system to be
useful if the distributed books are not placed in the path of their
original location, pointed to by :dir :system, which will often happen
if the executable image is obtained from another site.  Also see
INCLUDE-BOOK, in particular its "soundness warning".

The printing of results in raw mode (see SET-RAW-MODE) may now
be partially controlled by the user:  see ADD-RAW-ARITY.  Also,
newlines are printed when necessary before the value is printed.

For those using Unix/Linux make: A cert.acl2 file can contain forms to
be evaluated before an appropriate certify-book command is invoked
automatically (not included in cert.acl2).

Jared Davis has contributed a new set of books for ordered finite set
theory to the standard distribution,
books/finite-set-theory/osets-0.81/.  See the README file in that
directory.  Thanks, Jared.

Robert Krug has contributed two related changes (thanks, Robert!) in
support of stronger arithmetic reasoning.  First, one can now enable
and disable nonlinear arithmetic with a :nonlinearp hint, which will
override the default provided by set-non-linearp (initially, nil).  See
HINTS.  Second, computed-hints can now have access to the
HISTORY, PSPV, and CTX variables of the waterfall, which (for example)
allows the writing of a hint which will enable nonlinear arithmetic on
precisely those goals that are stable-under-simplificationp.  See
COMPUTED-HINTS.

Robert Krug has contributed a new set of arithmetic books to the
standard distribution, books/arithmetic-3/.  See the README file in that
directory.  Thanks, Robert.

NOTE-2-8-ORDINALS    ACL2 Version  2.8 Notes on Changes to the Ordinals

Please see ORDINALS.

NOTE-2-8-OTHER    ACL2 Version  2.8 Notes on Miscellaneous Changes

Execution of table events has been sped up in many cases by avoiding
excessive consing.

ACL2 now warns if :rewrite (or :definition) rules contain free
variables on the right-hand side.  Thanks to Dave Greve for raising this
issue.

Emacs file emacs/emacs-acl2.el has been updated to better comprehend the
notion of the "ACL2 shell", which is the buffer to which ACL2 forms are
written by commands defined in the above file.  Thus, command control-t
e has been modified always to write to the ACL2 shell (which is
"*shell*" by default), and the following new commands have been defined.

     o control-t c
     Set the ACL2 shell to the current buffer.  o control-t b
     Change to the ACL2 shell.

The commands :pl and :pr may now be given a macro name that corresponds
via the macro-aliases-table to a function name, so that for example :pl
append is treated the same as :pl binary-append.  A more interesting
improvement, for :pl only, is that :pl may now take any term.  When :pl
is given a term other than a symbol, it will print all rewrite rules
that match that term.  Thanks to David Russinoff, Robert Krug, and Bill
Legato for getting this going.

A new function, pkg-witness, returns a symbol in the given package.

The installation instructions have been updated, for example to give
more guidance on obtaining Lisp implementations and to mention the
acl2-help mailing list.

Jared Davis has suggested some symbols to be added to *acl2-exports*,
and we have done so.  Thanks, Jared.

     o MFC (used in syntaxp and extended-metafunctions; thanks also to
     Robert Krug for this one) o ID, CLAUSE, WORLD, and
     STABLE-UNDER-SIMPLIFICATIONP (used   in computed-hints) o
     SET-DEFAULT-HINTS

The command :pe has been improved so that when the event is inside an
included book, the path of included books (from the top-level book down
to the one containing the event) is shown.  Thanks to Eric Smith
(perhaps among others) for pointing out the utility of this improvement.

A new release of the rtl library has been included: books/rtl/rel4/.
See the README file in that directory.

NOTE-2-8-PROOF-CHECKER    ACL2 Version  2.8 Notes on Proof-checker Changes

Added new proof-checker commands wrap1, wrap, and wrap-induct.  Wrap
replaces multiple goals by their conjunction: (wrap instr1 instr2 ...)
employs wrap1 so that the indicated instructions create only at most
one new goal.  Wrap-induct is a simple example of the use of wrap, so
that induction creates only one goal (the conjunction of the base and
induction steps).  Wrap1 can be used immediately after a prover call
(bash, prove, reduce, bdd, or induct) to collapse the new goals into
one.  See PROOF-CHECKER-COMMANDS.

The proof-checker command = failed to work as expected when a governing
IF-test of the current term is T.  This has been fixed (by fixing
source function conjuncts-of).  Thanks to Yoann Padioleau for bringing
this problem to our attention.

The type-alist command now takes optional arguments that control whether
or not the governors and/or conclusion are used in computing the context
that is printed (see PROOF-CHECKER-COMMANDS, specifically
subtopic type-alist).  Thanks to Rob Sumners for suggesting this
improvement.

The macro toggle-pc-macro has always taken an optional second argument
of atomic-macro or macro.  However, this was not clearly documented,
and those two symbols had to be in the ACL2 package.  Both of these
problems have been remedied.  Thanks to John Erickson for bringing the
lack of documentation of the second argument to our attention.

NOTE-2-8-PROOFS    ACL2 Version  2.8 Notes on Changes in Proof Engine

ACL2 now prevents certain rewriting loops; see
REWRITE-STACK-LIMIT.

During the computation of constraints for functional instantiation,
(prog2$ term1 term2) and (the type term2) are now treated as term2.

A change has been made in heuristics for controlling rewriting during
proofs by induction.  Formerly, during induction proofs, ACL2
suppressed rewriting of certain "induction hypothesis" terms, and
forced expansion of certain "induction conclusion" terms, until
rewriting had stabilized.  This meddling with the rewriter is still
turned off when rewriting has stabilized, but it is now turned off
earlier once an ancestor has been through the rewriter and the current
goal is free of "induction conclusion" terms.  Thanks to Dave Greve and
Matt Wilding for providing an example and associated analysis that led
us to look for a heuristic modification.

A change has been made in the heuristics for handling certain "weak"
compound-recognizer rules when building contexts.  Those who want to dig
deeply into this change are welcome to look at the code following the
call of most-recent-enabled-recog-tuple in the code for function
assume-true-false in the ACL2 sources.

The handling of free variables in a hypothesis of a rewrite rule (see
FREE-VARIABLES) has been improved in the case that the
hypothesis is of the form (equiv x y), where equiv is a known
equivalence relation (see EQUIVALENCE).  Previously, if the
rewriter was attempting to rewrite the hypothesis (equiv x y) of a
rewrite rule, in a context where x' is an instance of x, then the
rewriter could fail to notice a term (equiv x' y') true in the current
context where y' is an instance of y, in the case that x' precedes y'
in the term-order.  This has been remedied.  This improvement applies
regardless of whether x, y, or (we believe) both are already fully
instantiated in the present context.  Thanks to Joe Hendrix for
bringing up an example and to Vernon Austel for providing another,
simple example.

A very minor change has been made to the rewriter in the case that an
equality appears on the left-hand side of a :rewrite rule.  Formerly,
when such an equality (equal x y) was commuted to (equal y x) in order
for the rule to match the current term, then all equalities on the
instantiated right-hand side of the rule were commuted, except for
those occurring inside another equality.  The instantiated right-hand
side is no longer modified.  It seems very unlikely that this change
will cause proofs to fail, though we cannot completely rule out that
possibility.

We have modified how the ACL2 simplifier handles the application of a
defined function symbol to constant arguments in certain cases, which
we now describe.  As before, ACL2 attempts to simplify such a function
application by evaluation, provided the :executable-counterpart of the
function is enabled.  And as before, if that evaluation fails due to a
subroutine call of a constrained function (introduced by encapsulate),
ACL2 may wrap a call of hide around this function application.  (See
HIDE.)  But now, ACL2 attempts to apply definitions and rewrite
rules in the case that this evaluation fails, and only if the resulting
term is unchanged does ACL2 wrap hide around this function application.
Thanks to Matt Wilding for bringing up the idea of this modification.

The generation of "Goal" for recursive (and mutually-recursive)
definitions now uses the subsumption/replacement limitation (default
500).  See CASE-SPLIT-LIMITATIONS.

Default hints now apply to hints given in definitions, not just
theorems.  See DEFAULT-HINTS.

Thanks to Robert Krug for implementing the following two improvements
involving linear arithmetic reasoning: linear arithmetic now uses the
conclusions of forward-chaining rules, and type-set now uses a small
amount of linear reasoning when deciding inequalities.

NOTE-2-8-RULES    ACL2 Version  2.8 Notes on Changes in Rules, Definitions, and Constants

The theory minimal-theory has been changed by adding the definition
rune for mv-nth to the theory.  A corresponding change has been made to
the theory warning mechanism, which was failing to warn if the
definition of mv-nth is disabled, even though calls of mv-nth can be
expanded by special-purpose code in the rewriter.  Thanks to Serita Van
Groningen for pointing out this problem with the theory warning
mechanism.

The defevaluator event has been modified so that in the body of the
evaluator function, to add a new case (ATOM X) (returning nil) has been
inserted immediately after the case (EQ (CAR X) 'QUOTE).  This is a
no-op semantically but may speed up proofs.  Thanks to Warren Hunt for
suggesting this change.

A new form of :compound-recognizer rule is now allowed:

     (if (fn x) concl1 concl2)

This is equivalent to an existing form:

     (and (implies (fn x) concl1)
          (implies (not (fn x)) concl2))

Thanks to Josh Purinton for bringing this to our attention.

Rewrite rules realpart-+ and imagpart-+ have been added in order to
simplify the realpart and imagpart (respectively) of a sum.  They
follow from a theorem add-def-complex that equates a sum with the
complex number formed by adding real and imaginary parts.  All three of
these theorems may be found in source file axioms.lisp.  Thanks to Eric
Smith for raising a question leading to these additions, as well as to
Joe Hendrix and Vernon Austel for helpful suggestions.

NOTE-2-8-SYSTEM    ACL2 Version  2.8 Notes on System-level Changes

ACL2 now runs on OpenMCL, "an opensourced Common Lisp implementation,
derived from Digitool's Macintosh Common Lisp product."  Thanks to Greg
Wright and Robert Krug for doing most of the work for this port.

When (LP) is first executed, the underlying raw Lisp package will
change to "ACL2" (if that is not already the current package in raw
Lisp).  This is a minor change that will probably not be noticed, since
up to now it has probably been the case that the ACL2 executable starts
up with "ACL2" as the underlying raw Lisp package.  But this change was
made because we have been informed that ACL2 executables based on
OpenMCL need not start up with "ACL2" as the underlying raw Lisp
package.

ACL2 now runs on MCL 5.0.  Thanks to Pascal Costanza for updates to the
instructions in file mcl-acl2-startup.lisp and for an update to the
ACL2 sources (parameter *compiled-file-extension*).

NOTE-2-8(R)    ACL2 Version  2.8(r) (March, 2003) Notes

The Makefile has been modified by adding a new target, clean-links.
This can be used in order to remove all soft links, which is useful if
the directory is copied or moved to a new location or if there are file
system changes that cause problems with link pathnames.

Please also see NOTE-2-8 for changes to Version_2.8 of ACL2.

NOTE-2-9    ACL2 Version  2.9 (October, 2004) Notes

     *TABLE OF CONTENTS.*

     ==============================
     BUG FIXES.
     NEW FUNCTIONALITY.
     CHANGES IN PROOF ENGINE.
     GUARD-RELATED CHANGES.
     PROOF-CHECKER CHANGES.
     SYSTEM-LEVEL CHANGES.
     BOOK CHANGES.
     MISCELLANEOUS CHANGES.
     ==============================

*BUG FIXES.*

We fixed a soundness bug due to a conflict between user-supplied package
names and internal package names (obtained by prepending a Lisp
constant, *1*-package-prefix*) and user-supplied package names.  For
example, the form (defpkg "ACL2_*1*_MYPKG" ()) is no longer legal.
Thanks to Robert Krug for asking a question that led directly to the
discovery of this bug.

We fixed a soundness bug that allows :logic mode functions to call
:program mode functions.  The fix furthermore prevents functions with
guards verified from calling functions with guards not verified.  We
had thought we already prevented all this, but there was a problem with
the interaction of local definitions and redundancy checking (see
REDUNDANT-EVENTS).

We fixed a soundness bug that could occur when built-in functions were
called during macroexpansion (a hole in so-called "safe-mode").

Fixed a minor bug in system functions genvar1 and genvar, where eq had
been used in place of eql.  This bug was discovered during the plugging
of a hole in safe-mode, mentioned just above.

We fixed handling of the :inline keyword for defstobj, which previously
could cause raw Lisp errors in OpenMCL and CMU Common Lisp.  Thanks to
John Matthews for bringing this issue to our attention.

Calls of include-book could result in a state for which some function
definitions were not compiled that should have been.  The result could
be performance degradation or even stack overflows.  This situation
could arise in the following two ways.

     o Inclusion of a book with an absolute pathname that differs from
     the absolute pathname at certification time, presumably because of
     the use of soft links.  Thanks to Bob Boyer and Warren Hunt for
     bringing a stack overflow to our attention that led us to this fix.

     o Large mutual-recursion nests (more than 20 functions) are
     executed in a superior book.

We fixed some performance bugs that can increase the speed of
include-book calls by a factor of close to 2.  Thanks to Eric Smith for
asking if we could speed up include-book processing; we have done so in
the past, but primarily focusing on large mutual-recursion nests (which
have nothing in particular to do with the current improvements).  Also,
thanks to Rob Sumners for a very useful remark early in the process
that kept us from drawing an incorrect conclusion at that point.

We fixed :pl so that it can be run on a form that returns multiple
values, which it could not do previouslly.  Thanks to Eric Smith for
pointing out this problem.

Fixed a bug in the Allegro ACL2 trace utility (see TRACE$) that
was causing "10>" to be printed as "9>", "11>" to be printed as "10 >",
"12>" to be printed as "11 >", and so on.

Fixed a proof-checker bug that was preventing the use of the DV command
(or a numerical command) on let expressions.  Thanks to Bill Young for
pointing out this problem.

Fixed a bug in a comment on how to set ACL2_BOOKS_DIR in the makefile.
Thanks to Dave Greve for pointing out this problem.

Fixed a potential soundness bug in the linear arithmetic routines.
Thanks to Jared Davis for noticing this problem and to Robert Krug for
implementing the fix.  (Technical details: We had been assuming that
polynomials were being normalized - see the definition of good-polyp in
linear-a.lisp - but this assumption was false.)

When the macro open-trace-file is opened twice in succession, it now
automatically closes the first trace output channel before opening
another.

It is now possible to use make to build ACL2 on Windows systems that
support make.  Thanks to Pete Manolios and Mike Thomas for pointing out
the problem, to Jared Davis and Mike for helping us to analyze the
problem, and to Jared for testing the fix.

Fixed a bug in the guard of with-output that was causing a needless
guard violation.

*NEW FUNCTIONALITY.*

The new events add-default-hints and remove-default-hints allow one to
append to or subtract from the current list of default hints.  The
event set-default-hints continues to set the list of default hints,
discarding the previous value of the default-hints.  Note that
set-default-hints is still local to the encapsulate or book in which it
occurs, and add-default-hints has the same property, although neither
is implemented any longer using the acl2-defaults-table.  New events
add-default-hints!, remove-default-hints!, and set-default-hints! are
the same as add-default-hints, remove-default-hints, and
set-default-hints, respectively, except that the former three events
are not local to their enclosing encapsulate or book.  Thanks to Jared
Davis for suggesting these enhancements.

OpenMCL's tracing routines have been modified in a similar manner as
those of Allegro CL.  Thanks to Robert Krug for providing this
enhancement.

Guard-checking can now be caused to happen on recursive calls.  See
"GUARD-RELATED CHANGES" below for details.

Advanced users can now inhibit compilation of so-called "*1* functions"
with the :comp command; see COMP.  Thanks to Rob Sumners for
suggesting this enhancement.

Added new legal argument hard? for the er macro, which is now
documented.  See ER.  Thanks to Rob Sumners for a discussion
leading to this change.  Also, the three legal first arguments to er --
hard, hard?, and soft -- may now be in any package (thanks to Jared
Davis for bringing this issue to our attention).

We have removed the requirement that for a rule's hypothesis (bind-free
term var-list), at least one variable must occur free in term.  For
example, the expression (bind-free (bind-divisor a b) (x)) was legal
because a and b occur free in (bind-divisor a b); but (bind-free (foo
(bar)) (x)) was not legal.  The latter is no longer disallowed.
(Technical note: this allows bind-free to be used to create explicit
substitutions in metafunction hypotheses.)

The following two enhancements have been implemented for rules of class
:meta.  Thanks to Eric Smith for requesting more control of reasoning
with :meta rules, which led to these enhancements, and to him and
Robert Krug for helpful discussions.

     o It is now possible to control backchaining in rules of class
     :meta by providing a :backchain-limit-lst argument, as was already
     allowed for rules of class :rewrite and :linear.  See
     RULE-CLASSES.  However, unlike those other two rule classes, the
     value for :backchain-limit-lst is prohibited from being a
     non-empty list; it must be either nil or a non-negative integer.

     o (For advanced users.) It is now legal for hypothesis
     metafunctions to generate, in essense, calls of syntaxp and
     bind-free, handled essentially as they are handled in hypotheses
     of :rewrite and :linear rules.  We say "essentially" primarily
     because both syntaxp and bind-free are actually macros, but
     hypothesis metafunctions must generate translated terms (see
     TERM).  The enterprising advanced user can call :trans to see
     examples of translated terms corresponding to calls of syntaxp and
     bind-free.

A new command :trans! has been added, which is like :trans except that
:trans! ignored issues of single-threadedness.  See TRANS!.
Thanks to Eric Smith for suggesting this addition.

The :pf command now works when the argument is the name of a macro
associated with a function by macro-aliases-table.

*CHANGES IN PROOF ENGINE.*

The simplifier has been changed slightly in order to avoid using
forward-chaining facts derived from a literal (essentially, a top-level
hypothesis or conclusion) that has been rewritten.  As a practical
matter, this may mean that the user should not expect forward-chaining
to take place on a term that can be rewritten for any reason (generally
function expansion or application of rewrite rules).  Formerly, the
restriction was less severe: forward-chaining facts from a hypothesis
could be used as long as the hypothesis was not rewritten to t.  Thanks
to Art Flatau for providing an example that led us to make this change;
see the comments in source function rewrite-clause for details.

The rewriter has been modified to work slightly harder in relieving
hypotheses.  Thanks to Eric Smith for providing an example that
inspired the following, which illustrates the issue.  Suppose we
introduce functions foo and bar with the (non-local) properties shown
below.

      (encapsulate
       (((foo *) => *)
        ((bar *) => *))

       (local (defun foo (x) (declare (ignore x)) t))
       (local (defun bar (x) (declare (ignore x)) t))

       (defthm foo-holds
         (implies x
                  (equal (foo x) t)))
       (defthm bar-holds-propositionally
         (iff (bar x) t)))

Consider what happens when ACL2's rewriter is used to prove the
following theorem.

     (thm (foo (bar y)))

With ACL2's inside-out rewriting, (bar y) is first considered, but
rewrite rule bar-holds-propositionally does not apply because the
context requires preserving equality, not mere Boolean (iff)
equivalence.  Then the rewriter moves its attention outward and sees
the term (foo (bar y)).  It attempts to apply the rule foo-holds, in a
context created by binding its variable x to the term (bar y).  It then
attempts to relieve the hypothesis x of rule foo-holds in that context.
Before this change, ACL2 basically assumed that since rewriting was
inside out, then (bar y) had already been rewritten as much as
possible, so the rewrite of x in the aforementioned context (binding x
to (bar y)) simply returned (bar y), and the attempt to relieve the
hypothesis of foo-holds failed.  The change is essentially for ACL2's
rewriter to make a second pass through the rewriter when the attempt
fails to rewrite a variable to t, this time using the fact that we are
in a Boolean context.  (We mention that source function
rewrite-solidify-plus implements this idea, for those who want to dig
deeply into this issue.)  In our example, that means that the rewriter
considers (bar y) in a Boolean context, where it may apply the rule
bar-holds-propositionally to relieve the hypothesis successfully.

When (set-non-linearp t) has been executed, non-linear-arithmetic can
now be applied in some cases for which it previously was not.  Thanks
to Robert Krug for supplying this modification and to Julien Schmaltz
for providing a motivating example.

We modified the rewriter to avoid certain infinite loops caused by an
interaction of the opening of recursive functions with equality
reasoning.  (This change is documented in detail in the source code, in
particular functions rewrite-fncall and fnstack-term-member.)  Thanks
to Fares Fraij for sending us an example that led us to make this
change.

The :executable-counterpart of function hide is now disabled when ACL2
starts up.  This removes an anomoly, for example that

     (thm (not (equal 1 (* (hide 0) a))))

succeeded while

     (thm (equal (foo (equal 1 (* (hide 0) a))) (foo nil)))

failed.  Now both fail.

The theory *s-prop-theory* is no longer used by the proof-checker; it
has been replaced by (theory 'minimal-theory.  We have left the
constant *s-prop-theory* defined in the source code in support of
existing books, however.  This change eliminates annoying theory
warnings printed upon invocation of proof-checker commands s-prop, sl,
and split.

Terms are now kept in an internal form that avoids calls of primitive
functions (built-ins without explicit definitions; see code for
cons-term for details), in favor of the constants that result from
evlaluating those calls.  So for example, the internal form for (cons 1
2) is (quote (1 . 2)).  This change was made at around the same time as
changes in support of bind-free; see above.  One consequence is that the
splitting of goals into cases (technically, source function clausify and
even more technically, source function call-stack) has been modified,
which can cause subgoal numbers to change.

*GUARD-RELATED CHANGES.*

Guard-checking can now be caused to happen on recursive calls, where
this was formerly not the case for :program mode functions and, perhaps
more important, for :logic mode functions whose guards have not been
verified.  Moreover, a warning is printed when ACL2 does not rule out
the exclusion of guard-checking on recursive calls.  See
SET-GUARD-CHECKING.  Thanks to David Rager for bringing this issue to
our attention, and to Rob Sumners and the Univ. of Texas ACL2 seminar
in general for their feedback.

Guard violations are reported with less of the offending term hidden.
Thanks to Jared Davis for suggesting that we look at this issue.

*PROOF-CHECKER CHANGES.*

We fixed the proof-checker so that diving works as you might expect for
a macro call (op a b c) representing (binary-op a (binary-op b c)).  In
the past, if the current term was of the form (append t1 t2 t3), then
(DV 3) (and 3) would dive to t3 even though the corresponding function
call is (binary-append t1 (binary-append t2 t3)).  This is still the
case, but now this behavior holds for any macro associated with a
function in binop-table (see ADD-BINOP).  Moreover, users can
now write customized diving functions; see
DIVE-INTO-MACROS-TABLE, and also see books/misc/rtl-untranslate.lisp
for example calls to add-dive-into-macro.  Of course, the old behavior
can still be obtained using the proof-checker's DIVE command; see
PROOF-CHECKER-COMMANDS.

The runes command in the proof-checker now shows only the runes used by
the most recent primitive or macro command (as shown by :comm), unless
it is given a non-nil argument.  Also, proof-checker command
lemmas-used has been added as, in essence, an alias for runes.

(The following two items are also mentioned above under "BUG FIXES.")

Fixed a proof-checker bug that was preventing the use of the DV command
(or a numerical command) on let expressions.  Thanks to Bill Young for
pointing out this problem.

The theory *s-prop-theory* is no longer used by the proof-checker; it
has been replaced by (theory 'minimal-theory.  We have left the
constant *s-prop-theory* defined in the source code in support of
existing books, however.  This change eliminates annoying theory
warnings printed upon invocation of proof-checker commands s-prop, sl,
and split.

*SYSTEM-LEVEL CHANGES.*

Fixed a problem with building ACL2 on CMUCL in some systems (source
function save-acl2-in-cmulisp).  Thanks to Bill Pase for bringing this
to our attention.

The installation instructions have been extended to include
instructions for building on GCL in Mac OS X.  Thanks to Jun Sawada and
Camm Maguire.

Initial pre-allocation of space has been updated for GCL to reflect more
current GCL executables (we considered GCL 2.6.1-38).  This can help
avoid running out of memory for large ACL2 sessions.

The main Makefile has been replaced by GNUmakefile, in order to enforce
the use of GNU make.  If you use another make program, you'll get an
error message that may help you proceed.

(GCL only) SGC is no longer turned on for GCL 2.6 sub-versions through
2.6.3 if si::*optimize-maximum-pages* is bound to T, due to an apparent
issue with their interaction in those sub-versions.  Also, we have
eliminated preallocation for all versions after 2.6.1 because GCL
doesn't need it (comments are in source function save-acl2-in-akcl).
Thanks to Camm Maguire for excellent GCL help and guidance, and to Camm
and Bob Boyer for useful discussions.

We have removed support for so-called "small" images.  Thus, :doc, :pe
and :pc, verify-termination, and other commands are fully supported in
ACL2 saved images.  Because of this and other changes in the generation
of the so-called "*1*" logical functions, related to guards (as
described above in -GUARD-RELATED CHANGES", and related to the
discussion of safe-mode in "BUG FIXES" above), image sizes have
increased substantially.

We no longer time or run "nice" the certification of individual books.
The file books/Makefile-generic had done these by default, and some
individual distributed and workshop book directories had Makefiles that
did so as well.  Thanks to Mike Thomas, who pointed out the lack of
nice on some Windows systems (and we decided on this simple solution).
Overall targets in books/Makefile still time their runs by default, and
the partiular time program is now controlled by a Makefile variable.

Failures during make certify-books or make regression now show up in
the log as "**CERTIFICATION FAILED**", regardless of the operating
system (as long as it supports make).  Formerly, one searched for "**"
but this did not appear in openMCL runs.

We have eliminated "Undefined function" warnings that could occur in
OpenMCL.

*BOOK CHANGES.*

Reconciled the definitions of firstn in book/misc/csort.lisp,
books/bdd/bdd-primitives.lisp, books/ordinals/ordinal-definitions.lisp,
and books/data-structures/list-defuns.lisp.  Thanks to Ray Richards for
bringing this issue to our attention.

Distributed book books/misc/defpun now can handle stobjs where it did
not previously.  Thanks to John Matthews for bringing this issue to our
attention.

The "make" variable COMPILE_FLG in file books/Makefile-generic formerly
only had an effect if there was a cert.acl2 file present.  That
oversight has been remedied.

File "books/arithmetic/certify.lsp" was missing a certify-book command
for "natp-posp".  Thanks to John Cowles for noticing this deficiency
and supplying a fix.  (This file is of use to those who want to certify
the "books/arithmetic/" books without using "make".)

A few small changes have been made to "books/rtl/rel4".

Small changes were made to books misc/symbol-btree and
misc/rtl-untranslate.  In particular, the definition of symbol-btreep
was strengthened.

We made a minor fix to books/ordinals/e0-ordinal.lisp, adding
(verify-guards ob+) and hence (verify-guards ocmp) as well.  This was
necessitated by the fix prohibiting functions with guards verified from
calling functions with guards not verified (see also the related
discussion under "BUG FIXES" above).

*MISCELLANEOUS CHANGES.*

Further sped up processing of large mutual-recursion nests (extending
what was done for Version_2.7), perhaps by a factor of two in some
cases.

As promised in Version_2.5 (see NOTE-2-5), structured pathnames
are no longer supported.  So for example, the argument to include-book
must now be a string constant.

Some documentation has been improved, for stobjs thanks to suggestions
by John Matthews and much of the rest thanks to feedback from Eric
Smith.

The function current-package is now available to users (it has been
taken off the list of so-called "untouchables").  Thanks to Jared Davis
for bringing this issue to our attention.

The documentation for topic using-computed-hints-7 has been improved.
Thanks to Doug Harper and Eric Smith for inspiring this improvement.

We added several symbols to *acl2-exports*: cw, er, intern$,
set-case-split-limitations, and set-difference-eq.  Thanks to Jared
Davis for suggesting most of these.

Now, a table event that sets the value for a key, (table tbl key val
:put), is redundant (see REDUNDANT-EVENTS) when it does not
change the value associated with an existing key of the table.  In
particular, define-pc-macro is now fully redundant when it does not
change an existing proof-checker macro-command definition.  Thanks to
Bill Young for bringing the latter issue to our attention.

The definitions of unused system functions ev-w and ev-w-lst have been
deleted.

ACL2 now prints a warning if a defpkg event introduces a package name
with lower-case letters, since there is opportunity for later confusion
in that case.  Thanks to Frederic Peschanski for bringing this problem
to our attention and Sandip Ray for encouragement.

ACL2 now works in Version 19 of CMU Common Lisp.

The function sys-call has been modified so that for ACL2 built on
Allegro Common Lisp in Unix or Linux, the existing environment is used.
Thanks to Erik Reeber for bringing this issue to our attention.

The function disabledp can now be given a macro name that has a
corresponding function; see MACRO-ALIASES-TABLE.  Also,
disabledp now has a guard of t but causes a hard error on an
inappropriate argument.

NOTE-2-9(R)    ACL2 Version  2.9(r) (October, 2004) Notes

No changes have been made for support of non-standard analysis, other
than a minor modification or two in books/nonstd/ books.

Please also see NOTE-2-9 for changes to Version_2.9 of ACL2.

NOTE-2-9-1    ACL2 Version  2.9.1 (December, 2004) Notes

(GCL only) A bug in symbol-package-name has been fixed that could be
exploited to prove nil, and hence is a soundness bug.  Thanks to Dave
Greve for sending us an example of a problem with defcong (see below)
that led us to this discovery.

ACL2 now warns when defcong specifies equal as the first equivalence
relation, e.g., (defcong equal iff (member x y) 2).  The warning says
that the rule has no effect because equal already refines all other
equivalence relations.  Formerly, this caused an error unless
:event-name was supplied (see DEFCONG), and in fact the error
was a nasty raw Lisp error on GCL platforms due to some mishandling of
packages by ACL2 that has been fixed (see the paragraph about
symbol-package-name above).  Thanks to Dave Greve for sending a helpful
example in his report of this problem.

(GCL only) The build process was broken for GCL 2.6.0 (and perhaps some
earlier versions), and has been fixed.  Thanks to Jose Luis Ruiz-Reyna
for bringing this problem to our attention.

(GCL only) We have increased the hole size to at least 20% of max-pages,
which may eliminate some garbage collection at the expense of larger
virtual memory (not larger resident memory or larger image).  Thanks to
Camm Maguire for helpful explanations on this topic.

We have clarified the guard warning message that is printed during
evaluation of recursively-defined functions whose guards have not been
verified, for example:

       ACL2 Warning [Guards] in TOP-LEVEL:  Guard-checking may be inhibited
       on some recursive calls of executable counterparts (i.e., in the ACL2
       logic), including perhaps EVENLP.  To check guards on all recursive
       calls:
         (set-guard-checking :all)
       To leave behavior unchanged except for inhibiting this message:
         (set-guard-checking :nowarn)

And, ACL2 no longer prints that message when the guard was unspecified
for the function or was specified as T.  Thanks to Serita Nelesen for
bringing the latter issue to our attention.  Finally, ACL2 now prints
such a warning at most once during the evaluation of any top-level
form; thanks to Bill Young for pointing out this issue.

The function verbose-pstack has been enhanced to allow specified prover
functions *not* to be traced.  See VERBOSE-PSTACK.

Added lp, wet, and set-non-linearp to *acl2-exports*, and hence to the
"ACL2-USER" package.

The distributed book books/arithmetic-3/bind-free/integerp.lisp has
been modified in order to prevent potential looping; specifically, the
definition of function reduce-integerp-+-fn-1.  Thanks to Robert Krug
for providing this change.

A small improvement was made in the wet failure message when the error
occurs during translation to internal form.  Thanks to Jared Davis for
pointing out the obscurity of some wet error messages.

We have improved ACL2's evaluation mechanism for the function
bad-atom<=, which now is specified to return nil if neither argument is
a so-called "bad atom" (as recognized by function bad-atom).  The
following events had caused a hard error, for example.  (We're sorry
that bad-atom and bad-atom<= are not documented, but we also consider
it unlikely that anyone needs such documentation; otherwise, please
contact the implementors.)

     (defun foo (x y) (declare (xargs :guard t)) (bad-atom<= x y))
     (defun bar (x y) (declare (xargs :guard t)) (foo x y))
     (thm (equal (bar 3 4) 7))

We have also changed the guard on alphorder to require both arguments
to be atoms.

For forms (local x) that are skipped during include-book, or during the
second pass of certify-book or encapsulate, ACL2 had nevertheless
checked that x is a legal event form.  This is no longer the case.

The proof-checker now does non-linear arithmetic when appropriate.  It
had formerly ignored set-non-linearp executed in the ACL2 command loop.

Incremental releases are now supported.  See VERSION and see
SET-TAINTED-OKP.  Thanks to Hanbing Liu for discovering a flaw
in our original design.

The pattern-matching algorithm for :rewrite rules has been made
slightly more restrictive, thanks to a suggestion and examples from
Robert Krug.  For example, previously one could get an infinite loop as
follows.

     (defstub foo (x) t)
     (defaxiom foo-axiom
       (equal (foo (+ 1 x))
              (foo x)))
     (thm (foo 0)) ; or replace 0 by any integer!

That is because the term (foo 0) was considered to match against the
pattern (foo (+ 1 x)), with x bound to -1.  While such matching is
sound, it leads to an infinite loop since it allows foo-axiom to
rewrite (foo 0) to (foo -1), and then (foo -1) to (foo -2), and so on.
The fix is to insist that the new value, in this case -1, is no larger
in size according to acl2-count than the old value, in this case 0.
Since that test fails, the match is considered to fail and the loop no
longer occurs.  An analogous fix has been made for multiplication,
where now we only match when the new term is still a non-zero integer.
That change avoids a loop here.

     (defstub foo (x) t)
     (defaxiom foo-axiom
       (equal (foo (* 2 x))
              (foo x)))
     (thm (foo 0)) ; or try (thm (foo 4))

Added macro find-lemmas in books/misc/find-lemmas.lisp (see brief
documentation there) for finding all lemmas that mention all function
symbols in a given list.

:Restrict hints now work for :definition rules, though they continue to
be ignored by the preprocessor and hence you may want to use :do-not
'(preprocess) with any restrict hints.  Thanks to John Matthews for
pointing out the lack of support for :definition rules in :restrict
hints.

Some books have been updated.  In particular, there is a new directory
books/workshops/2004/ in workshops distribution, for the 2004 ACL2
workshop.  There is also a new version of Jared Davis's ordered sets
library, formerly in books/finite-set-theory/osets-0.81/ but now in
books/finite-set-theory/osets/.

Fixed a bug in the (under-the-hood) raw Lisp definition of defchoose,
which had been causing a warning in CMU Common Lisp.

[Technical improvements related to the use of "make dependencies" for
certifying distributed books:]
File books/Makefile-generic now does a better job with "make
dependencies," specifically with respect to handling *.acl2 files and
handling include-book commands with :dir :system.  Regarding the
latter, suppose for example that book basic.lisp contains the line:

     (include-book "arithmetic/top-with-meta" :dir :system)

Then make dependencies would generate the following line:

     basic.cert: $(ACL2_SRC_BOOKS)/arithmetic/top-with-meta.cert

Thus, if :dir :system is used with include-book, the corresponding
Makefile should define the variable ACL2_SRC_BOOKS.  A standard
Makefile header for a books directory could thus be as follows.

     # The following variable should represent the ACL2 source directory.  It is the
     # only variable in this Makefile that may need to be edited.
     ACL2_SRC = ../../../../../..

     ACL2_SRC_BOOKS = $(ACL2_SRC)/books
     include $(ACL2_SRC_BOOKS)/Makefile-generic
     ACL2 = $(ACL2_SRC)/saved_acl2

Finally, the "-s" flag may now be omitted when running "make
dependencies."

NOTE-2-9-2    ACL2 Version  2.9.2 (April, 2005) Notes

Also see NOTE-2-9-1 for other changes since the last
non-incremental release (Version_2.9).

There was a bug in non-linear arithmetic (see
NON-LINEAR-ARITHMETIC) that caused the following error:

     ACL2 !>(include-book "rtl/rel4/lib/top" :dir :system)
     ....
     ACL2 !>(set-non-linearp t)
      T
     ACL2 !>(thm
      (implies (and (bvecp a 77)
                    (bvecp b 50))
               (bvecp (fl (/ (* a b) (expt 2 23)))
                      104))
      :hints (("Goal" :in-theory (enable bvecp))))

     [Note:  A hint was supplied for our processing of the goal above.
     Thanks!]

     By the simple :definition BVECP, the :executable-counterparts of EXPT
     and UNARY-/ and the simple :rewrite rule ASSOCIATIVITY-OF-* we reduce
     the conjecture to

     Goal'
     (IMPLIES (AND (INTEGERP A)
                   (<= 0 A)
                   (< A 151115727451828646838272)
                   (INTEGERP B)
                   (<= 0 B)
                   (< B 1125899906842624))
              (BVECP (FL (* A B 1/8388608)) 104)).

     HARD ACL2 ERROR in VARIFY:  This should not have happened.  The supposed
     variable, '1/8388608, is instead a constant.

     ACL2 !>

Thanks to Robert Krug for providing a fix for the above error.

Guard-checking was being inhibited (since v2-9) for calls of built-in
primitives on explicit values, e.g., (car 3).  This has been fixed.

Guard-related warnings could be printed during proofs (this bug was
introduced in Version_2.9.1).  These warnings have been eliminated.

Compound-recognizer rules natp-compound-recognizer and
posp-compound-recognizer are now built into ACL2 for predicates natp
and posp, and hence have been deleted from book natp-posp.lisp (where
they were called natp-cr and posp-cr, respectively).

The function file-clock-p, which recognizes a component of the ACL2
state, is now defined using natp instead of integerp.  Thanks to Jared
Davis for suggesting this change.  (Technical explanation about
functions in ACL2 source file axioms.lisp: With a file-clock of -1, the
call of make-input-channel in open-input-channel will create a channel
that can't be closed; see the guard of close-input-channel.)

(Allegro CL users only) Support is now provided for building an Allegro
CL application, provided you have an Allegro CL dynamic runtime
license.  (Our belief is that with such a license, many users can use
the same application, rather than each user needing a separate
license.)  See new GNUmakefile target allegro-app and file
build-allegro-exe.cl for more information.

The new home page now contains a link to a new page other-releases.html,
which contains information about other ACL2 releases.  (This is in one's
local home page, but may not show up on the central ACL2 home page
until the next non-incremental release.)  Thanks to Warren Hunt for
suggesting this addition.

We thank Erik Reeber for suggesting a solution to output redirection
using sys-call, which we have described at the end of its documentation.

A new documentation topic fixes the flawed argument for conservativity
of the defchoose event that appears in Appendix B of Kaufmann and
Moore's paper, "Structured Theory Development for a Mechanized Logic"
(Journal of Automated Reasoning 26, no. 2 (2001), pp. 161-203).  See
CONSERVATIVITY-OF-DEFCHOOSE.  Thanks to John Cowles and Ruben
Gamboa for helpful feedback on drafts of this note.

The solution to exercise 6.15 in books/textbook/chap6/solutions.txt has
been fixed.  Thanks to Aaron Smith for pointing out the problem.

A new documentation topic defun-sk-example gives a little more help in
using defun-sk effectively.  Thanks to Julien Schmaltz for presenting
this example as a challenge.

(GCL only) There is now a way to speed up GCL builds of ACL2, at the
cost of perhaps a percent or so in performance of the resulting image.
Using make one supplies the following.

     LISP='gcl -eval "(defparameter user::*fast-acl2-gcl-build* t)"

Various makefiles have been improved in several ways.

     (1) Parallel book certification, using GNU make's -j option, can
     be used.

     (2) Book certifications now stops at the first failure if
     books/Makefile or books/Makefile-generic is used, and returns
     non-zero exit status.  However, the various make targets in the
     ACL2 source directory (regression, certify-books, etc.) still
     continue past failures unless you provide ACL2_IGNORE=' ' on the
     make command line.

     (3) The build process has been modified (file GNUmakefile) so that
     it stops upon a failed compile or a failed initialization.

     (4) The automatic dependency generation (from "make dependencies"
     has been improved so that commands of the form (ld "my-book.lisp")
     in .acl2 files cause the appropriate depedencies to be generated.

Thanks to comments from several users that led to the above Makefile
improvements: Ray Richards, Doug Harper, and the Rockwell ACL2 users
for (1) and (2) (and inspiring (4)), and David Rager for (2) and (3).
In particular, Doug Harper sent a replacement for the .date mechanism,
which was interfering with make -n; so, these files are no longer
written.

A mechanism has been added for saving output.  In particular, you can
now call ld on a file with output turned off, for efficiency, and yet
when a proof fails you can then display the proof attempt for the
failed (last) event.  See SET-SAVED-OUTPUT.  Another new
command -- see SET-PRINT-CLAUSE-IDS -- causes subgoal numbers
to be printed during proof attempts when output is inhibited.

Documentation has been added for using ACL2's makefile support to
automate the certification of collections of books.  See
BOOK-MAKEFILES.

Fixed a bug in sys-call-status that was causing hard Lisp errors.

Improved cw-gstack to allow a :frames argument to specify a range of
one or more frames to be printed.  see CW-GSTACK.

Fixed a bug in proof-checker command forwardchain.  Thanks to Ming-Hsiu
Wang for bringing this bug to our attention.

We have provided a mechanism for saving an executable image.  See
SAVING-AND-RESTORING and see SAVE-EXEC.  We have eliminated
obsolete functions note-lib and make-lib.

Modified the ground-zero theory so that it contains all of the built-in
rules (in ACL2 source file axioms.lisp).  It had formerly failed to
include rules from some definitions and theorems near the end of
axioms.lisp.

A new event, set-enforce-redundancy, allows the enforcement of defthm,
defun, and most other events during book development.  See
SET-ENFORCE-REDUNDANCY.

A bug has been fixed that had allowed deftheory events to cause a hard
Lisp error when calling union-theories on ill-formed theories after,
for example:

     :set-guard-checking nil
     (in-theory (union-theories '((:rewrite no-such-rule))
                                (current-theory 'ground-zero)))

The handling of guard checking has been modified somewhat in a way that
should only very rarely affect users.  (An "Essay on Guard Checking" in
the ACL2 source code explains this point to anyone interested in
implementation details.)

(GCL ONLY) Removed the -dir setting in the ACL2 wrapper script for GCL.
This should generally have no effect for most users, but it eliminates
a potential source of error down the road.

Several interesting new definitions and lemmas have been added to the
rtl library developed at AMD, and incorporated into books/rtl/rel4/lib/.
Other book changes include a change to lemma truncate-rem-elim in
books/ihs/quotient-remainder-lemmas.lisp, as suggested by Jared Davis.

The macro real/rationalp may now be referred to in in-theory events and
hints, thanks to a new add-macro-alias event.  Thanks to Jared Davis
for this suggestion.

ACL2 terms of the form (if p 'nil 't) are now printed as (not p), where
in some setting they had been printed as (and (not p) t).  Thanks to
Robert Krug for this improvement.

(GCL ONLY) Added profiling support, based heavily on code supplied by
Camm Maguire.  See file save-gprof.lsp for instructions.  Thanks to
Camm, and also to David Hardin for inspiring this addition.

Added support for preprocessing before printing (untranslating) a term.
See USER-DEFINED-FUNCTIONS-TABLE, in particular the discussion
of untranslate-preprocess.  Thanks to Jared Davis for inspiring this
addition, and for providing a book that takes advantage of it
(books/misc/untranslate-patterns.lisp).

The documentation has been improved for explaining how runes are
assigned; see RUNE.  Thanks to Robert Krug for pointing out
inaccuracies in the existing documentation.

NOTE-2-9-3    ACL2 Version  2.9.3 (August, 2005) Notes

Also see NOTE-2-9-1 and see NOTE-2-9-2 for other
changes since the last non-incremental release (Version_2.9).

We fixed a soundness bug that exploited the ability to define :program
mode functions that are improperly guarded, and then to use those
functions in defconst forms.  The fix is to evaluate defconst forms
using the same "safe-mode" that is used in macroexpansion (see
GUARDS-AND-EVALUATION).  Here is a proof of nil that succeeded in
Allegro Common Lisp (but not, for example, GCL).  See also a long
comment in source function defconst-fn for an example that does not
require the use of :set-guard-checking.

     :set-guard-checking nil ; execute before certifying the book below

     (in-package "ACL2")

     (encapsulate
      ()
      (local (defun f1 ()
               (declare (xargs :mode :program))
               (char-upcase (code-char 224))))
      (local (defconst *b* (f1)))
      (defun f1 ()
        (char-upcase (code-char 224)))
      (defconst *b* (f1))
      (defthm bad
        (not (equal *b* (code-char 224)))
        :rule-classes nil))

     (defthm ouch
       nil
       :hints (("Goal" :use bad))
       :rule-classes nil)

We fixed a soundness hole due to the fact that the "LISP" package does
not exist in OpenMCL.  We now explicitly disallow this package name as
an argument to defpkg.  Thanks to Bob Boyer and Warren Hunt for bringing
an issue to our attention that led to this fix.

ACL2 now requires all package names to consist of standard characters
(see STANDARD-CHAR-P, none of which is lower case.  The reason
is that we have seen at least one lisp implementation that does not
handle lower case package names correctly.  Consider for example the
following raw lisp log (some newlines omitted).

     >(make-package "foo")
     #<"foo" package>
     >(package-name (symbol-package 'FOO::A))
     "foo"
     >(package-name (symbol-package '|FOO|::A))
     "foo"
     >

Distributed book books/textbook/chap10/compiler, as well as workshop
books in directory books/workshops/2004/cowles-gamboa/support/, were
modified to accommodate the above change.

Added newline, add-to-set-eql, the-fixnum, and the-fixnum!  to
*acl2-exports*.  Thanks to Jared Davis for bringing these to our
attention.

Added a line to acl2.lisp to support CMUCL running on Mac OSX, thanks to
a suggestion from Fabricio Chalub Barbosa do Rosario.

The executable scripts for saved ACL2 images now include $*, so that
command-line arguments will be passed along.

(For GCL profiling only) Fixed a colon (:) that should have been a
semicolon (;) in file save-gprof.lsp.  Thanks to David Hardin for
pointing out this bug.

The documentation for :elim rules has been expanded and improved,
thanks to useful feedback from Hanbing Liu.

Fixed a bug in the guard for function include-book-dir.

For those who want to experiment with an alternate implementation of mv
and mv-let, there is now support for under-the-hood implementation of
these in terms of raw Lisp functions values and multiple-value-bind,
respectively.  The regression suite has seen about a 10% speed-up in
Allegro CL and about an 8% slowdown in GCL for builds with this change.
See the makefile (GNUmakefile) for examples of how to build ACL2 by
including the feature, :acl2-mv-as-values.  Source file init.lsp has
been renamed to init.lisp in support of this change (technical detail:
otherwise GCL loads the init file too soon, before its -eval argument
is evaluated).  Thanks to David Rager for inspiring this change, by
pointing out the problematic use of globals by the existing mv
implementation from the standpoint of supporting parallel evaluation.
This capability is experimental: there is likely to be some remaining
work to be done on it.

A change related to the one just above is that we now limit the maximum
number of arguments to any call of mv to 32.  Thanks to Bob Boyer for
raising a question that lead to this change.

Eliminated some compiler warnings in OpenMCL.

In the rtl library (books/rtl/rel4/), functions bits and setbits have
had their guards improved (as they had been too restrictive, especially
for setbits).

A new function time$ permits timing of forms, by using (under the hood)
the host Common Lisp's time utility.

We fixed an infinite loop that could occur during destructor elimination
(see ELIM).  Thanks to Sol Swords to bringing this to our
attention and sending a nice example, and to Doug Harper for sending a
second example that we also found useful.

The method of speeding up GCL-based builds (see NOTE-2-9-2) has
changed slightly from Version_2.9.2.  Now, in the make command:

       LISP='gcl -eval "(defparameter user::*fast-acl2-gcl-build* t)"

We improved the pretty-printer's handling of keywords.  For example,
before this change one might see the following printed by ACL2.

     (MODIFY TH S :KEY1 VAL1 :KEY2
             (IF (IF X Y Z) AAAAAAAAAA BBBBBBB))

Now, the above might print as follows.  Notice that we have avoided
breaking after a keyword (see KEYWORDP) that is preceded by
other forms on the same line.

     (MODIFY TH S
             :KEY1 VAL1
             :KEY2 (IF (IF X Y Z) AAAAAAAAAA BBBBBBB))

See NOTE-2-9-3-PPR-CHANGE for a detailed discussion of this
change.

(GCL ONLY) Evaluation in a break is no longer inhibited by ACL2 when
built on top of GCL, so GCL now matches other Common Lisps in this
respect.

For ACL2 built on most host Common Lisps, you will see the string [RAW
LISP] in the prompt, at least at a break, to emphasize that one is
inside a break and hence should probably quit from the break.  See
BREAKS.

Jared Davis suggested improvements to lemmas len-update-nth (in source
file axioms.lisp) and append-true-listp-type-prescription (in
books/meta/term-defuns.lisp), which have been incorporated.  The former
required a change in books/workshops book
2004/ruiz-et-al/support/q-dag-unification.cert, which has been made.

The proof-checker command rewrite allows further binding of free
variables in hypotheses, with new optional argument instantiate-free.
Proof-checker command show-rewrites (sr) gives corresponding additional
information.  Documentation for these commands has been improved; see
PROOF-CHECKER-COMMANDS.  Thanks to John Matthews and Bill Young
for suggestions and feedback leading to these improvements.

Fixed downcase printing so that the package name of a symbol is also
downcased.  For example, after execution of (defpkg "FOO" nil) and
(set-acl2-print-case :downcase), 'foo::ab will print back as the same,
rather than as 'FOO::ab.

It is now possible to control the output so that numbers are printed in
binary, octal, or hex, though the default is still radix 10.  See
SET-PRINT-BASE.  Note that in support of this change, built-in
functions explode-nonnegative-integer and explode-atom now take an
extra print-base argument.  Different support for radix conversion may
be found in a book newly contributed by Jun Sawada,
books/misc/radix.lisp.

Built-in axiom car-cdr-elim is now only an :elim rule.  It was formerly
both an :elim rule and a :rewrite rule.  A new rule, cons-car-cdr,
takes the place of the old :rewrite rule, but is instead a
hypothesis-free rule that can cause a case split (see source file
axioms.lisp).  Thanks to Jared Davis for suggesting this change.

Lemmas about alphorder (alphorder-reflexive, alphorder-transitive,
alphorder-anti-symmetric, and alphorder-total) are now available.
(They had been local in source file axioms.lisp.)  Thanks to Serita
Nelesen for bringing this issue to our attention.

ACL2 has, for some time, printed a space in the event summary after the
open parenthesis for a defthm event, in order to ease backward
searching for the original form, for example (defthm bar ...):

     Form:  ( DEFTHM BAR ...)

The intention was that this extra space should be printed for every
event form; but it was missing in some cases, for example, for
verify-guards.  This has been fixed.

In analogy to include-book, now ld takes the (optional) keyword
argument :dir.  Thanks to Jared Davis for providing an implementation of
this feature and to Eric Smith and Jeff Marshall for requesting this
feature.

We fixed a bug in include-book that could cause an error when
redefinition is on, for example:

     (set-ld-redefinition-action '(:warn! . :overwrite) state)
     (include-book "/u/acl2/books/arithmetic/top")

The behavior of include-book now matches the documentation: handling of
compiled files for uncertified books will follow the same rules as for
certified books.  In particular, if you create an object file in raw
Lisp for some book, then including that book will load that object
file.  Thanks to Jared Davis for bringing this issue to our attention.

New documentation explains the interaction of redefinition and
redundancy.  See REDUNDANT-EVENTS -- the "Note About
Unfortunate Redundancies" is new.  Thanks to Grant Passmore for
providing examples that led us to write this additional documentation.

Solutions to exercises in "How To Prove Theorems Formally"
(`http://www.cs.utexas.edu/users/moore/publications/how-to-prove-thms')
are now available in distributed book books/misc/how-to-prove-thms.lisp.
Also in that directory may be found a new book hanoi.lisp that contains
a solution to the Towers of Hanoi problem.

NOTE-2-9-3-PPR-CHANGE    change in pretty-printing for ACL2 Version_2.9.3

We have improved pretty-printing in ACL2 Version_2.9.3 to handle
keywords a little differently.  To see a discussion of the basics of
this change, see NOTE-2-9-3.  In this note we describe it in
considerable detail.

Those who wish to understand the ACL2 pretty-printer's implementation
can now find considerably more comments on it in the source code.  In
this note, we do not focus on the implementation.  Rather, we motivate
the change and show how the improved prettyprinter performs.

Why do we want better keyword handling?  Imagine a macro that builds a
new state from an old state by changing the values in the affected
fields, leaving everything else unchanged.  One could write

     (modify th s :key1 val1 :key2 val2 :key3 val3)

where the three keys identify fields in the state.

To make it easier to read new concrete states, we may have a function
that prints them "relative" to a given base state, expressing the new
state as a modification of the given base state.  So we may find
ourselves prettyprinting modify forms like that above.

The previous prettyprinter will sometimes print the form above as
follows.

     (modify th s :key1
             val1
             :key2 val2 :key3 val3)

This can be unpleasant to read, because of the way :key1 and val1 are
separated.  Here is an example of the old prettyprinter and the new
one, both printing an expression from the ACL2 source code in a width
of 40:

     Old:
     (ADD-TO-TAG-TREE
      'ASSUMPTION
      (MAKE
       ASSUMPTION :TYPE-ALIST TYPE-ALIST
       :TERM TERM :REWRITTENP REWRITTENP
       :IMMEDIATEP IMMEDIATEP :ASSUMNOTES
       (LIST
        (MAKE
             ASSUMNOTE :CL-ID
             NIL :RUNE RUNE :TARGET TARGET)))
      TTREE)

     New:
     (ADD-TO-TAG-TREE
          'ASSUMPTION
          (MAKE ASSUMPTION
                :TYPE-ALIST TYPE-ALIST
                :TERM TERM
                :REWRITTENP REWRITTENP
                :IMMEDIATEP IMMEDIATEP
                :ASSUMNOTES
                (LIST (MAKE ASSUMNOTE
                            :CL-ID NIL
                            :RUNE RUNE
                            :TARGET TARGET)))
          TTREE)

Basically the change we made forces the prettyprinter to print each :key
on a new line unless they all fit on a single line.  So we would now get
either

     (modify th s :key1 val1 :key2 :val2 :key3 val3)

or

     (modify th s
             :key1 val1
             :key2 val2
             :key3 val3)

Furthermore, we fixed it so that if val1 (say) is a big s-expression we
may still print it on the same line as its key.  The old prettyprinter
enforced the rule that if you wanted to print (foo a b) and b gets
broken up into several lines, then it has to start on a new line.  Thus,
we'd never print

     (foo a (bbb
             (mum x)))

but would print instead

     (foo a
          (bbb
           (mum x)))

Now, if a is a keyword, we can print the first way.

So here are some nice examples of prettyprinted keyword forms.  All of
these are printed for a page of width 40.

     <--            40 chars               ->
     xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

     (MODIFY TH S :KEY1 V1 :KEY2 V2)

     (MODIFY TH S :KEY1 V1 :KEY2 V2 :KEY3 V3)

     (MODIFY TH S1                               ; Because of the extra char
             :KEY1 V1                            ; in S1 the flat size exceeds
             :KEY2 V2                            ; 40 and we break it.
             :KEY3 V3)

The old ppr would have printed this as:

     (MODIFY
          TH S1 :KEY1 V1 :KEY2 V2 :KEY3 V3)

Returning to new examples:

     <--            40 chars               ->
     xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

     (MODIFY TH S
             :KEY1 (IF (IF X Y Z) AAAA BBBB)
             :KEY2 VAL2
             :KEY3 VAL3)

Now we extend AAAA and BBBB by one char each, so it would overflow the
right margin if printed as above, and we get:

     <--            40 chars               ->
     xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

     (MODIFY
          TH S
          :KEY1 (IF (IF X Y Z) AAAAX BBBBX)
          :KEY2 VAL2
          :KEY3 VAL3)

If we make these names even longer we force the value off the line
containing :key1:

     (MODIFY
          TH S
          :KEY1
          (IF (IF X Y Z) AAAAXXXXX BBBBXXXXX)
          :KEY2 VAL2
          :KEY3 VAL3)

Here are some examples from the ACL2 source code, printed in 40
characters:

     (DEFTHM
      ALPHORDER-ANTI-SYMMETRIC
      (IMPLIES (AND (NOT (CONSP X))
                    (NOT (CONSP Y))
                    (ALPHORDER X Y)
                    (ALPHORDER Y X))
               (EQUAL X Y))
      :HINTS
      (("Goal"
        :IN-THEORY
        (UNION-THEORIES
         '(STRING< SYMBOL-<)
         (DISABLE
            CODE-CHAR-CHAR-CODE-IS-IDENTITY))
        :USE
        ((:INSTANCE SYMBOL-EQUALITY (S1 X)
                    (S2 Y))
         (:INSTANCE BAD-ATOM<=-ANTISYMMETRIC)
         (:INSTANCE
              CODE-CHAR-CHAR-CODE-IS-IDENTITY
              (C Y))
         (:INSTANCE
              CODE-CHAR-CHAR-CODE-IS-IDENTITY
              (C X)))))
      :RULE-CLASSES
      ((:FORWARD-CHAINING
        :COROLLARY
        (IMPLIES
           (AND (ALPHORDER X Y)
                (NOT (CONSP X))
                (NOT (CONSP Y)))
           (IFF (ALPHORDER Y X) (EQUAL X Y)))
        :HINTS
        (("Goal"
          :IN-THEORY (DISABLE ALPHORDER))))))

Here is that same one, printed in a width of 60.

     (DEFTHM
      ALPHORDER-ANTI-SYMMETRIC
      (IMPLIES (AND (NOT (CONSP X))
                    (NOT (CONSP Y))
                    (ALPHORDER X Y)
                    (ALPHORDER Y X))
               (EQUAL X Y))
      :HINTS
      (("Goal"
          :IN-THEORY
          (UNION-THEORIES
               '(STRING< SYMBOL-<)
               (DISABLE CODE-CHAR-CHAR-CODE-IS-IDENTITY))
          :USE ((:INSTANCE SYMBOL-EQUALITY (S1 X)
                           (S2 Y))
                (:INSTANCE BAD-ATOM<=-ANTISYMMETRIC)
                (:INSTANCE CODE-CHAR-CHAR-CODE-IS-IDENTITY (C Y))
                (:INSTANCE CODE-CHAR-CHAR-CODE-IS-IDENTITY
                           (C X)))))
      :RULE-CLASSES
      ((:FORWARD-CHAINING
           :COROLLARY (IMPLIES (AND (ALPHORDER X Y)
                                    (NOT (CONSP X))
                                    (NOT (CONSP Y)))
                               (IFF (ALPHORDER Y X) (EQUAL X Y)))
           :HINTS (("Goal" :IN-THEORY (DISABLE ALPHORDER))))))

Just for comparison, here is the above printed in 60 columns by the old
prettyprinter.

     (DEFTHM
      ALPHORDER-ANTI-SYMMETRIC
      (IMPLIES (AND (NOT (CONSP X))
                    (NOT (CONSP Y))
                    (ALPHORDER X Y)
                    (ALPHORDER Y X))
               (EQUAL X Y))
      :HINTS
      (("Goal" :IN-THEORY
               (UNION-THEORIES
                    '(STRING< SYMBOL-<)
                    (DISABLE CODE-CHAR-CHAR-CODE-IS-IDENTITY))
               :USE
               ((:INSTANCE SYMBOL-EQUALITY (S1 X)
                           (S2 Y))
                (:INSTANCE BAD-ATOM<=-ANTISYMMETRIC)
                (:INSTANCE CODE-CHAR-CHAR-CODE-IS-IDENTITY (C Y))
                (:INSTANCE CODE-CHAR-CHAR-CODE-IS-IDENTITY
                           (C X)))))
      :RULE-CLASSES
      ((:FORWARD-CHAINING
            :COROLLARY
            (IMPLIES (AND (ALPHORDER X Y)
                          (NOT (CONSP X))
                          (NOT (CONSP Y)))
                     (IFF (ALPHORDER Y X) (EQUAL X Y)))
            :HINTS
            (("Goal" :IN-THEORY (DISABLE ALPHORDER))))))

Of course, given that you cannot tell for sure whether the keywords
you're seeing are part of a keyword/value parameter list or part of
some constant containing random keywords, the prettyprinter can't solve
the problem perfectly.  We just tried to make it work nicely on
well-formed keyword/value parameter lists.

For example, here is a form printed by the each prettyprinter.

     Old:
     (MEMBER
      X
      '(:MONDAY
           :MON :TUESDAY :TUES :WEDNESDAY
           :WED :THURSDAY :THURS :FRIDAY
           :FRI :SATURDAY :SAT :SUNDAY :SUN))

     New:
     (MEMBER X
             '(:MONDAY :MON
                       :TUESDAY :TUES
                       :WEDNESDAY :WED
                       :THURSDAY :THURS
                       :FRIDAY :FRI
                       :SATURDAY :SAT
                       :SUNDAY :SUN))

The new way is not how one would print it by hand!  But then, neither
is the old way.

NOTE-2-9-4    ACL2 Version  2.9.4 (February, 2006) Notes

Also see NOTE-2-9-1, see NOTE-2-9-2, and see
NOTE-2-9-3 for other changes since the last non-incremental release
(Version_2.9).

A soundness bug has been fixed that was due to inadequate checking of
:meta rules in the presence of local events.  Specifically, a local
defevaluator event is insufficient for supporting a :meta rule (an
example is shown in source function chk-acceptable-rules).  Thanks to
Dave Greve and Jared Davis for bringing this bug to our attention, by
sending a proof of nil that exploited this bug.  The fix is to check
legality of :meta rules even when skipping proofs during an
include-book event or the second pass of an encapsulate event.

Fixed problem with parallel make for workshop books by adding a
dependency line to books/workshops/2003/Makefile.

Default hints (see SET-DEFAULT-HINTS) no longer prevent the use
of :INSTRUCTIONS (see PROOF-CHECKER).  Thanks to Jared Davis
for pointing out this problem.

New functions remove-eq and remove-equal have been defined, in analogy
to remove.  These two symbols have also been added to *acl2-exports*.
Thanks to David Rager for pointing out that remove-equal was missing.
Moreover, the definitions of delete1-eq and delete1-equal have been
eliminated.  Function remove1-eq, now in :logic mode in source file
axioms.lisp, serves in place of delete1-eq, with corresponding new
function definitions for remove1 and remove1-equal.

The symbol assert$ has been added to *acl2-exports*.  Thanks to Jared
Davis for the suggestion.

Added SBCL support.  Thanks to Juho Snellman for significant assistance
with the port.  Thanks to Bob Boyer for suggesting the use of feature
:acl2-mv-as-values with SBCL, which can allow thread-level parallelism
in the underlying lisp; we have done so when feature :sb-thread is
present.

We have continued to incorporate suggestions for wording improvements in
documentation and error messages.  Thanks to all who send these
suggestions, especially to Eric Smith, who has suggested the vast
majority of them.

Made a small improvement to errors and warnings caused on behalf of
set-enforce-redundancy, to indicate when an event of the same name
already exists.

Fixed a bug in books/misc/rtl-untranslate.lisp that was causing a guard
violation when adding a new entry for an existing key.

Fixed a bug in translation to internal form that caused defun-sk and
defchoose to have difficulties handling ignored variables in let forms.
Thanks to Sandip Ray to bringing this issue to our attention with a
helpful example.

The form (push :acl2-mv-as-values *features*) has been added in source
file acl2-init.lisp for SBCL and OpenMCL only, in order to support
parallel execution (looking to the future...).

Default-hints (see SET-DEFAULT-HINTS) were being ignored inside
the proof-checker, but no longer.  Thanks to John Erickson for bringing
this problem to our attention and providing a simple example of it.

Modified the TAGS "make" target (specifically, function make-tags) so
that it is gracefully skipped if the etags program is not found.
Thanks to David Rager for pointing out this issue.

Sandip Ray has re-worked the supporting materials for his ACL2 Workshop
2003 talk (originally with John Matthews and Mark Tuttle), to run in a
few minutes.  The result is in
workshops/2003/ray-matthews-tuttle/support/ and is included in the full
ACL2 regression suite.  Thanks, Sandip.

Debian releases of ACL2 had created superfluous .cert.final files when
certifying books.  This has been fixed; thanks to Jared Davis for
noticing this problem.

Jared Davis has pointed out that "If you add a :backchain-limit-lst 0 to
a rewrite rule whose hypotheses are all forced, then ACL2 `really
assumes them' without trying to relieve them right there through
rewriting."  Relevant documentation has been added for
:backchain-limit-lst; see RULE-CLASSES.

A new version of the rtl library has been included in books/rtl/rel5/.
Thanks to David Russinoff for contributing hand proofs for the new
lemmas, and to Matt Kaufmann for carrying out their mechanization.

Fixed a bug in save-exec that was failing to set the initial cbd
according to the current directory when starting up ACL2.  Thanks to
Camm Maguire for bringing our attention to this problem.

Variables introduced during let* abstraction are now in the current
package.  Thanks to Jared Davis for suggesting such a change.  See
SET-LET*-ABSTRACTIONP.

It is now allowed for two definitions to be considered the same from the
standpoint of redundancy (see REDUNDANT-EVENTS) when one
specifies a :guard of t and the other has no explicit :guard (hence,
the guard is implicitly t).  Thanks to Jared Davis for bringing this
issue to our attention.

(For users of emacs/emacs-acl2.el) There have been a few enhancements to
distributed file emacs/emacs-acl2. el (skip this paragraph if you don't
use that file):

     o Control-t q continues to compare windows ignoring whitespace,
     but now,    a prefix argument can be given to control case is also
     ignored (ignore case if    positive, else use case).

     o Control-t Control-l has been defined to be similar to Control-t
     l,    except that proofs are skipped and output is suppressed.

     o Control-t u has been defined to print, to the shell buffer, a
     :ubt! form for the command containing the cursor.

     o Control-t Control-f buries the current buffer.

     o Meta-x new-shell now puts the new shell buffer in shell-mode
     (thanks to David Rager for noticing this issue).

Linear arithmetic has been modified so that we do not generate the
equality (equal term1 term2) from the pair of inequalities (<= term1
term2) and (<= term2 term1) in the case that we would have to force both
term1 and term2 to be acl2-numberps.  Thanks to Dave Greve for
providing a motivating example and to Robert Krug for providing a fix.

The event delete-include-book-dir had not been allowed inside books and
encapsulate forms.  This was an oversight, and has been fixed.

Sandip Ray has contributed a new library of books to support proofs of
partial and total correctness of sequential programs based on
assertional reasoning, in books/symbolic/.  This work is based on the
paper J. Matthews, J S. Moore, S. Ray, and D. Vroon, "A Symbolic
Simulation Approach to Assertional Program Verification," currently in
draft form.  In particular, the books include the macro defsimulate,
which automatically transforms inductive assertion proofs of
correctness of sequential programs to the corresponding interpreter
proofs.  See the README in that directory.

We have changed the implementation of :dir :system for ld and
include-book.  This change will not affect you if you build an ACL2
executable in the normal manner, leaving in place the books/
subdirectory of the source directory; nor will it affect you if you
download a GCL Debian binary distribution.  The change is that if
environment variable ACL2_SYSTEM_BOOKS is set, then it specifies the
distributed books directory, i.e., the directory determined by :dir
:system.  You may find it convenient to set this variable in your ACL2
script file (typically, saved_acl2).  If it is set when you build ACL2,
the generated script for running ACL2 will begin by setting
ACL2_SYSTEM_BOOKS to that value.  Thanks to various people who have
discussed this issue, in particular Jared Davis who sent an email
suggesting consideration of the use of an environment variable, and to
Eric Smith who helped construct this paragraph.  (Note that this use of
ACL2_SYSTEM_BOOKS replaces the use of ACL2_SRC_BOOKS described
previously; see NOTE-2-9-1.)

ACL2 now automatically deletes files TMP*.lisp created during the build
process and created by :comp.  If you want these to be saved, evaluate
(assign keep-tmp-files t) in the ACL2 loop or in raw Lisp.  The clean
target for the standard make process for certifying books (see
BOOK-MAKEFILES) will however delete all files TMP*.*.

The TMP files discussed just above now generally include the current
process ID in their names, e.g., TMP@16388@1.lisp instead of TMP1.lisp.
Thanks to Bob Boyer for suggesting this measure, which will reduce the
possibility that two different processes will attempt to access the same
temporary file.

Now, :pe will print the information formerly printed by :pe!, slightly
enhanced to work for logical names that are strings, not just symbols.
Thanks to Warren Hunt for leading us to this change by suggesting that
:pe nth print the definition of nth.

We eliminated spurious warnings that could occur in raw mode in OpenMCL
or CMUCL when stobjs are present.  We thank Juho Snellman for pointing
out the relevant bug and appropriate fix.

Mfc-rw now takes a third argument that can specify an arbitrary known
equivalence relation; see EXTENDED-METAFUNCTIONS.  Thanks to
Dave Greve for discussions suggesting this improvement.

A small modification to a symbol-reading function allows documentation
string processing on Windows systems that use CR/LF for line breaks.
Thanks to William Cook for bringing this issue to our attention.

The documentation has been improved on how to control the printing of
ACL2 terms.  See USER-DEFINED-FUNCTIONS-TABLE.  Thanks to
Sandip Ray for asking a question that led to the example presented
there.

We fixed an inefficiency that could cause an ld command to seem to hang
at its conclusion.  Thanks to Sandip Ray for pointing out this problem.

We checked that ACL2 runs under LispWorks 4.4.5 (last checked before
4.3), and have inhibited redefinition warnings.

Two changes have been made on behalf of congruence-based reasoning.
Thanks to Dave Greve for examples and discussions that have led to
these changes, and to Eric Smith and Vernon Austel, who also sent
relevant examples.

     o When a call of the new unary function double-rewrite is
     encountered by the rewriter, its argument will be rewritten twice.
     This solves certain problems encountered in congruence-based
     rewriting.  Warnings for :rewrite and :linear rules will suggest
     when calls of double-rewrite on variables in hypotheses are likely
     to be a good idea.  See DOUBLE-REWRITE.

     o Hypotheses of the form (equiv var (double-rewrite term)), where
     equiv is a known equivalence relation and var is a free variable
     (see FREE-VARIABLES), will bind var to the result of
     rewriting term twice.  Previously, hypotheses of the form (equal
     var term) would bind a free variable var, but the call had to be
     of equal rather than of an arbitrary known equivalence relation.

The following improvements were made in support of ACL2 on top of
OpenMCL.

     o New versions of OpenMCL that do not have :mcl in Lisp variable
     *features* will now work with ACL2.  Thanks to David Rager for
     bringing this issue to our attention.

     o Added support for OpenMCL 1.0 for 64-bit DarwinPPC/MacOS X,
     thanks to Robert Krug.

     o Fixed tracing in OpenMCL so that the level is reset to 1 even if
     there has been an abort.

     o Added support in OpenMCL for WET.

     o Incorporated suggestions from Gary Byers for printing the
     "Welcome to OpenMCL" prompt before initially entering the ACL2
     loop and, and for setting useful environment variable
     CCL_DEFAULT_DIRECTORY in the ACL2 script.

Fixed a long-standing bug in forward-chaining, where variable-free
hypotheses were being evaluated even if the executable-counterparts of
their function symbols had been disabled.  Thanks to Eric Smith for
bringing this bug to our attention by sending a simple example that
exhibited the problem.

Improved reporting by the break-rewrite utility upon failure to relieve
hypotheses in the presence of free variables, so that information is
shown about the attempting bindings.  See
FREE-VARIABLES-EXAMPLES-REWRITE.  Thanks to Eric Smith for requesting
this improvement.  Also improved the break-rewrite loop so that terms,
in particular from unifying substitutions, are printed without hiding
subterms by default.  The user can control such hiding
("evisceration"); see :DOC set-brr-term-evisc-tuple.

A new directory books/defexec/ contains books that illustrate the use of
mbe and defexec.  Thanks to the contributors of those books (see the
README file in that directory).

The directories books/rtl/rel2 and books/rtl/rel3 are no longer
distributed.  They are still available by email request.  (Subdirectory
rel1/ supports some of the optional workshop/ books, so it is still
distributed.)

Added book books/misc/sticky-disable.lisp to manage theories that might
otherwise be modified adversely by include-book.  Thanks to Ray
Richards for a query that led to our development of this tool.

The commands (exit) and (quit) may now be used to quit ACL2 and Lisp
completely; in fact they macroexpand to calls of the same function as
does good-bye (which is now a macro).  Thanks to Jared Davis for
suggesting the new aliases.  (OpenMCL-only comment:) These all work for
OpenMCL even inside the ACL2 loop.

The macro wet now hides structure by default on large expressions.
However, a new optional argument controls this behavior, for example
avoiding such hiding if that argument is nil.  Thanks to Hanbing Liu for
pointing out that wet was not helpful for very large terms.

We have fixed a bug in the forward-chaining mechanism that, very rarely,
could cause a proof to be aborted needlessly with an obscure error
message.  Thanks to Jared Davis for sending us an example that evoked
this bug.

Fixed a bug that was causing proof output on behalf of
:functional-instance to be confusing, because it failed to mention that
the number of constraints may be different from the number of subgoals
generated.  Thanks to Robert Krug for pointing out this confusing
output.  The fix also causes the reporting of rules used when silently
simplifying the constraints to create the subgoals.

Fixed a bug in handling of leading ./ in pathnames, as in:
(include-book "./foo").  Thanks to Jared Davis for bringing this bug to
our attention.

Made a small fix for handling of free variables of :forward-chaining
rules, which had erroneously acted as though a hypothesis (equal var
term) can bind the variable var.

A small change has been made for :type-prescription rules for
hypotheses of the form (equal var term), where c[var] is a free variable
and no variable of term is free (see FREE-VARIABLES).  As with
:rewrite and :linear rules, we now bind var to term even if (equal u
term) happens to be known in the current context for some term u.  Also
as with :rewrite and :linear rules, similar handling is given to
hypotheses (equiv var (double-rewrite term)) where equiv is a known
equivalence relation.

We changed the handling of free variables in hypotheses of :rewrite
rules being handled by the proof-checker's rewrite (r) command, in
complete analogy to the change described just above for
:type-prescription rules.

The installation instructions have been updated for obtaining GCL on a
Macintosh.  Thanks to Robert Krug for supplying this information and to
Camm Maguire for simplifying the process by eliminating the gettext
dependency.

The macro comp is now an event, so it may be placed in books.

Previously, a save-exec call could fail because of file permission
issues, yet ACL2 (and the underlying Lisp) would quit anyhow.  This has
been fixed.  Thanks to Peter Dillinger for bringing this problem to our
attention.

Jared Davis, with assistance from David Rager, has updated his ordered
sets library, books/finite-set-theory/osets/.  See file CHANGES.html in
that directory.

A new function, reset-kill-ring, has been provided for the rare user
who encounters memory limitations.  See RESET-KILL-RING.

NOTE-2-9-5    Changes in Version  3.0 since Version  2.9.4

Fixed a bug in cw-gstack that was causing a hard error when attempting
to report on a forced assumption.  Thanks to Jared Davis for pointing
this out and sending an example that helped us to determine a fix.

Added set-backchain-limit to the set of legal events that can be placed
in encapsulate forms and books.  Thanks to John Cowles for bringing
this issue to our attention.

Fixed a bug that broke wet.  Thanks to David Rager for bringing this
bug to our attention.

Guard verification now evaluates ground subexpressions (those with no
free variables) when computing the guard conjecture for the body of a
function.  Thanks to Jared Davis for useful conversations leading to
this change.  See VERIFY-GUARDS, in particular its "Note on
computation of guard conjectures and evaluation" near the end of that
topic, for more details.

Added a warning when a theory-invariant is redefined.  Thanks to Jared
Davis for suggesting a warning in this case and providing an informative
example.  Also, theory-invariants are now maintained more completely,
as they are checked at the end of every event except for events
executed on behalf of an include-book or the second pass of an
encapsulate.

Fixed the handling of runic designators to match their specification
(see THEORIES), so that disabling the name of a defthm event
disables all rules generated for that event.

(For those who do numerous builds using feature :acl2-mv-as-values,
currently only OpenMCL and multi-threaded SBCL by default:) You can
speed up builds by adding the following parameter to make, under
conditions described in GNUmakefile: USE_ACL2_PROCLAIMS=:REUSE.

Arranged that traced functions (see TRACE$) are automatically
untraced when events are undone (for example see UBT), at least
for most underlying Common Lisp implementations.

The macro defun-sk now creates non-executable functions, which allows
stobjs to be used where they had previously been prohibited.  More
generally, the user now has control over declare forms to be used by
the underlying defun'd function; see DEFUN-SK.  Thanks to
Sandip Ray for pointing out the need for such a modification.

:Definition rules are now treated, at least by default, as truly
first-class definitions.  In particular, :expand hints use the latest
:definition rule by default.  You may specify :install-body nil to get
the previous behavior of :definition rules; See DEFINITION, and
you may choose a previously-installed :definition rule to provide the
current body; see SET-BODY.  Also see RULE-CLASSES for
details of the :install-body field, and see HINTS to see a new
:with directive for controlling expansion.  The :with directive for
:expand hints can even direct the use of a :rewrite rule for expansion!
Thanks to various people, including Sandip Ray and Rob Sumners, for
discussions on the issue of the applicability of :definition rules for
:expand hints.

Constraints for functional instantiation now use the original definition
rather than a simplified ("normalized") version of it.

Fixed a bug that caused the prompt to stay the same when guard-checking
is off (see SET-GUARD-CHECKING) and raw-mode is changed (see
SET-RAW-MODE).

Lemma names in directory books/ordinals have been changed by replacing
/\ with & and replacing \/ with V.  We made this change because
backslash is an escape character and hence disappears unless it is
itself escaped.

Fixed proof-tree output so that failed non-proof events do not cause the
proof-tree to be re-printed.  Thus for example, if you have already
advanced the checkpoint marker, it will not be reset by subequent
failed non-proof events.  Thanks to Pete Manolios and Peter Dillinger
for bringing this bug to our attention.

Fixed a bug that was preventing the printing of stobj fields as
constants instead of numbers in certain cases.  (Note that this bug only
affected printing, not soundness.) Thanks to Eric Smith for bringing
this problem to our attention and providing the following example
(which now works fine).

     (defstobj st fld1 fld2)
     (in-theory (disable update-nth))
     (defund run (st)
       (declare (xargs :stobjs (st))) ;adding this didn't seem to help..
       st)

     ;works great; *fld1* prints as  *fld1*
     (thm (equal (update-nth *fld1* 'abc st)
                 (car (cons x y))))

     ;*fld1* gets printed as 0, presumably because the call to run intervenes.
     (thm (equal (update-nth *fld1* 'abc (run st))
                 (car (cons x y))))

The macro progn now allows the use of macros defined within its bodies
even when at the event level, as illustrated by the following example.

     (progn (defmacro my-defun (&rest args)
              `(defun ,@args))
            (my-defun g (x) x))

Thanks to Anna Slobodova for bringing this issue to our attention.  A
related change is that all arguments of progn must now be embedded
event forms (see EMBEDDED-EVENT-FORM), so use er-progn instead
if this is not the case.

The change to progn mentioned above also fixes a bug in handling local
events inside a progn that is inside an encapsulate or in a book.  For
example, the following form formerly caused an error.

     (encapsulate
      ()
      (defun foo (x) x)
      (progn (local (defun bar (x) x))
             (defun abc (x) x)))

We fixed two bugs in :puff and :puff*.  The first, brought to our
attention by Eric Smith (who we thank), caused a cryptic error message
when puffing a command with no subsidiary stored events; try, for
example, (encapsulate () (value-triple 3)).  The second was due to a
failure to restore the acl2-defaults-table.  Suppose for example that
we have certified the book foo.lisp, which contains (program) followed
by some definitions and/or theorems.  Now suppose we start ACL2 and
execute the following.

     (include-book "foo")
     (defthm test-thm
       (equal x x)
       :rule-classes nil)

If we now execute :puff 1, ACL2 will roll back the world to before the
include-book; then "puff" the include-book, which will leave us in
:program mode; and finally skip re-execution of the defthm because such
events are skipped in :program mode.  The fix is to re-install the
acl2-defaults-table immediately after the include-book to its
pre-include-book value.

A new event, make-event, provides something like macros that take
state.  For example, one can use it to put tests into certified books,
do proof search, and generate new function names.  Many examples appear
in directory books/make-event/.  See MAKE-EVENT.  Thanks to Bob
Boyer and Jared Davis for useful feedback and to Warren Hunt, David
Rager, and Sandip Ray for helpful discussions leading to some of the
examples in directory books/make-event/.

In support of make-event, which is described in the preceding
paragraph, certify-book has a new keyword argument, :save-expansion,
that controls whether the result of expanding make-event forms is
written out to a file.  See CERTIFY-BOOK; and for a discussion
of book expansion files, see MAKE-EVENT.

We fixed a soundness bug that did not correctly detect local events.
For example, the following event was admitted.

     (encapsulate
      ()
      (local
       (encapsulate
        ()
        (local (progn (program))) ; or, (local (with-output :off summary (program)))
        (set-irrelevant-formals-ok t)
        (defun foo (x)
          (declare (xargs :measure (acl2-count x)))
          (1+ (foo x)))))
      (defthm inconsistent
        nil
        :hints (("Goal" :use foo))
        :rule-classes nil))

A new value for guard checking, :none, is now allowed.  If you execute
:set-guard-checking :none, then no guard checking will take place (but
raw Lisp code will not be executed in this case).  As a result, you
should never see a guard violation, even for calls of :program mode
functions.  We thank Pete Manolios, who has long wanted this feature,
and also Peter Dillinger, for asking for it.  New documentation
explains the interaction between the defun-mode and the value supplied
to :set-guard-checking.  See GUARD-EVALUATION-TABLE, see
GUARD-EVALUATION-EXAMPLES-SCRIPT, and see
GUARD-EVALUATION-EXAMPLES-LOG.

In the course of adding the guard-checking value :none described in the
paragraph above, we eliminated an optimization that eliminated guard
checking for some recursive calls of :logic mode mutually-recursive
functions that have not had their guards verified.  But we doubt that
this change will be noticed by any users!)

The ACL2 hyper-card has been enhanced, thanks to David Rager, with a
listing of "Useful EMACS Commands" to match comments in
emacs/emacs-acl2.el.

Users contributed books following the Readme.lsp methodology:
data-structures/memories and unicode (Jared Davis), proofstyles (Sandip
Ray and J Moore).

Made some improvements to books/Makefile-generic (a file discussed
elsewhere; see BOOK-MAKEFILES).  In particular, improved
handling of .acl2 files for dependencies target.

(Only OpenMCL and, with feature :acl2-mv-as-values, GCL) Fixed a bug
that was causing proclaiming to fail when definitions are submitted
interactively.

The default stack size has been increased for several lisps.

(Very technical) A restriction has been weakened on the use of local
stobjs under a call of an ACL2 evaluator (trans-eval or
simple-translate-and-eval).  Now, the error can only take place for
stobj names that occur in the term being evaluated.  Thanks to Erik
Reeber for bringing this issue to our attention.

The notion of "ancestor" has been changed slightly.  This notion is
used by extended metafunctions and break-rewrite (see
EXTENDED-METAFUNCTIONS and see BRR@), and also with
backchain limits (see BACKCHAIN-LIMIT and see
SET-BACKCHAIN-LIMIT).  Basically, each time a hypothesis is
encountered during application of a rewrite rule, that hypothesis is
pushed (after instantiating and negating) onto the current list of
ancestors before it is rewritten.  However, hypotheses of the form
(equal var term), where var is free (see FREE-VARIABLES), had
not been included in the ancestors (similarly for (equiv var
(double-rewrite term)) where equiv is a known equivalence relation).
Now such "binding hypotheses" are included in a special way in
ancestors data structures.  In particular, (null (mfc-ancestors mfc))
will now be true if and only if the term being rewritten is part of the
current goal as opposed to a hypothesis from a rule encountered during
backchaining, even if that hypothesis is a binding hypothesis.  Thanks
to Dave Greve for bringing this issue to our attention.

Termination and induction analysis now continue through both arguments
of prog2$, not just the second.  (Normally, the gathering up of if
tests stops at function calls; but it continued through the second
argument of prog2$, and now it will continue through both arguments.)
Thanks to Sol Swords for discussion leading to this change.

The ACL2 distribution is now kept on the http server rather than the ftp
server (but the home page has not been moved).  Thanks to Robert Krug
for letting us know that some ACL2 users have found it inconvenient to
fetch ACL2 using ftp.

The file books/README.html has been renamed to books/Readme.html, since
some browsers don't show the former in the directory listing.

NOTE-3-0    ACL2 Version  3.0 (June, 2006) Notes

Please see NOTE-2-9-5 for a description of changes since
Version  2.9.4.  These include the new make-event feature, a soundness
bug fix, an improvement for :expand hints, evaluation in the logic by
way of :set-guard-checking :none, and many other improvements.

More generally, there have been several incremental releases since
Version  2.9: see NOTE-2-9-1, see NOTE-2-9-2, see
NOTE-2-9-3, see NOTE-2-9-4, and see NOTE-2-9-5.

A very few users have contributed books following the instructions on
the web.  We expect that when more contributions come in, we will give
more attention to the question of how to organize the distributed and
workshop books.  For now, we have simply added the new contributions
according to the old-style distribution methodology.

NOTE-3-0(R)    ACL2 Version  3.0(r) (June, 2006) Notes

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

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

NOTE-3-0-1    ACL2 Version  3.0.1 (August, 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 a soundness bug, introduced in the previous release, due to a
failure to disallow table events that set the acl2-defaults-table in a
local context.  Here is a proof of nil that exploits the bug.

     (encapsulate ()
      (local (program))
      (defun foo ()
        (declare (xargs :measure 17))
        (+ 1 (foo))))
     (thm
      nil
      :hints (("Goal" :in-theory (disable foo (foo)) :use foo)))

Fixed a bug in the alternatives to good-bye, which are the exit and
quit commands.  Thanks to Jared Davis and Peter Dillinger for pointing
this out right away.

The definition of len has been highly optimized in raw Lisp.  Thanks to
Bob Boyer and Warren Hunt for suggesting such an improvement and
providing a lot of help in coming up with the current implementation.

The clause subsumption algorithms have been improved, both to improve
efficiency during warnings for :rewrite rules and to punt when the
subsumption computation for induction appears to be blowing up.  Thanks
to Robert Krug for bringing this issue to our attention and supplying a
useful example.

A bug has been fixed that prevented time$ from working properly in
OpenMCL and multi-threaded SBCL (actually, in any ACL2 image where
feature :acl2-mv-as-values is present).  Thanks to Sol Swords for
bringing this problem to our attention.

A type-spec of the form (satisfies pred) carries the requirement that
pred be a unary function symbol in the current ACL2 world; otherwise,
it is illegal.  Thanks to Dave Greve for pointing out that Common Lisp
has this requirement.

Installed a fix provided by Gary Byers (for ACL2 source function
install-new-raw-prompt), for OpenMCL, that fixes an issue exposed in
some versions of OpenMCL when compiler optimization is off.

Fixed a bug in contributed book misc/untranslate-patterns.lisp that was
causing calls of add-untranslate-pattern to be rejected in books.
Thanks to Ray Richards for pointing out this bug and to Jared Davis for
assisting in the fix.

Fixed a bug in defstobj when keywords :initially and :resizable are
both supplied.  In this case, the definition of the resizing function
mistakenly failed to quote the :initially value, even though this value
is not to be evaluated.  One could even get an error in this case, as
in the following example supplied by Erik Reeber, whom we thank for
bringing this bug to our attention:

       (defstobj $test
         (test-x :type (array t (5)) :initially (0) :resizable t))

A new feature, with-prover-time-limit, allows the setting of time
limits during proofs.  This is *not* a general-purpose time-limit
utility, nor is it guaranteed to implement a strict bound; it only
attempts to limit time approximately during proofs.  Thanks to Pete
Manolios and Daron Vroon, who made the most recent request for such a
feature, and to Robert Krug for a helpful discussion.

(GCL only) Fixed a bug in the procedure for building a profiling image.
Thanks to Sol Swords for bringing this bug to our attention and to Eric
Smith for bringing a subsequent problem to our attention.

Handling of theories can now use significantly less time and space.  A
regression suite run took about 25% longer before this change than it
did after making this change (and also the ones in the next two
paragraphs).  Thanks to Vernon Austel for bringing this issue to our
attention and for supplying code, quite some time ago, that provided
detailed, useful implementation suggestions.  Also thanks to the folks
at Rockwell Collins, Inc. for pushing the limits of the existing
implementation, thus encouraging this improvement.

Fixed a performance bug in obtaining executable counterpart symbols.

We now avoid certain computations made on behalf of warnings, when such
warnings are disabled.

We have relaxed the checks made when including an uncertified book, to
match the checks made when including a certified book.  Thanks to Eric
Smith for suggesting this change.

Fixed a bug in :pso (see SET-SAVED-OUTPUT) that caused an error
when printing the time summary.

Made fixes to avoid potential hard Lisp errors caused by the use of
:program mode functions.  The fix was to use a "safe mode," already in
use to prevent such errors during macroexpansion; see
GUARDS-AND-EVALUATION.  However, such errors were possible during
evaluation of macro guards, for example as follows:

     (defun foo (x)
       (declare (xargs :mode :program))
       (car x))
     (defmacro mac (x)
       (declare (xargs :guard (foo 3)))
       x)
     (defun g (x)
       (mac x))

A similar issue existed for calls of defpkg, in-theory, table,
make-event, and value-triple, but has been fixed for all but in-theory
and make-event, where technical issues have caused us to defer this
change.

Fixed a bug in wet that caused problems in OpenMCL, and perhaps other
Lisp implementations, when the argument to wet calls, or depends on,
certain built-ins including prog2$, time$, mbe, and must-be-equal.
Thanks to David Rager for bringing this problem to our attention.

The file books/Makefile-generic has been improved so that when book
certification fails with make, the failure message contains the book
filename.

Documentation has been written to explain how to avoid an expensive
immediate rewrite of the result of applying a :rewrite or :meta rule.
See META.  Thanks to Robert Krug for supplying this trick, and
to Eric Smith and Dave Greve for useful discussions.

(OpenMCL only) OpenMCL-based ACL2 image names formerly had extension
".dppccl", which was correct only for some platforms (including 32-bit
Darwin PPC).  That has been fixed, thanks to a suggestion from Gary
Byers.

It is now legal to attach both a :use and a :cases hint at the same
goal.  Thanks to Eric Smith for (most recently) requesting this feature.

It is now permissible to include the same symbol more than once in the
imports list of a defpkg form (i.e., its second argument).  Also, the
evaluation of defpkg forms with long import lists now uses a reasonably
efficient sorting routine to check for two different symbols with the
same name (see also books/misc/sort-symbols.lisp).  If you currently
call a function like remove-duplicates-eql for your imports list, as
had been suggested by a defpkg error message, then you may experience
some speed-up by removing that call.  Thanks to Eric Smith for helping
to discover this issue through profiling.

Made miscellaneous efficiency improvements not listed above (for
example, following a suggestion of Eric Smith to avoid checking for
so-called "bad Lisp objects" during include-book, which saved almost 3%
in time on one large example).

Modified the notion of "untouchable" to separate the notion of
untouchable functions and macros from the notion of untouchable state
global variables.  See PUSH-UNTOUCHABLE.  Thanks to Bob Boyer
for sending an example, (put-global 'ld-evisc-tuple t state), that
suggested to us the need for more restrictive handling of untouchables.
In particular, many ld specials (see LD) are now untouchable.
You may be able to work around this restriction by calling ld; see for
example the change to books/misc/expander.lisp.  But please contact the
ACL2 implementors if this sort of workaround does not appear to be
sufficient for your purposes.

Fixed a bug in function set-standard-oi (see STANDARD-OI).

Fixed a bug in the use of ld-evisc-tuple.  The bad behavior was an
improper use of the print-level and print-length components of the tuple
(specifically, taking its caddr and cadddr instead of taking its cadr
and caddr).  Thanks to Bob Boyer for bringing this bug to our attention.

A new argument to the compile-flg argument of certify-book, :all,
causes creation of a file to be compiled in place of the given book,
where that file contains not only a copy of the book (with make-event
forms expanded) but also contains definitions of the so-called
"executable counterparts" of the functions defined in the book.  Then,
functions defined in the book will be run compiled when including the
book, even for functions whose guards have not been verified, or are in
:program mode and running in so-called "safe mode" (for example, during
expansion of macros).  The default behavior, value t of compile-flg, is
unchanged.  Moreover, a new :comp! argument of include-book now
compiles the executable counterparts when creating the book's compiled
file, and unlike :comp, always deletes the old compiled file first so
that one always gets a fresh compile.

Now, certify-book gives a "Guards" warning only for :logic mode
functions that are defined in the given book but have not had their
guards verified.  Previously, it also warned about such functions that
were defined in the certification world or in sub-books.

A new command, redo-flat, facilitates the debugging of failed
encapsulate and progn forms by evaluating preliminary forms in order to
leave one at the point of failure.  See REDO-FLAT.  Thanks to
Ray Richards and others for asking for such a utility, and to Sandip Ray
for useful discussions.

We have changed the automatic declaration of of function types (still
done in GCL and OpenMCL only, for now).  Our motivation was to avoid
the assumption that Common Lisp functions return one value when ACL2
says that they do; thanks to Bob Boyer for bringing this issue to our
attention with the example of defining (foo x y) to be (floor x y).
ACL2 was saying that foo returns a single value, but because floor
returns two values in raw Lisp, so does foo.  Other changes to
automatic declaration include comprehending defund, not just defun.

A new function, mod-expt, computes (mod (expt base exp) m), and does so
efficiently in some implementations (currently only in GCL 2.7.0, which
is not yet released).  Thanks to Warren Hunt for suggesting such an
addition.

New functions getenv$ and setenv$ have been made available for reading
and writing environment variables.  Thanks to Jun Sawada for requesting
these utilities.

The query utility :pl has been improved in several ways.  As before,
:meta rules are only printed if the argument is a symbol; but the
information printed for them is now more appropriate.  The following
are changes for the case that the argument is not a symbol, but rather,
a term.  (1) Rules are displayed that have equivalence relations other
than equal.  (2) All matching :definition rules are displayed, where
previously :definition rules were only shown if they were "simple"
rules (sometimes known as "abbreviations"); see SIMPLE.  (3)
The "Equiv" field is printed for terms, not just symbols.  (4) The
substitution is shown that, when applied to the left-hand side of the
rule, will yield the specified term.  Thanks to Eric Smith for
suggesting these changes.

The proof-checker command ;show-rewrites has been improved to match the
changes described above for :pl.  In particular, :definition rules that
are not "simple" are now displayed by the proof-checker's show-rewrites
(and sr) command, and the proof-checker's rewrite command has been
correspondingly modified to accept these :definition rules.

Fixed make targets copy-distribution, copy-workshops, and copy-nonstd
so that they should also work for non-developers.

Fixed a bug that was causing :pr to display syntaxp hypotheses oddly in
some cases, in particular (syntaxp (let ...)).  (The problem was in the
"untranslate" display of the internal form of syntaxp calls.)  Thanks
to Robert Krug for bringing this problem to our attention.  We also
removed the restriction on bind-free that its argument could not be a
variable, a constant, or (more interestingly) a lambda application
(i.e., a let or mv-let expression).

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
     (added after Version_3.3: now books/hacking/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.  Thanks to Sandip Ray for his
contribution.

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 :a! 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).)  [Note
added for Version_3.4: This state global has been changed to
'program-fns-with-raw-code.]  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.

NOTE-3-3    ACL2 Version  3.3 (November, 2007) Notes

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

Below we roughly organize the changes since Version  3.2.1 into new
features, bug fixes, prover algorithm enhancements, and miscellaneous.
Also see NOTE-3-2-1 for other changes since Version  3.2.

*NEW FEATURES*

A new "gag-mode" provides less verbose, more helpful feedback from the
theorem prover, in support of The Method (see THE-METHOD).  See
SET-GAG-MODE.  We recommend the use of gag-mode, which may
become the default in future ACL2 releases, and we welcome suggestions
for improvement.  We thank Robert Krug and Sandip Ray for helpful
feedback in the design of gag-mode.  Note that when proofs fail, then
even without gag-mode and even if proof output is inhibited, the
summary will contain a useful listing of so-called "key checkpoints"
(see SET-GAG-MODE).

Added support for a leading `~' in filenames.  Thanks to Bob Boyer for
suggesting this enhancement.  Note that since `~/' depends on the user,
it is disallowed in books to be certified (see CERTIFY-BOOK),
since otherwise an include-book form in a book, b, could have a
different meaning at certification time than at the time include-book
is later executed on book b.

Made a change to allow (time$ FORM) and (with-prover-time-limit TIME
FORM) when FORM includes make-event calls that change the ACL2 world.
Thanks to Jared Davis for requesting such support for time$.

Computed hints (see COMPUTED-HINTS) may now produce a so-called
"error triple", i.e., a result of the form (mv erp val state), where a
non-nil erp causes an error, and otherwise val is the value of the
hint.  It remains legal for a computed hint to return a single ordinary
value; indeed, the symbol form of a computed hint must still be a
function that returns an ordinary single value.

New hints provide additional control of the theorem prover, as follows.
See HINTS for more details, and see new distributed book
directory books/hints/ for examples, in particular file
basic-tests.lisp in that directory for simple examples.

     o The hint :OR (hints-1 ... hints-k) causes an attempt to prove the
     specified goal using each hints-i in turn, until the first of these
     succeeds.  If none succeeds, then the prover proceeds after
     heuristically choosing the "best" result, taking into account the
     goals pushed in each case for proof by induction.

     o A custom hint is a keyword that the user associates with a
     corresponding hint-generating function by invoking
     add-custom-keyword-hint.  Thus, a custom hint may be viewed as a
     convenient sort of computed hint.

     o A custom hint, :MERGE, is implemented in distributed book
     books/hints/merge.lisp.  It is useful for combining hints.

     o A sophisticated yet useful custom hint is the :CONSIDER hint
     implemented in distributed book books/hints/consider-hint.lisp.
     With this hint, you can for example give the equivalent of a :USE
     hint without the need to supply an instantiation.  Include that
     book in order to see documentation online with :doc consideration,
     and see the book books/hints/consider-hint-tests.lisp for examples.

A new hint, :reorder, allows the specification of which subgoals are to
be considered first.  Thanks to Sandip Ray for putting forward this
idea.

Enhanced set-saved-output by supporting a second argument of :same,
which avoids changing which output is inhibited.

Added macros thm? and not-thm? to distributed book
books/make-event/eval.lisp, so that it's easy to test within a certified
book that a proof attempt succeeds or that it fails.

Added printing function cw!, which is analogous to cw just as fmt! is
to fmt, i.e., printing so that the result can be read back in.  Thanks
to Jared Davis for suggesting this enhancement (after doing his own
implementation).

The ACL2 customization file can now be specified using environment
variable ACL2-CUSTOMIZATION.  See ACL2-CUSTOMIZATION.  Thanks
to Peter Dillinger for requesting this feature.

Added new emacs capabilities for proof trees (all documented in emacs):

     o New function start-proof-tree-noninteractive, for example
     (start-proof-tree-noninteractive "*shell*")

     o C-z o      Switch to another frame

     o C-z b      Switch to prooftree buffer

     o C-z B      Switch to prooftree buffer in "prooftree-frame" frame

Added Common Lisp function, search, as a macro in logic mode, with
limited support for keyword arguments.  Thanks to Warren Hunt for
requesting this addition.

Sandip Ray has contributed a book, books/make-event/defrefine.lisp, that
provides a collection of macros to aid in reasoning about ACL2
functions via refinement.

Wrote and incorporated new utility for listing all the theorems in an
included book.  See books/misc/book-thms.lisp.  Thanks to Jared Davis
for requesting this functionality.

The new distributed book misc/defp.lisp generalizes the defpun macro to
allow more general forms of tail recursion.

(Low-level printing improvement) A new function,
set-ppr-flat-right-margin, allows the right margin for certain kinds of
"flat" printing to exceed column 40.  Thanks to Jared Davis for pointing
out that state global variables 'fmt-hard-right-margin and
'fmt-soft-right-margin are not alone sufficient to extend the right
margin in all cases.

The event add-include-book-dir can now take a relative pathname as an
argument.  Formerly, it required an absolute pathname.

A new book, books/misc/defopener.lisp, provides a utility creating a
theorem that equates a term with its simplification.

ACL2 now provides limited support for the Common Lisp primitive FLET,
which supports local function bindings.  See FLET.  Thanks to
Warren Hunt for requesting this feature.

Added a definition of boole$, a close analogue of Common Lisp function
boole.  Thanks to Bob Boyer for providing an initial implementation.

*BUG FIXES*

Fixed defstobj to inhibit a potentially useless theory warning.

Fixed a bug in the application of certify-book to relative pathnames
for files in other than the current directory.  Thanks to Amr Helmy for
bringing this bug to our attention.

Fixed a bug in :pl and :pr for displaying rules of class :meta.  Thanks
to Jared Davis for finding this bug and providing a fix.

Formerly, set-default-backchain-limit was not a legal event form for
encapsulate forms and books.  This has been fixed.  Thanks to Robert
Krug and Sandip Ray for bringing this bug to our attention.

Fixed the handling of hints in proof-checker commands for the prover,
such as bash -- see PROOF-CHECKER-COMMANDS -- so that the user
can override the default settings of hints, in particular of :do-not
and :do-not-induct hints attached to "Goal".  This fix also applies to
the distributed book misc/bash.lisp, where Robert Krug noticed that he
got an error with :hints (("Goal" :do-not '(preprocess))); we thank
Robert for pointing out this problem.

Fixed a bug in handling of stobjs occurring in guards of functions whose
guards have been verified.  In such cases, a raw Lisp error was possible
when proving theorems about non-"live" stobjs.  We thank Daron Vroon
for sending us an example that highlighted this bug.  The following
(simpler) example causes such an error in previous versions of ACL2.

     (defstobj st fld)
     (defun foo (st)
       (declare (xargs :stobjs st :guard (fld st)))
       st)
     (thm (equal (foo '(3))
                 '(3)))

The dmr feature for dynamic monitoring of rewrites had a bug, where the
file used for communicating with emacs was the same for all users,
based on who built the ACL2 executable image.  This has been fixed.
Thanks to Robert Krug for bringing this bug to our attention.

Fixed a bug in some warnings, in particular the warning for including an
uncertified book, that was giving an incorrect warning summary string.

Inclusion of uncertified books erroneously re-used make-event
expansions that were stored in stale certificates.  This is no longer
the case.  Thanks to Jared Davis for bringing this bug to our attention.

Fixed a bug that was disallowing calls of with-output in events that
were executing before calling certify-book.

Modified the functionality of binop-table so other than binary function
symbols are properly supported (hence with no action based on
right-associated arguments).  See ADD-BINOP.

Fixed small proof-checker issues related to packages.  Emacs commands
ctrl-t d and ctrl-t ctrl-d now work properly with colon (`:') and
certain other punctuation characters.  The p-top command now prints
"***" regardless of the current package.

Fixed a bug that allowed certify-book to succeed without specifying
value t for keyword argument :skip-proofs-okp, even with include-book
events in the certification world depending on events executed under
skip-proofs.

Improved show-accumulated-persistence in the following two ways.
Thanks to Robert Krug and Bill Young for requesting these improvements
and for providing useful feedback.

     o It can provide more complete information when aborting a proof.

     o The :frames reported for a rule are categorized as "useful" and
     "useless" according to whether they support "useful" or "useless"
     :tries of that rule, respectively.  See
     ACCUMULATED-PERSISTENCE for further explanation.

Modified make-event so that the reported time and warnings include
those from the expansion phase.  In analogy with encapsulate and progn,
the rules reported still do not include those from subsidiary events
(including the expansion phase).  A related change to ld avoids
resetting summary information (time, warnings) with each top-level form
evaluation; events already handle this information themselves.

Fixed set-inhibit-output-lst so that all warnings are inhibited when
warning! but not warning is included in the list.  Formerly, only
soundness-related warnings were inhibited in this case.  Thanks to Eric
Smith for bringing this bug to our attention.

Distributed directory doc/HTML/ now again includes installation
instructions (which was missing in Version_3.2.1), in
doc/HTML/installation/installation.html.

Some fixes have been made for proof-tree support.

     o Proof-tree output is no longer inhibited automatically during
     certify-book, though it continues to be inhibited by default (i.e.,
     ACL2 continues to start up as though set-inhibit-output-lst has
     been called with argument '(proof-tree)).

     o Fixed a bug in Xemacs support for proof-tree help keys C-z h and
     C-z ?.

     o Fixed a bug in proof-trees that was failing to deal with the
     case that a goal pushed for proof by induction is subsumed by such
     a goal to be proved later.  Now, the proof-tree display regards
     such subsumed goals as proved, as is reported in the theorem
     prover's output.

Fixed a bug that was disallowing value-triple forms inside encapsulate
forms in a certification world (see PORTCULLIS).

If the :load-compiled-file argument of a call of include-book is :comp,
then an existing compiled file will be loaded, provided it is more
recent than the corresponding book (i.e., .lisp file).  A bug was
causing the compiled file to be deleted and then reconstructed in the
case of :comp, where this behavior was intended only for :comp!.

Fixed a bug that was avoiding compilation of some executable
counterparts (sometimes called "*1* functions") during certify-book,
and also during include-book with :load-compiled-file value of :comp or
:comp!).  Thanks to Eric Smith for sending a small example to bring this
bug to our attention.

Incorporated a fix from Eric Smith for a typo (source function
ancestors-check1) that could cause hard Lisp errors.  Thanks, Eric!

Fixed the following issues with packages and book certificates.  See
HIDDEN-DEATH-PACKAGE if you are generally interested in such
issues, and for associated examples, see comments on "Fixed the
following issues with packages" in note-3-3 in the ACL2 source code.

     o Reduced the size of .cert files by eliminating some unnecessary
     defpkg events generated for the portcullis.

     o Fixed a bug that has caused errors when reading symbols from a
     portcullis that are in undefined packages defined in locally
     included books.

     o Fixed a bug that could lead to failure of include-book caused by
     a subtle interaction between set-ignore-ok and defpkg events
     generated for the portcullis of a certificate.

*PROVER ALGORITHM ENHANCEMENTS*

Non-linear arithmetic (see NON-LINEAR-ARITHMETIC) has been
improved to be more efficient or more powerful in some cases.  Thanks
to Robert Krug for contributing these improvements.

Improved certain (so-called "type-set") reasoning about whether or not
expressions denote integers.  Thanks to Robert Krug for contributing
code to implement this change, along with examples illustrating its
power that are now distributed in the book
books/misc/integer-type-set-test.lisp.

Improved ACL2's heuristics for relieving hypotheses, primarily to use
linear reasoning on conjuncts and disjuncts of the test of an if
expression.  For example, given a hypothesis of the form (if (or term1
term2) ...), ACL2 will now use linear reasoning to attempt to prove
both term1 and term2, not merely for term2.  Thanks to Robert Krug for
supplying examples illustrating the desirability of such an improvement
and for useful discussions about the fix.

Made a slight heuristic change, so that when a hypothesis with let or
mv-let subterms (i.e. lambda subterms) rewrites to t, then that
hypothesis is necessarily eliminated.  Thanks to Jared Davis for sending
an example that led us to develop this change, and thanks to Robert
Krug for a helpful discussion.

*MISCELLANEOUS*

Added documentation on how to use make-event to avoid duplicating
expensive computations, thanks to Jared Davis.  See
USING-TABLES-EFFICIENTLY.

Modified the error message for calls of undefined functions to show the
arguments.  Thanks to Bob Boyer for requesting this enhancement.

Modified utilies :pr, :pr!, :pl, and :show-bodies to incorporate code
contributed by Jared Davis.  That code defines low-level source
functions info-for-xxx that collect information about rules, which is
thus available to advanced users.

Dynamic monitoring of rewrites (see DMR) has been improved in
the following ways, as suggested by Robert Krug.

     o Some stale entries from the rewrite stack are no longer printed,
     in particular above ADD-POLYNOMIAL-INEQUALITIES.

     o An additional rewrite stack entry is made when entering
     non-linear arithmetic (see NON-LINEAR-ARITHMETIC).

     o An ADD-POLYNOMIAL-INEQUALITIES entry is printed with a counter,
     to show how often this process is called.

Modified save-exec so that the newly-saved image will have the same raw
Lisp package as the existing saved image.  This is a very technical
change that will likely not impact most users; for example, the package
in the ACL2 read-eval-print loop (see LP) had already persisted
from the original to newly-saved image.  Thanks to Jared Davis for
suggesting this change.

Changed make-event expansion so that changes to set-saved-output,
set-print-clause-ids, set-fmt-soft-right-margin, and
set-fmt-hard-right-margin will persist after being evaluated during
make-event expansion.  (Specifically, *protected-system-state-globals*
has been modified; see MAKE-EVENT-DETAILS.)  Thanks to Jared
Davis for bringing this issue to our attention.

Output from the proof-checker is now always enabled when invoking
verify, even if it is globally inhibited (see
SET-INHIBIT-OUTPUT-LST).

Improved the message printed when an :induct hint fails, to give more
information in some cases.  Thanks to Rex Page for suggesting where an
improvement could be made and providing useful feedback on an initial
improvement.

Added a warning for congruence rules (see DEFCONG) that specify
iff as the second equivalence relation when equal can be used instead.
Those who heed these warnings can eliminate certain subsequent
double-rewrite warnings for rewrite rules with conclusions of the form
(iff term1 term2), and hence implicitly for Boolean conclusions term1
that are interpreted as (iff term1 t).  Thanks to Sarah Weissman for
sending us an example that highlighted the need for such a warning.

Modified macro :redef! (which is for system implementors) so that it
eliminates untouchables.

Several improvements have been made to the experimental hons/memoization
version of ACL2.  See HONS-AND-MEMOIZATION.

The distributed books directory, (@ distributed-books-dir), is now
printed in the start-up message.

NOTE-3-3(R)    ACL2 Version  3.3(r) (November, 2007) Notes

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

NOTE-3-4    ACL2 Version  3.4 (August, 2008) Notes

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

Below we roughly organize the changes since Version  3.3 into changes to
existing features, new features, bug fixes, new and updated books, and
Emacs support.  Each change is described just once, though of course
many changes could be placed in more than one category.

*CHANGES TO EXISTING FEATURES*

Fixed a long-standing potential infinite loop in the rewriter.  Thanks
to Sol Swords for sending a concise example illustrating the looping
behavior.  (Those interested in details are welcome to look at the
comment about loop behavior in source function rewrite-equal.)

Incorporated a slight strengthening of non-linear arithmetic
contributed by Robert Krug (thanks, Robert).  With non-linear
arithmetic enabled, the problem was essentially that ACL2 made the
following "optimization": given inequalities (< a u) and (< b v), for
positive rational constants a and b terms u and v of which at least one
is known to be rational, infer (< (* a b) (* u v)).  Without this
optimization, however, ACL2 now infers the stronger inequality obtained
by direct multiplication of the two given inequalities.  To see the
effect of this change, submit the event (set-non-linearp t) followed by:

     (thm (implies (and (rationalp x) (< 3 x)
                        (rationalp y) (< 4 y))
                   (< 0 (+ 12 (* -4 x) (* -3 y) (* x y)))))

The utility set-checkpoint-summary-limit has been modified in several
ways: it now takes a single argument (no longer takes state as an
argument); a natural number n abbreviates the pair (n . n); the
argument is no longer evaluated, but it still optionally may be quoted;
and a new value, t, suppresses all printing of the checkpoint summary.
Thanks to Jared Davis for suggesting most of these improvements.

There was formerly a restriction on mbe that the :exec argument may not
contain a call of mbe.  This restriction has been removed, thanks to a
request from Jared Davis and Sol Swords.  Thanks also to Sandip Ray, who
pointed out that this restriction may have been in place in order that
defexec can guarantee termination using the :exec code; its
documentation has therefore been updated to clarify this situation.

Rules of class :rewrite are now stored by performing certain logical
simplifications on the left side of the conclusion: (prog2$ X Y) is
replaced by Y, (mbe :logic X :exec Y) is replaced by X (more precisely,
the analogous change is made to the generated call of must-be-equal);
and (the TYPE X) is replaced by X (again, the change is actually made
on the macroexpanded form).  Thanks to Jared Davis and Sol Swords for
requesting this change.  An analogous change has also been made for
rules of class :forward-chaining.

The trace$ utility has been reimplemented to work independently of the
underlying Lisp trace.  It thus works the same for every host Lisp,
except as provided by an interface to the underlying host Lisp trace
(the :native option).  Note that the host Lisp trace continues to be
modified for GCL, Allegro CL, and CCL (OpenMCL); see TRACE.
See TRACE$ for updated detailed documentation on tracing
options, many of which are new, for example an :evisc-tuple option that
can be set to :no-print if you want the function traced without the
usual entry and exit printing.  The previous trace$ had some issues,
including the following, which have all been fixed.  Thanks to Peter
Dillinger for assistance in determining desired functionality of the
new trace$ and for helping to test it.

     Recursive calls were not always shown in the trace for two reasons.
     (1) Compiler inlining could prevent recursive calls from being
     shown in the trace, in particular in CCL (OpenMCL).  Thanks to
     Jared Davis and Warren Hunt for pointing out this issue and
     requesting a fix, and to Bob Boyer and Gary Byers for relevant
     helpful discussions.  (2) ACL2's algorithm for producing
     executable counterparts prevented tracing of recursive calls even
     after (set-guard-checking :none).  Thanks to Peter Dillinger for
     requesting a fix.

     It was possible to exploit a bug in the interaction of multiple
     values and trace to prove a contradiction.  An example is in a
     comment in (deflabel note-3-4 ...) in the ACL2 source code.

     Certain large structures could cause expensive computations for
     printing even when a :cond condition was specified and evaluated
     to nil.

     Trace! now suppresses printing of the event summary, and returns
     the value that would be returned (if there is an active trust tag)
     by the corresponding call of trace$.

     Some bugs have been fixed in the underlying native trace installed
     by ACL2 for GCL, Allegro CL, and CCL (OpenMCL), including the
     following.  In GCL it had been impossible to use the variable
     ARGLIST in a :cond expression.  In Allegro CL and CCL, a trace$
     bug mishandled tracing non-ACL2 functions when directives such as
     :entry and :exit were supplied.  GCL trace now hides the world
     even when tracing non-ACL2 functions.  Tracing in CCL no longer
     causes a Lisp error when untracing a traced function defined
     outside the ACL2 loop; for example (trace$ len1) followed by
     (untrace$ len1) no longer causes an error.

The macro wet has been changed, for the better we think.  see
WET.

The generation of goals for forcing-rounds has been changed to avoid
dropping assumptions formerly deemed "irrelevant".  (A simple example
may be found in a comment in source function unencumber-assumption,
source file prove.lisp.)  Thanks to Jared Davis for sending us an
example that led us to make this change.

Modified the implementation of make-event so that in the certificate of
a book, local events arising from make-event forms are elided.  For
example, if (make-event <form>) expands to (local <expanded-form>),
then where the latter had been stored in the certificate, now instead
(local (value-triple :ELIDED)) will be stored.  Thanks to Eric Smith
for requesting this improvement.  He has reported that a preliminary
version of this improvement shrunk a couple of his .cert files from
perhaps 40MB each to about 140K each.

Now, a table event that sets the entire table, (table tbl nil alist
:clear), is redundant (see REDUNDANT-EVENTS) when the supplied
alist is equal to the current value of the table.  Thanks to Peter
Dillinger for requesting this change.

The event constructor progn! now returns the value that is returned by
evaluation of its final form if no error occurs, except that it still
returns nil if the that final evaluation leaves ACL2 in raw-mode.

:Pso and :psog have been improved so that they show the key checkpoint
summary at the end of a failed proof.  (For a discussion of key
checkpoints, see SET-GAG-MODE.)  As a result, a call of
set-checkpoint-summary-limit now affects subsequent evaluation of :pso
and :psog.  In particular, you no longer need to reconstruct a proof
(by calling thm or defthm) in order to see key checkpoints that were
omitted due to the limit; just call set-checkpoint-summary-limit and
then run :pso or :psog.

The proof-checker behaves a little differently under gag-mode.  Now,
proof-checker commands that call the theorem prover to create new
proof-checker goals, such as bash and induct (see
PROOF-CHECKER-COMMANDS), will show key checkpoints when in gag-mode.
As before, proof-checker commands pso and pso! (and now, also psog) --
see PSO, see PSOG, and see PSO! -- can then
show the unedited proof log.  However, unlike proof attempts done in
the ACL2 loop, such proof attempts will not show a summary of key
checkpoints at the end, because from a prover perspective, all such
goals were considered to be temporarily "proved" by giving them "byes",
to be dispatched by later proof-checker commands.

A little-known feature had been that a measure of 0 was treated as
though no measure was given.  This has been changed so that now, a
measure of nil is treated as though no measure was given.

Expanded *acl2-exports* to include every documented symbol whose name
starts with "SET-".  Thanks to Jared Davis for remarking that
set-debugger-enable was omitted from *acl2-exports*, which led to this
change.

The trace mechanism has been improved so that the :native and
:multiplicity options can be used together for Lisps that support the
trace :exit keyword.  These Lisps include GCL and Allegro CL, whose
native trace utilities have been modified for ACL2.  For SBCL and CCL
(OpenMCL), which use the built-in Lisp mechanism for returning multiple
values in ACL2 (see MV), the use of :multiplicity with :native
remains unnecessary and will be ignored.  In support of this change, the
modification of native Allegro CL tracing for ACL2 was fixed to handle
:exit forms correctly that involve mv.

*NEW FEATURES*

The command :redef! is just like :redef, but prints a warning rather
than doing a query.  The old version of :redef! was for system hackers
and has been renamed to :redef+.

Introduced a new utility for evaluating a function call using the
so-called executable counterpart -- that is, executing the call in the
logic rather than in raw Lisp.  See EC-CALL.  Thanks to Sol
Swords for requesting this utility and participating in its high-level
design.

See PRINT-GV for a new utility that assists with debugging guard
violations. Thanks to Jared Davis for requesting more tool assistance
for debugging guard violations.

Improved the guard violation error message to show the positions of the
formals, following to a suggestion of Peter Dillinger.

Added new guard-debug capability to assist in debugging failed attempts
at guard verification.  See GUARD-DEBUG.  Thanks to Jared Davis
for requesting a tool to assist in such debugging and to him, Robert
Krug, and Sandip Ray for useful discussions.

New utilities provide the formula to be proved by verify-guards.  See
VERIFY-GUARDS-FORMULA and see GUARD-OBLIGATION, Thanks
to Mark Reitblatt for making a request leading to these utilities.
These utilities can be applied to a term, not just an event name;
thanks to Peter Dillinger for correspondence that led to this extension.

A new utility causes runes to be printed as lists in proof output from
simplification, as is done already in proof summaries.  See
SET-RAW-PROOF-FORMAT.  Thanks to Jared Davis for requesting this
utility.

An experimental capability allows for parallel evaluation.  See
PARALLELISM.  Thanks to David Rager for providing an initial
implementation of this capability.

Defined xor in analogy to iff.  Thanks to Bob Boyer, Warren Hunt, and
Sol Swords for providing this definition.

Improved distributed file doc/write-acl2-html.lisp so that it can now be
used to build HTML documentation files for documentation strings in user
books.  See the comment in the definition of macro
acl2::write-html-file at the end of that file.  Thanks to Dave Greve and
John Powell for requesting this improvement.

It is now possible to specify :hints for non-recursive function
definitions (which can be useful when definitions are automatically
generated).  See SET-BOGUS-DEFUN-HINTS-OK.  Thanks to Sol
Swords for requesting such a capability.

Keyword argument :dir is now supported for rebuild just as it has been
for ld.

We relaxed the criteria for functional substitutions, so that a function
symbol can be bound to a macro symbol that corresponds to a function
symbol in the sense of macro-aliases-table.  So for example, a
functional substitution can now contain the doublet (f +), where
previously it would have been required instead to contain (f binary-+).

We now allow arbitrary packages in raw mode (see SET-RAW-MODE)
-- thanks to Jared Davis for requesting this enhancement -- and more
than that, we allow arbitrary Common Lisp in raw mode.  Note however
that for arbitrary packages, you need to be in raw mode when the input
is read, not just when the input form is evaluated.

Two new keywords are supported by the with-output macro.  A :gag-mode
keyword argument suppresses some prover output as is done by
set-gag-mode.  Thanks to Jared Davis for asking for a convenient way to
set gag-mode inside a book, in particular perhaps for a single theorem;
this keyword provides that capability.  A :stack keyword allows
sub-events of progn or encapsulate to "pop" the effect of a superior
with-output call.  Thanks to Peter Dillinger for requesting such a
feature.  See WITH-OUTPUT.

The command good-bye and its aliases exit and quit now all take an
optional status argument, which provides the Unix exit status for the
underlying process.  Thanks to Florian Haftmann for sending a query to
the ACL2 email list that led to this enhancement.

Keyword commands now work for macros whose argument lists have lambda
list keywords.  For a macro with a lambda list keyword in its argument
list, the corresponding keyword command reads only the minimum number
of required arguments.  See KEYWORD-COMMANDS.

It is now legal to declare variables ignorable in let* forms, as in
(let* ((x (+ a b)) ...) (declare (ignorable x)) ...).  Thanks to Jared
Davis for requesting this enhancement.

Added a warning when more than one hint is supplied explicitly for the
same goal.  It continues to be the case that only the first hint
applicable to a given goal will be applied, as specified in the
user-supplied list of :hints followed by the default-hints-table.
Thanks to Mark Reitblatt for sending a question that led both to adding
this clarification to the documentation and to adding this warning.

You may now use set-non-linear, set-let*-abstraction, set-tainted-ok,
and set-ld-skip-proofs in place of their versions ending in "p".
Thanks to Jared Davis for suggesting consideration of such a change.
All "set-" utilites now have a version without the final "p" (and most
do not have a version with the final "p").

Added a "Loop-Stopper" warning when a :rewrite rule is specified with a
:loop-stopper field that contains illegal entries that will be ignored.
Thanks to Jared Davis for recommending such a warning.

Added a substantial documentation topic that provides a beginner's
guide to the use of quantification with defun-sk in ACL2.  Thanks to
Sandip Ray for contributing this guide, to which we have made only very
small modifications.  See QUANTIFIER-TUTORIAL.

Defun-sk now allows the keyword option :strengthen t, which will
generate the extra constraint that that is generated for the
corresponding defchoose event; see DEFCHOOSE.  Thanks to Dave
Greve for suggesting this feature.

*BUG FIXES*

Fixed a soundness bug related to the use of mbe inside encapsulate
events.  An example proof of nil (before the fix) is in a comment in
(deflabel note-3-4 ...) in the ACL2 source code.  We therefore no
longer allow calls of mbe inside encapsulate events that have non-empty
signatures.

Fixed a bug related to the definition of a function supporting the
macro value-triple.  Although this bug was very unlikely to affect any
user, it could be carefully exploited to make ACL2 unsound:

     (defthm fact
       (equal (caadr (caddr (value-triple-fn '(foo 3) nil nil)))
              'value) ; but it's state-global-let* in the logic
       :rule-classes nil)
     (defthm contradiction
       nil
       :hints (("Goal" :use fact :in-theory (disable (value-triple-fn))))
       :rule-classes nil)

Non-LOCAL definitions of functions or macros are no longer considered
redundant with built-ins when the built-ins have special raw Lisp code,
because ACL2 was unsound without this restriction!  A comment about
redundant definitions in source function chk-acceptable-defuns shows
how one could prove nil without this new restriction.  Note that system
utility :redef+ removes this restriction.

Although ACL2 already prohibited the use of certain built-in :program
mode functions for verify-termination and during macroexpansion, we
have computed a much more complete list of functions that need such
restrictions, the value of constant
*primitive-program-fns-with-raw-code*.

Modified what is printed when a proof fails, to indicate more clearly
which event failed.

Fixed a problem with dmr in CCL (OpenMCL) that was causing a raw Lisp
break after an interrupt in some cases.  Thanks to Gary Byers for a
suggestion leading to this fix.

Fixed bugs in proof-checker code for dealing with free variables in
hypotheses.

Upon an abort, the printing of pstack and gag-mode summary information
for other than GCL was avoided when inside a call of ld.  This has been
fixed.

(Windows only) Fixed bugs for ACL2 built on SBCL on Windows, including
one that prevented include-book parameters :dir :system from working,
and one that prevented certain compilation.  Thanks to Peter Dillinger
for bringing these to our attention and supplying a fix for the second.
Thanks also to Andrew Gacek for bringing include-book issues to our
attention.  Also, fixed writing of file saved_acl2 at build time so
that for Windows, Unix-style pathnames are used.

Fixed a hard Lisp error that could occur with keywords as table names,
e.g., (table :a :a nil :put).  Thanks to Dave Greve for bringing this
problem to our attention and providing this example.

Fixed handling of :OR hints so that proof attempts under an :OR hint do
not abort (reverting to induction on the original input conjecture)
prematurely.  Thanks to Robert Krug for pointing out this problem and
pointing to a possible initial fix.

(SBCL and CLISP only) It is now possible to read symbols in the
"COMMON-LISP" package inside the ACL2 command loop (see LP).
This could cause a raw Lisp error in previous versions of ACL2 whose
host Common Lisp was SBCL or CLISP.  Thanks to Peter Dillinger for
bringing this issue to our attention.

Fixed a bug that was preventing certain hints, such as :do-not hints,
from being used after the application of an :or hint.  Thanks to Robert
Krug for bringing this bug to our attention.

(Hons version only) Fixed a bug in the interaction of memoize (hons
version only) with event processing, specifically in interaction with
failures inside a call of progn or encapsulate.  Thanks to Jared Davis
for bringing this bug to our attention and sending an example.  A
simplified example may be found in a comment in source function
table-cltl-cmd, source file history-management.lisp; search for
"Version_3.3" there.

Fixed cw-gstack so that its :evisc-tuple is applied to the top clause,
instead of using (4 5 nil nil) in all cases.  If no :evisc-tuple is
supplied then (term-evisc-tuple t state) is used for the top clause, as
it is already used for the rest of the stack.

Fixed a bug in the interaction of proof-trees with :induct hint value
:otf-flg-override.  Thanks to Peter Dillinger for reporting this bug
and sending an example that evokes it.

Fixed bugs in :pr and find-rules-of-rune for the case of rule class
:elim.  Thanks to Robert Krug and Jared Davis for bringing these
related bugs to our attention.

Improved failure messages so that the key checkpoints are printed only
once when there is a proof failure.  Formerly, a proof failure would
cause the key checkpoints to be printed for every encapsulate or
certify-book superior to the proof attempt.

Fixed a bug in generation of guards for calls of pkg-witness.  Thanks
to Mark Reitblatt for sending an example showing this bug.  The bug can
be in play when you see the message:  "HARD ACL2 ERROR in
MAKE-LAMBDA-APPLICATION: Unexpected unbound vars ("")".  A distillation
of Mark's example that causes this hard error is as follows.

     (defun foo (x)
       (declare (xargs :guard t))
       (let ((y x)) (pkg-witness y)))

The cond macro now accepts test/value pairs of the form (T val) in
other than the last position, such as the first such pair in (cond (t
1) (nil 2) (t 3)).  Thanks to Jared Davis for sending this example and
pointing out that ACL2 was sometimes printing goals that have such a
form, and hence cannot be submitted back to ACL2.  A few macros
corresponding to cond in some books under books/rtl and books/bdd were
similarly modified.  (A second change will probably not be noticeable,
because it doesn't affect the final result: singleton cond clauses now
generate a call of or in a single step of macroexpansion, not of if.
For example, (cond (a) (b x) (t y)) now expands to (OR A (IF B X Y))
instead of (IF A A (IF B X Y)).  See the source code for cond-macro for
a comment about this change.)

Fixed a bug in the interaction of proof-checker command DV, including
numeric ("diving") commands, with the add-binop event.  Specifically,
if you executed (add-binop mac fn) with fn having arity other than 2, a
proof-checker command such as 3 or (dv 3) at a call of mac could have
the wrong effect.  We also fixed a bug in diving with DV into certain
AND and OR calls.  Thanks for Mark Reitblatt for bringing these
problems to our attention with helpful examples.

Fixed a couple of bugs that were causing an error, "HARD ACL2 ERROR in
RENEW-NAME/OVERWRITE".  Thanks to Sol Swords for bringing the first of
these bugs to our attention.

Fixed a bug that could cause certify-book to fail in certain cases
where there are local make-event forms.

Fixed a bug in start-proof-tree that could cause Lisp to hang or
produce an error.  Thanks to Carl Eastlund for sending an example to
bring this bug to our attention.

Fixed a bug in the proof output, which was failing to report cases
where the current goal simplifies to itself or to a set including itself
(see SPECIOUS-SIMPLIFICATION).

Fixed a bug in with-prover-time-limit that was causing a raw Lisp error
for a bad first argument.  Thanks to Peter Dillinger for pointing out
this bug.

The following was claimed in :doc note-3-3, but was not fixed until the
present release:
Distributed directory doc/HTML/ now again includes installation
instructions, in doc/HTML/installation/installation.html.

In certain Common Lisp implementations -- CCL (OpenMCL) and LispWorks,
at least -- an interrupt could leave you in a break such that quitting
the break would not show the usual summary of key checkpoints.  This
has been fixed.

*NEW AND UPDATED BOOKS*

Updated books/clause-processors/SULFA/ with a new version from Erik
Reeber; thanks, Erik.

Added new books directory tools/ from Sol Swords.  See
books/tools/Readme.lsp for a summary of what these books provide.

The distributed book books/misc/file-io.lisp includes a new utility,
write-list!, which is like write-list except that it calls
open-output-channel! instead of open-output-channel.  Thanks to Sandip
Ray for requesting this utility and assisting with its implementation.

Added record-update macro supplied by Sandip Ray to distributed book
books/misc/records.lisp.

Sandip Ray has contributed books that prove soundness and completeness
of different proof strategies used in sequential program verification.
Distributed directory books/proofstyles/ has three new directories
comprising that contribution: soundness/, completeness/, and
counterexamples/.  The existing books/proofstyles/ directory has been
moved to its subdirectory invclock/.

Jared Davis has contributed a profiling utility for ACL2 built on CCL
(OpenMCL).  See books/misc/oprof.lisp.  Thanks, Jared.

ACL2 utilities getprop and putprop take advantage of under-the-hood
Lisp (hashed) property lists.  The new book books/misc/getprop.lisp
contains an example showing how this works.

Added the following new book directories: books/paco/, which includes a
small ACL2-like prover; and books/models/jvm/m5, which contains the
definition of one of the more elaborate JVM models, M5, along with other
files including JVM program correctness proofs.  See files Readme.lsp in
these directories, and file README in the latter.

Added books about sorting in books/sorting.  See Readme.lsp in that
directory for documentation.

Added book books/misc/computed-hint-rewrite.lisp to provide an interface
to the rewriter for use in computed hints.  Thanks to Jared Davis for
requesting this feature.

Jared Davis has provided a pseudorandom number generator, in
books/misc/random.lisp.

Robert Krug has contributed a new library, books/arithmetic-4/, for
reasoning about arithmetic.  He characterizes it as being more powerful
than its predecessor, books/arithmetic-3/, and without its predecessor's
rewriting loops, but significantly slower than its predecessor on some
theorems.

Incorporated changes from Peter Dillinger to verify guards for
functions in books/ordinals/lexicographic-ordering.lisp (and one in
ordinal-definitions.lisp in that directory).

A new directory, books/hacking/, contains a library for those who wish
to use trust tags to modify or extend core ACL2 behavior.  Thanks to
Peter Dillinger for contributing this library.  Obsolete version
books/misc/hacker.lisp has been deleted.  Workshop contribution
books/workshops/2007/dillinger-et-al/code/ is still included with the
workshops/ tar file, but should be considered deprecated.

In books/make-event/assert.lisp, changed assert! and assert!-stobj to
return (value-triple :success) upon success instead of (value-triple
nil), following a suggestion from Jared Davis.

*EMACS SUPPORT*

Changed emacs/emacs-acl2.el so that the fill column default (for the
right margin) is only set (still to 79) in lisp-mode.

Modified Emacs support in file emacs/emacs-acl2.el so that names of
events are highlighted just as defun has been highlighted when it is
called.  Search in the above file for font-lock-add-keywords for
instructions on how to eliminate this change.

The name of the temporary file used by some Emacs utilities defined in
file emacs/emacs-acl2.el has been changed to have extension .lsp instead
of .lisp; thus it is now temp-emacs-file.lsp.  Also, `make' commands to
`clean' books will delete such files (specifically,
books/Makefile-generic has been changed to delete temp-emacs-file.lsp).

NOTE-3-4(R)    ACL2 Version  3.4(r) (August, 2008) Notes

Please also see NOTE-3-4 for changes to Version  3.4 of ACL2.

Fixed makefiles, books/nonstd/Makefile and GNUmakefile.  The old set-up
seemed to work fine as long as all books certified, but it was really
broken, for example only certifying some of the books in
books/nonstd/nsa/, and then only when required by books in other
directories.  Also fixed the "clean" target to clean links rather than
to make links.

NOTE-3-5    ACL2 Version  3.5 (May, 2009) Notes

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

Below we roughly organize the changes since Version  3.4 into the
following categories: changes to existing features, new features,
heuristic improvements, bug fixes, new and updated books, Emacs
support, and experimental hons version.  Each change is described in
just one category, though of course many changes could be placed in
more than one category.

*CHANGES TO EXISTING FEATURES*

Many improvements have been made to ACL2's "evisceration" mechanism for
hiding substructures of objects before they are printed, and to related
documentation:

     o A new documentation topic explains evisc-tuples.  See
     EVISC-TUPLE.

     o A new interface, set-evisc-tuple, has been provided for setting
     the four global evisc-tuples.  See SET-EVISC-TUPLE.

     o A new mode, "iprinting", allows eviscerated output to be read
     back in.  See SET-IPRINT.

     o Function default-evisc-tuple has been deprecated and will
     probably be eliminated in future releases; use abbrev-evisc-tuple
     instead.  Also eliminated is the brr-term-evisc-tuple (also the
     user-brr-term-evisc-tuple).  The term-evisc-tuple controls
     printing formerly controlled by the brr-term-evisc-tuple or
     user-brr-term-evisc-tuple.

     o ACL2 output is done in a more consistent manner, respecting the
     intention of those four global evisc-tuples.  In particular, more
     proof output is sensitive to the term-evisc-tuple.  Again, see
     SET-EVISC-TUPLE.

     o A special value, :DEFAULT, may be provided to set-evisc-tuple in
     order to restore these evisc-tuples to their original settings.

     o (Details for heavy users of the evisc-tuple mechanism) (1) There
     are no longer state globals named user-term-evisc-tuple or
     user-default-evisc-tuple.  (2) Because of the above-mentioned
     :DEFAULT, if you have referenced state globals directly, you
     should use accessors instead, for example (abbrev-evisc-tuple
     state) instead of (@ abbrev-evisc-tuple).  (3) For uniformity,
     set-trace-evisc-tuple now takes a second argument, state.

Improved break-on-error in several ways.  First, it breaks earlier in a
more appropriate place.  Thanks to Dave Greve for highlighting this
problem with the existing implementation.  Also, break-on-error now
breaks on hard errors, not only soft errors (see ER, options
hard and hard?).  Thanks to Warren Hunt and Anna Slobodova for sending
an example that showed a flaw in an initial improvement.  Finally, new
options cause printing of the call stack for some host Common Lisps.
See BREAK-ON-ERROR.  Thanks to Bob Boyer for requesting this
feature.

Trace! may now be used in raw Lisp (though please note that all
soundness claims are off any time you evaluate forms in raw Lisp!).
Thanks to Bob Boyer for feedback that led to this enhancement.

ACL2 now searches for file acl2-customization.lsp in addition to (and
just before) its existing search for acl2-customization.lisp; See
ACL2-CUSTOMIZATION.  Thanks to Jared Davis for suggesting this change,
which supports the methodology that files with a .lisp extension are
certifiable books (thus avoiding the need to set the BOOKS variable in
makefiles; see BOOK-MAKEFILES).

Improved the error message for illegal declare forms of the form (type
(satisfies ...)).  Thanks to Dave Greve for sending an example
highlighting the issue.

If trace output is going to a file (because open-trace-file has been
executed), then a note will be printed to that effect at the time that
a call of trace$ or trace! is applied to one or more trace specs.

The notion of redundancy (see REDUNDANT-EVENTS) has been made
more restrictive for mutual-recursion events.  Now, if either the old
or new event is a mutual-recursion event, then redundancy requires that
both are mutual-recursion events that define the same set of function
symbols.  Although we are not aware of any soundness bugs fixed by this
modification, nevertheless we believe that it reduces the risk of
soundness bugs in the future.

The definition of trace* has been moved to a book, misc/trace1.lisp.  A
new version, used in ACL2s, is in book misc/trace-star.lisp.  Trace
utilities trace$ and trace! are still built into ACL2.  [Note: File
misc/trace1.lisp was deleted after Version  4.2.]

Certain certificate files will now be much smaller, by printing in a way
that takes advantage of structure sharing.  Certifying the following
example produces a .cert file of over 3M before this change, but less
than 1K after the change.

     (defun nest (i)
       ;; Makes an exponentially-sized nest of conses i deep.
       (if (zp i)
           nil
         (let ((next (nest (1- i))))
           (cons next next))))

     (make-event
      `(defconst *big* ',(nest 20)))

Thanks to Sol Swords for providing the above example and to him as well
as to Bob Boyer, Jared Davis, and Warren Hunt for encouraging
development of this improvement.  We have also applied this improvement
to the printing of function definitions to files on behalf of
certify-book and comp.

Names of symbols are now printed with vertical bars according to the
Common Lisp spec.  Formerly, if the first character of a symbol name
could be the first character of the print representation of a number,
then the symbol was printed using vertical bars (|..|) around its name.
Now, a much more restrictive test for "potential numbers" is used,
which can result in fewer such vertical bars.  Base 16 is now carefully
considered as well; see SET-PRINT-BASE.  Thanks to Bob Boyer
for requesting this improvement.  Note that macros set-acl2-print-base
and set-acl2-print-case have been replaced by functions; see
SET-PRINT-BASE and see SET-PRINT-CASE.

The ACL2 reader now supports `#.' syntax in place of the `#, syntax
formerly supported.  Thanks to Bob Boyer for requesting this change.
See SHARP-DOT-READER.  NOTE that because of this change, `#.'
no longer causes an abort; instead please use (a!) or optionally, if in
the ACL2 loop, :a!; see A!.

Some small changes have been made related to gag-mode:

     o Gag-mode now suppresses some messages that were being printed
     upon encountering disjunctive splits from :OR hints.  Thanks to Sol
     Swords for suggesting this improvement.

     o ACL2 had printed "Q.E.D." with all output suppressed and
     gag-mode enabled.  Now, "Q.E.D." will be suppressed when PROVE and
     SUMMARY output are suppressed, even if gag-mode is enabled.

     o The use of set-gag-mode had drastic effects on the inhibited
     output (see SET-INHIBIT-OUTPUT-LST), basically inhibiting
     nearly all output (even most warnings) when turning on gag-mode
     and enabling all output except proof-tree output when turning off
     gag-mode.  Now, set-gag-mode only inhibits or enables proof
     (PROVE) output, according to whether gag-mode is being turned on
     or off (respectively).  The related utility set-saved-output has
     also been modified, basically to eliminate :all as a first
     argument and to allow t and :all as second arguments, for
     inhibiting prover output or virtually all output, respectively
     (see SET-SAVED-OUTPUT).

A defstub event signature specifying output of the form (mv ...) now
introduces a :type-prescription rule asserting that the new function
returns a true-listp result.  Thanks to Bob Boyer for sending the
following example, which motivated this change.

     (defstub census (*) => (mv * *))
     (defn foo (x)
       (mv-let (a1 a2)
               (census x)
               (list a1 a2)))

Improved the efficiency of string-append so that in raw Lisp, it calls
concatenate.  Thanks to Jared Davis for suggesting this change,
including the use of mbe.  A minor change was made to the definition of
concatenate to support this change, and the lemma append-to-nil was
added (see below).

The checksum algorithm used for certificate files of books has been
changed.  Thanks to Jared Davis for contributing the new code.  This
change will likely not be noticed unless one is using the experimental
hons version of ACL2, where it can greatly speed up book certification
and inclusion because of function memoization (of source function
fchecksum-obj).

Fewer calls are made to the checksum algorithm on behalf of
certify-book and a few other operations.  Thanks to Jared Davis for
providing data that helped lead us to these changes.

Formatted printing directives ~p, ~q, ~P, and ~Q are deprecated, though
still supported.  See FMT.  Instead, please use ~x, ~y, ~X, and
~Y (respectively).  As a by-product, rule names in proof output are no
longer hyphenated.

A new keyword, :multiplicity, is available for tracing raw Lisp
functions using the ACL2 trace utility.  See TRACE$.

Users may now control whether or not a slow array access results in a
warning printed to the screen (which is the default, as before), and if
so, whether or not the warning is followed by a break.  See
SLOW-ARRAY-WARNING.

On linux-like systems (including Mac OS X and SunOS), :comp will now
write its temporary files into the "/tmp" directory, which is the value
of state global 'tmp-dir.  You can change that directory with (assign
tmp-dir "<your_temp_directory_path>").

The messages printed for uncertified books have been enhanced.  Thanks
to Jared Davis for requesting such an improvement.

A function definition that would be redundant if in :logic mode is now
considered redundant even if it (the new definition) is in :program
mode.  That is, if a definition is "downgraded" from :logic to :program
mode, the latter (:program mode) definition is considered redundant.
Previously, such redundancy was disallowed, but we have relaxed that
restriction because of a scenario brought to our attention by Jared
Davis: include a book with the :logic mode definition, and then include
a book with the :program mode definition followed by
verify-termination.  Thanks, Jared.

The ACL2 reader no longer accepts characters other than those
recognized by standard-char-p except for #\Tab, #\Page, and #\Rubout
(though it still accepts strings containing such characters).  As a
result, no make-event expansion is allowed to contain any such
unacceptable character or string.  Thanks to Sol Swords for sending an
example that led us to make this restriction.  A simple example is the
following book:

     (in-package "ACL2")
     (defconst *my-null* (code-char 0))
     (make-event `(defconst *new-null* ,*my-null*))

For this book, a call of certify-book formerly broke during the
compilation phase, but if there was no compilation, then a call of
include-book broke.  Now, the error occurs upon evaluation of the
make-event form.

ACL2 now collects up guards from declare forms more as a user might
expect, without introducing an unexpected ordering of conjuncts.  We
thank Jared Davis for sending us the following illustrative example,
explained below.

     (defun f (x n)
       (declare (xargs :guard (and (stringp x)
                                   (natp n)
                                   (= (length x) n)))
                (type string x)
                (ignore x n))
       t)

Formerly, a guard was generated for this example by unioning the
conjuncts from the :guard onto a list containing the term (string x)
generated from the type declaration, resulting in an effective guard of:

     (and (natp n)
          (= (length x) n)
          (stringp x))

The guard of this guard failed to be verified because (stringp x)) now
comes after the call (length x).  With the fix, contributions to the
guards are collected up in the order in which they appear.  So in the
above example, the effective guard is the specified :guard; the
contribution (stringp x) comes later, and is thus dropped since it is
redundant.  NOTE by the way that if :guard and :stobjs are specified in
the same xargs form, then for purposes of collecting up the effective
guard as described above, :stobjs will be treated as through it comes
before the :guard.

Modified close-output-channel to try to do a better job flushing
buffers.  Thanks to Bob Boyer for helpful correspondence.

The notion of "subversive recursion" has been modified so that some
functions are no longer marked as subversive.  See
SUBVERSIVE-RECURSIONS, in particular the discussion elaborating on
the notion of "involved in the termination argument" at the end of that
documentation topic.

Formerly, :type-prescription rules for new definitions inside
encapsulate forms were sometimes added as constraints.  This is no
longer the case.  See also discussion of the "soundness bug in the
forming of constraints", which is related.

*NEW FEATURES*

It is now possible to affect ACL2's termination analysis (and resulting
induction analysis).  Thanks to Peter Dillinger for requesting this
feature.  The default behavior is essentially unchanged.  But for
example, the following definition is accepted by ACL2 because of the
use of the new :ruler-extenders features; See RULER-EXTENDERS.

       (defun f (x)
         (declare (xargs :ruler-extenders :all))
         (cons 3
               (if (consp x)
                   (f (cdr x))
                 nil)))

The following lemma was added in support of the improvement to
string-append described above:

     (defthm append-to-nil
       (implies (true-listp x)
                (equal (append x nil)
                       x)))

A mechanism has been provided for users to contribute documentation.
See MANAGING-ACL2-PACKAGES for an example, which contains a
link to an external web page on effective use of ACL2 packages, kindly
provided by Jared Davis.  ACL2 documentation strings may now link to
external web pages using the new symbol, ~url; see MARKUP.  Of
course, those links appear in the web version of the documentation, but
you made need to take a bit of action in order for these to appear as
links in the Emacs Info version; see DOCUMENTATION.

Added intersectp (similar to intersectp-eq and intersectp-equal).

The user now has more control over how ACL2 prints forms; See
PRINT-CONTROL.  Thanks to Bob Boyer for useful discussions leading to
this enhancement.

Some Common Lisp implementations only allow the syntax
pkg-name::expression when expression is a symbol.  The ACL2 reader has
been modified to support a package prefix for arbitrary expressions;
see SHARP-BANG-READER.  Thanks to Hanbing Liu for a query that
led to this feature and to Pascal J. Bourguignon for suggesting an
implmentation.

Ill-formed documentation strings need not cause an error.  See
SET-IGNORE-DOC-STRING-ERROR.  Thanks to Bob Boyer for requesting this
feature.

Type declarations are now permitted in let* forms; see LET*,
see DECLARE, and see TYPE-SPEC.

(For Lisp programmers) Macro with-live-state has been provided for
programmers who refer to free variable STATE, for example with macros
that generate uses of STATE, and want to avoid compiler warnings when
evaluating in raw Lisp.  For example, the following form can be
submitted either inside or outside the ACL2 loop to get the desired
effect (see DOC-STRING): (with-live-state (f-put-global
'doc-prefix " " state)).  For another example use of this macro, see
the definition of trace$ (ACL2 source file other-events.lisp).

(System hackers only) Added :redef- to undo the effect of :redef+.  See
REDEF-.

Function random$ is a built-in random number generator.  See
RANDOM$.  Thanks to Sol Swords for requesting this feature and
providing an initial implementation.

*HEURISTIC IMPROVEMENTS*

Sped up guard generation for some functions with large if-then-else
structures in their bodies.  Thanks to Sol Swords for sending an
illustrative example.

Sped up guard generation in some cases by evaluating ground
(variable-free) subexpressions.  Thanks to Bob Boyer for sending a
motivating example: (defn foo (x) (case x ((1 2) 1) ((3 4) 3) ... ((999
1000) 999))).

Modified slightly a heuristic association of "size" with constants,
which can result in significant speed-ups in proofs involving constants
that are very large cons trees.

Added a restriction in the linear arithmetic procedure for deleting
polynomial inequalities from the linear database.  Formerly, an
inequality could be deleted if it was implied by another inequality.
Now, such deletion requires that certain heuristic "parent tree"
information is at least as restrictive for the weaker inequality as for
the stronger.  Thanks to Dave Greve for bringing a relevant example to
our attention and working with us to figure out some surprising
behavior, and to Robert Krug for making a key observation leading to
the fix.

(GCL especially) Improved compiled code slightly by communicating to
raw Lisp the output type when a function body is of the form (the
character ...).  This tiny improvement will probably only be observed
in GCL, if at all.

Applied a correction suggested by Robert Krug to the variant of
term-order used in parts of ACL2's arithmetic reasoning.

*BUG FIXES*

Fixed bugs in the handling of flet expressions, one of which had the
capability of rendering ACL2 unsound.  Thanks to Sol Swords for
pointing out two issues and sending examples.  One example illustrated
how ACL2 was in essence throwing away outer flet bindings when
processing an inner flet.  We have exploited that example to prove a
contradiction, as follows: this book was certifiable before this fix.

     (in-package "ACL2")

     (defun a (x)
       (list 'c x))

     ; Example from Sol Swords, which failed to be admitted (claiming that
     ; function A is undefined) without the above definition of A.
     (defun foo1 (x y)
        (flet ((a (x) (list 'a x)))
          (flet ((b (y) (list 'b y)))
            (b (a (list x y))))))

     (defthm not-true
       (equal (foo1 3 4)
              '(b (c (3 4))))
       :hints (("Goal"
                :in-theory
                (disable (:executable-counterpart foo1))))
       :rule-classes nil)

     (defthm contradiction
       nil
       :hints (("Goal" :use not-true))
       :rule-classes nil)

Sol's second example, below, pointed to a second bug related to
computing output signatures in the presence of nested flet expressions,
which we have also fixed: this form failed before the fix.

     :trans (flet ((foo (a) (list (flet ((bar (b) b)) a)))) x)

Fixed a subtle soundness bug in the forming of constraints from deduced
type prescriptions.  As a result, when ACL2 prints a warning message
labeling encapsulated functions as "subversive", ACL2 will no longer
deduce :type-prescription rules for those functions.  Examples that
exploit the bug in ACL2 Version_3.4 may be found in comments in ACL2
source function convert-type-set-to-term (file other-processes.lisp) and
especially in function putprop-type-prescription-lst (file
defuns.lisp).  For more on the general issue of "subversive
recursions," see SUBVERSIVE-RECURSIONS.)

Fixed a soundness bug in the handling of inequalities by the type-set
mechanism, which was using the inequality database inside the body of a
lambda.

Fixed a long-standing soundness bug in compress1 and compress2, whose
raw Lisp code gave the logically incorrect result in the case of a
single entry other than the header, where that entry mapped an index to
the default value.  Also fixed soundness bugs in compress1, in the case
of :order >, where the raw Lisp code could drop the header from the
result or, when the input alist had entries in ascending order, fail to
return an alist in descending order.  For example, the following book
certified successfully.

     (in-package "ACL2")
     (defthm true-formula-1
       (equal (compress1 'a '((:HEADER :DIMENSIONS (4) :MAXIMUM-LENGTH 5
                                       :DEFAULT 1 :NAME A :ORDER <)
                              (1 . 1)))
              '((:HEADER :DIMENSIONS (4) :MAXIMUM-LENGTH 5
                         :DEFAULT 1 :NAME A :ORDER <)))
       :hints (("Goal" :in-theory (disable (compress1))))
       :rule-classes nil)
     (defthm ouch-1
       nil
       :hints (("Goal" :use true-formula-1))
       :rule-classes nil)
     (defthm true-formula-2
       (equal (compress1 'a '((:HEADER :DIMENSIONS (4) :MAXIMUM-LENGTH 5
                                       :DEFAULT NIL :NAME A :ORDER >)
                              (1 . 1)
                              (2 . 2)))
              '((:HEADER :DIMENSIONS (4) :MAXIMUM-LENGTH 5
                         :DEFAULT NIL :NAME A :ORDER >)
                (2 . 2)
                (1 . 1)))
       :hints (("Goal" :in-theory (disable (compress1))))
       :rule-classes nil)
     (defthm ouch-2
       nil
       :hints (("Goal" :use true-formula-2))
       :rule-classes nil)
     (defthm true-formula-3
       (equal (compress1 'a '((:HEADER :DIMENSIONS (3) :MAXIMUM-LENGTH 4
                                       :NAME A :ORDER >)
                              (1 . B)
                              (0 . A)))
              '((:HEADER :DIMENSIONS (3) :MAXIMUM-LENGTH 4
                         :NAME A :ORDER >)
                (1 . B)
                (0 . A)))
       :hints (("Goal" :in-theory (disable (compress1))))
       :rule-classes nil)
     (defthm ouch-3
       nil
       :hints (("Goal" :use true-formula-3))
       :rule-classes nil)

Fixed a soundness bug involving measured subsets and verify-termination,
by changing verify-termination so that it uses make-event.  See
VERIFY-TERMINATION, in particular the discussion about make-event
near the end of that documentation topic.  Peter Dillinger first raised
the idea to us of making such a change; when we found this soundness
bug, we were certainly happy to do so!

Fixed a bug that could cause a hard Lisp error but not, apparently,
unsoundness.  The bug was in the lack of attention to the order of
guard and type declarations when checking for redundancy.  In the
following example, the second definition was redundant during the first
pass of the encapsulate form.  The second definition, however, was
stored on the second pass with a guard of (and (consp (car x)) (consp
x)), which caused a hard Lisp error when evaluating (foo 3) due to a
misguided attempt to evaluate (car 3) in raw Lisp.  The fix is to
restrict redundancy of definitions so that the guard and type
declarations must be in the same order for the two definitions.

     (encapsulate
      ()
      (local (defun foo (x)
               (declare (xargs :guard (consp x)))
               (declare (xargs :guard (consp (car x))))
               x))
      (defun foo (x)
        (declare (xargs :guard (consp (car x))))
        (declare (xargs :guard (consp x)))
        x))
     ; Now we get a hard Lisp error from evaluation of the guard of foo:
     (foo 3)

Fixed a bug in the guard violation report for function
intern-in-package-of-symbol.  Thanks to Dave Greve for bringing this
bug to our attention.

Made a change to allow certain hints, in particular certain
:clause-processor hints, that had previously caused errors during
termination proofs by viewing the function being defined as not yet
existing.  Thanks to Sol Swords for bringing this issue to our
attention with a nice example.

ACL2 now properly handles interrupts (via control-c) issued during
printing of the checkpoint summary.  Previously it was possible on some
platforms to make ACL2 hang when interrupting both during a proof and
during the ensuing printing of the checkpoint summary.  Thanks to Jared
Davis and Sol Swords for bringing this problem to our attention.

Fixed a bug that was preventing, inside some book "b", the use of a
:dir argument to include-book that refers to a directory defined using
add-include-book-dir earlier in the book "b".  (We found this
ourselves, but we thank John Cowles for observing it independently and
sending us a nice example.)

(GCL and CCL only) Fixed a bug in certain under-the-hood type
inferencing.  Thanks to Sol Swords for sending an example using stobjs
defined with the :inline keyword, along with a helpful backtrace in
CCL, and to Gary Byers for his debugging help.

Fixed a bug in print-gv, which was mishandling calls of functions with
more than one argument.

Fixed a bug in the handling of AND and OR terms by the proof-checker
command DV, including numeric ("diving") commands.  Thanks for Mark
Reitblatt for bringing this problems to our attention with a helpful
example.

Fixed printing of goal names resulting from the application of :OR
hints so that they aren't ugly when working in other than the "ACL2"
package.  Thanks to Sol Swords for bringing this issue to our attention.

Fixed proof-tree printing so that interrupts will not cause problems
with hiding ordinary output because of incomplete proof-tree output.
Thanks to Peter Dillinger for pointing out this issue.

Fixed a hard error that could be caused by mishandling a forced
hypothesis during forward-chaining.  Thanks to Peter Dillinger for
bringing this bug to our attention by sending a useful example.

Fixed a bug that could cause simplifications to fail because of alleged
"specious simplification."  This bug could appear when deriving an
equality from the linear arithmetic database, and then attempting to
add this equality to the current goal's hypotheses when it was already
present.  Thanks to Eric Smith for sending a helpful example (in July
2005!) that helped us debug this issue.

Fixed a bug in processing of :type-set-inverter rules.

Fixed a bug that was causing an error, at least for an underlying Lisp
of CCL (OpenMCL), when ec-call was applied to a term returning multiple
values.  Thanks to Sol Swords for sending an example that brought this
bug to our attention.

Fixed handling of array orders to treat keyword value :order :none
correctly from an array's header.  Previously, there were two problems.
One problem was that :order :none was treated like the default for
:order, <, while :order nil was treated in the manner specified by
:order :none (see ARRAYS).  Now, both :order :none and :order
nil are treated as :order nil had been treated, i.e., so that there is
no reordering of the alist by compress1.  The other problem with this
case of :order was that the :maximum-length field of the header was not
being respected: the length could grow without bound.  Now, as
previously explained (but not previously implemented) -- see
ARRAYS -- a compress1 call made on behalf of aset1 causes a hard
error if the header of the supplied array specifies an :order of :none
or nil.

An ignorable declare form had caused an error in some contexts when it
should have been allowed.  In particular, this problem could arise when
using an ignorable declaration at the top level in a defabbrev form.
It could also arise upon calling verify-termination when the
corresponding defun form contained an ignorable declaration at the top
level.  These bugs have been fixed.

Contrary to existing documentation (see MAKE-EVENT-DETAILS),
the value of "ld special variable" ld-skip-proofsp was always set to nil
during make-event expansion, not merely when the make-event form has a
non-nil value for keyword parameter :check-expansion.  This has been
fixed.  Thanks to Sol Swords for bringing this issue to our attention.

We have disallowed the certification of a book when not at the
top-level, either directly in the top-level loop or at the top level of
ld.  Before this restriction, the following would certify a book with a
definition such as (defun foo (x) (h x)) that calls function h before
defining it, if the certification was by way of the form such as:

     (er-progn (defun h (x) x) (certify-book "my-book"))

But a subsequent include-book of "my-book" would then fail, because h
is not defined at the top level.

Printing with fmt directive ~c now works properly even when the
print-base is other than 10.  Thanks to Sol Swords for reporting this
bug and providing a fix for it.

(SBCL, CMUCL, and CCL only) Fixed a bug in sys-call-status in the case
that the underlying Common Lisp is SBCL, CMUCL, or CCL (OpenMCL).
Thanks to Jun Sawada for bringing this bug to our attention and
providing a fix.

Fixed a bug that was preventing local defstobj events in encapsulate
events.  Thanks to Jared Davis for bringing this bug to our attention.

Fixed a bug evidenced by error message "Unexpected form in certification
world", which could result from attempting to certify a book after
evaluating an encapsulate form with a local defmacro.  Thanks to Jared
Davis for pointing out ths bug and sending the example:

     (encapsulate
      ()
      (local (defmacro foo (x) `(table foo 'bar ,x)))
      (local (foo 3)))

Formerly, evaluating a trace$ form inside a wormhole such as the
break-rewrite loop could leave the user in a bad state after returning
to the top level, in which that function could not be untraced.  This
has been fixed.  Note however that when you proceed from a break in the
break-rewrite loop, the tracing state will be the same as it was when
you entered that break: all effects of calling trace$ and untrace$ are
erased when you proceed from the break.

A :guard of (and) is no longer ignored.  Thanks to Sol Swords for
bringing this bug to our attention.

A bug has been fixed that could result in needlessly weak induction
schemes in the case that a recursive call is made in the first argument
of prog2$.  This has been fixed by including prog2$ as a default
ruler-extender in the new ruler-extenders feature (see above, and see
RULER-EXTENDERS).  For details on this bug see Example 11 in
distributed book books/misc/misc2/ruler-extenders-tests.lisp.

(For CCL/OpenMCL on Windows) ACL2 should now build on CCL (OpenMCL) on
Windows.  Thanks to David Rager for bringing this issue to our
attention and helping with a fix that worked for CCL 1.2, and to the
CCL team for improving handling of Windows-style filenames in CCL 1.3.

*NEW AND UPDATED BOOKS*

See `http://code.google.com/p/acl2-books/wiki/BooksSince34' for a list
of books in Version  3.5 of ACL2 but not Version  3.4.

Run the shell command

     svn log -r 94:HEAD

to see all changes to books/ since the release of Version  3.4.

Here are just a few highlights.

Thanks largely to Jared Davis, many Makefiles have been improved to do
automatic dependency analysis.  See BOOK-MAKEFILES for how to
get your own Makefiles to do this by adding a line: -include
Makefile-deps.

Libraries books/arithmetic-4/ and books/rtl/rel7/ have been eliminated
from the default book certification (make regression), in favor of new
libraries books/arithmetic-5/ and books/rtl/rel8/ contributed by Robert
Krug and Hanbing Liu, respectively.  They and Jun Sawada have arranged
the compatibility of these libraries; i.e., it is possible to evaluate
both of the following in the same session:

     (include-book "arithmetic-5/top" :dir :system)
     (include-book "rtl/rel8/lib/top" :dir :system)

Library books/rtl/rel1/ is no longer certified by default (though it is
still distributed in support of ACL2(r); see REAL).

*EMACS SUPPORT*

Slightly modified Control-t e (defined in emacs/emacs-acl2.el) to
comprehend the notion of an "ACL2 scope", and added Control-t o to
insert a superior encapsulate defining such a scope.  See the Emacs
documentation for Control-t e (generally obtained after typing
Control-h k).

Modified distributed file emacs/emacs-acl2.el so that if you put the
following two forms in your ~/.emacs file above the form that loads
emacs/emacs-acl2.el, then Emacs will not start up a shell.  Thanks to
Terry Parks for leading us to this modification.

     (defvar acl2-skip-shell nil)
     (setq acl2-skip-shell t)

*EXPERIMENTAL HONS VERSION*

Bob Boyer and others have contributed numerous changes for the
experimental "hons" version of ACL2 (see HONS-AND-MEMOIZATION).

The ACL2 state can now be queried with (@ hons-enabled) so that a
result of t says that one is in the experimental hons version, while
nil says the opposite.

NOTE-3-5(R)    ACL2 Version  3.5(r) (May, 2009) Notes

Please also see NOTE-3-5 for changes in Version  3.5 of ACL2.

This release incorporates improvements from Ruben Gamboa in support for
non-standard analysis in ACL2(r), in the following ways:

ACL2(r) now supports non-classical objects that are not also numeric,
e.g., non-classical cons pairs.  Consequently, the built-in
standard-numberp has been replaced with standardp.

If f is a classical function, the value (f x1 ... xn) is guaranteed to
be standard when the xi are standard.  ACL2(r) can now recognize this
fact automatically, using defun-std.  For example, the following can be
used to assert that the square root of 2 is a standard value.

     (defthm-std sqrt-2-rational
       (standardp (acl2-sqrt 2)))

More generally, the expression (f x1 ... xn) can contain free variables,
but the result is guaranteed to be standard when the variables take on
standard variables, as in the following:

     (defthm-std sqrt-x-rational
       (implies (standardp x)
                (standardp (acl2-sqrt x))))

A potential soundness bug in encapsulate was fixed.  Specifically, when
a classical, constrained function is instantiated with a lambda
expression containing free variables, it may produce non-standard
values depending on the values of the free variables.  This means that
the functional instantiation cannot be used to justify a non-classical
theorem.  For example, consider the following sequence:

     (encapsulate
       ((f (x) t))
       (local (defun f (x) x)))
     (defthm-std f-x-standard
       (implies (standardp x)
                (standardp (f x))))
     (defthm plus-x-standard
       (implies (standardp x)
                (standardp (+ x y)))
       :hints (("Goal"
                :use ((:functional-instance f-x-standard
                                            (f (lambda (x) (+ x y))))))))
     (defthm plus-x-eps-not-standard
       (implies (standardp x)
                (not (standardp (+ x (/ (i-large-integer)))))))
     (defthm nil-iff-t
       nil
       :hints (("Goal"
               :use ((:instance plus-x-standard
                                (y (/ (i-large-integer))))
                     (:instance plus-x-eps-not-standard)))))

ACL2(r) also supports the introduction of non-classical functions with
defchoose.  These behave just as normal functions introduced with
defchoose, but they have a non-classical choice property.

Finally, ACL2(r) now comes with a revamped library supporting
non-standard analysis, still distributed separately as books/nonstd/.
The new library uses defchoose to state more natural and useful
versions of the IVT, MVT, etc.  It also supports the introduction of
inverse functions, e.g., logarithms.  Finally, the library has much
more extensive support for differentiation.

NOTE-3-6    ACL2 Version  3.6 (August, 2009) Notes

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

Below we roughly organize the changes since Version  3.5 into the
following categories of changes: existing features, new features,
heuristic improvements, bug fixes, distributed books, Emacs support,
and experimental hons-and-memoization version.  Each change is
described in just one category, though of course many changes could be
placed in more than one category.

Note that (starting with ACL2 Version  3.5) LispWorks is no longer
supported as a platform for ACL2, as the LispWorks compiler could not
handle the ACL2 sources; see comments in the ACL2 sources about
"function size" being "too large".

*CHANGES TO EXISTING FEATURES*

In the xargs declare form, the function symbol (or symbols, plural, in
the case of mutual-recursion) being defined may now be used in the
specified :measure and :guard terms.  Note that, the definition(s) of
the new symbol(s) are still not used in the termination proof.  Thanks
to Daron Vroon for discussions leading to this addition for the measure
and to Dave Greve for requesting such an enhancement for the guard.

Processing of the :guard-hints in an xargs declare form is now delayed
until the start of guard verification.  As a result, the function
symbol(s) being defined may now be used as one might expect in such
hints, for example in an :in-theory form.  Thanks to Jared Davis for
suggesting that we make such an improvement and providing an example.

Made a low-level change to make-event in support of the ACL2s utility
"dynamic-make-event".  Thanks to Peter Dillinger for explaining the
issue leading to this change.

Modified the failure message printed when a measure conjecture fails to
be proved, to indicate whether or not the hint :ruler-extenders :all
would create a different measure conjecture.  Thanks to Peter Dillinger
for suggesting such a modification.

A call of add-default-hints had added hints to the end of the current
list of default hints.  Now, it adds them to the beginning of that
list, so that they are tried first.  However, add-default-hints now
takes a keyword argument, :at-end.  If that argument is supplied and
evaluates to other than nil, then the previous behavior occurs.

When save-exec is used to save ACL2 images, the build dates are now
printed on separate lines at startup and in the executable script.
Thanks To Bob Boyer for requesting some newlines.

Forward-chaining rules are now generated so that every let (also let*
and lambda) expression is expanded away, as is every call of a
so-called "guard holder" (must-be-equal, prog2$, ec-call, the).  These
were formerly only expanded away in the conclusion.  Thanks to Konrad
Slind for a helpful email leading to this change.

Current-theory now causes a hard error when applied to a name not found
in the current ACL2 logical world, rather than simply returning nil.

When the underlying Common Lisp is GCL, ACL2 no longer uses the #n=
reader macro when writing out certain files, including certificate
files.  In all other Lisps, it now uses the #n= "print-circle" feature
not only for certificate files and "expansion.lsp" files written for
example in support of make-event, but also for files written in support
of :comp.  This is all managed with new state global variable
print-circle-files; see PRINT-CONTROL.  Thanks to Dave Greve
for pointing out that GCL is limited by default to 1024 indices for #n=.

*NEW FEATURES*

A documentation topic explains in some detail how hints work with the
ACL2 proof "waterfall": see HINTS-AND-THE-WATERFALL.  This
topic may be useful to those who write computed hints (see
COMPUTED-HINTS) or other advanced hints.

Added a new hint keyword, :no-thanks, that avoids printing the usual
"Thanks" message for hints.  Thanks to Peter Dillinger for requesting
this feature.

Added a new hint keyword, :backtrack, that checks the goals produced by
processing a goal, and can cause the goal to be re-processed using a new
hint.  See HINTS.  Thanks to Pete Manolios for a conversation
that led to the idea of this hint.

Added a new class of hints, override-hints, that is similar to
default-hints, except that override-hints are always applied, even if
the user has supplied a hint explicitly for the goal.  See
OVERRIDE-HINTS.  Thanks to Pete Manolios and Harsh Raju Chamarthi for
useful discussions on this topic, including its application to testing.

When a goal ready to be pushed for proof by induction is given the new
hint ":do-not-induct :otf", it is indeed pushed for proof by induction,
rather than causing immediate failure as in the case of the hint
":do-not-induct t".  Instead, the proof fails when the goal is later
picked to be proved by induction.  Thanks to Peter Dillinger for
discussions leading to this feature.

Related to computed hints only: Each history entry in the list stored in
variable HIST (see COMPUTED-HINTS) now has a :CLAUSE field,
which provide's access to a goal's parent, parent's parent, and so on
(within the same induction and forcing round only).

It is now possible to inhibit warnings produced by in-theory events and
hints that occur when certain built-in definitions and
executable-counterparts are disabled: just evaluate (assign
verbose-theory-warning nil).  Thanks to Jared Davis (and probably
others in the past) for requesting such a mechanism.

*HEURISTIC IMPROVEMENTS*

A source function (linearize-lst) was replaced by tail-recursive code,
which can avoid a stack overflow.  Thanks to Dave Greve for sending a
helpful example.

The heuristics for limiting forward-chaining have been slightly relaxed,
to allow derivations based on the occurrence of all arguments of the
forward-chaining rule's conclusion in the goal (after stripping leading
calls of NOT).  Thanks to Dave Greve for contributing this improvement
and providing a motivating example.

We simplified induction schemes by eliminating each hypothesis of the
form (not (equal term (quote const))) for which some other hypothesis
in the same case equates term with some (presumably other) quoted
constant.  Thanks to Dave Greve for requesting an improvement of this
sort.

*BUG FIXES*

Fixed a soundness bug related to redundancy of encapsulate events (see
REDUNDANT-EVENTS) and ruler-extenders.  A proof of nil in ACL2
Version  3.5 appears in a comment in (deflabel note-3-6 ...) in the ACL2
source code.  The fix is to insist that in order for one encapsulate
event to be redundant with another, they must be evaluated with the same
default-ruler-extenders.  Analogous to this issue of
default-ruler-extenders for encapsulates is an issue of the
default-verify-guards-eagerness, which has similarly been fixed.

Fixed soundness bugs related to the handling of subversive-recursions
for constraints.  Proofs of nil in ACL2 Version  3.5 appear in a
comment in (deflabel note-3-6 ...) in the ACL2 source code.

Fixed a bug that could cause the following error during calls of
certify-book in the presence of calls of skip-proofs in the book:

        ACL2 Warning [Skip-proofs] in

        HARD ACL2 ERROR in FMT0: Illegal Fmt Syntax.  The tilde-@ directive at
        position 0 of the string below is illegal because its variable evaluated
        to 0, which is neither a string nor a list.

        "~@0"

Thanks to Dave Greve for reporting this bug and making available a very
helpful test case.

The :corollary of a rule (see RULE-CLASSES) failed to use the
default-hints of the logical world.  This has been fixed.

(CCL only) We removed a call, for CCL 1.3 (and beyond) only, of foreign
function sync in the closing of output channels.  Thanks to Daron Vroon
for reporting issues with such a call on a non-Intel platform.

Fixed a bug in reporting failures when monitoring rewrite rules with
free variables in the hypotheses, that could cause a hard Lisp error
(from which ACL2 continues, however).  Thanks to Eric Smith for sending
a very helpful example with his bug report.

Fixed the handling of :induct hints, which had thrown away hint
information from parent goals.  For example, the thm form below failed
to prove even though the second hint is in some sense superfluous;
induction occurs automatically at "Goal'" even without the hint on
that.  The failure was due to discarding the hint information on "Goal".

     (in-theory (disable append))
     (thm (equal (cdr (cons a (append (append x y) z))) (append x y z))
          :hints
          (("Goal" :in-theory (enable append))
           ("Goal'" :induct t) ; failed unless this line is commented out
           ))

Fixed a bug in the args command that was failing to show the formals of
primitives (built-in functions like consp that do not come with explicit
definitions).  Thanks to John Cowles for pointing out this bug.  (At a
lower level, the bug was that primitives failed to have 'stobjs-in or
'stobjs-out properties.)

Fixed bugs in the utility supporting moving directories of certified
books, sometimes used in Debian builds (as described in source function
make-certificate-file).  Thanks to Alan Dunn for pointing out such a
bug, in paths associated with defpkg events in portcullis commands in
certificates (which are used for error reporting).  There were also
bugs, now fixed, that prevented renaming some book paths.  Please note
that this mechanism is not guaranteed to be sound; in particular, it
can probably misbehave when macros are used to generate portcullis
events.  However, it seems likely that such issues will be very rare.

Eliminated warnings that could arise when tracing a function with
trace$.  Now, when trace$ is applied to a function without option
:native, that function's declarations and documentation are discarded.

Fixed a bug that could cause a failure when building an executable image
using SBCL as the underlying Common Lisp.  Thanks to Jun Sawada for
reporting this failure.  We made a similar fix for CMUCL.

Fixed a bug in save-exec in the case that an absolute pathnanme is
supplied.  Thanks to Jared Davis for bringing this bug to our attention.

Fixed a bug in the use of trace$ with the :native and :multiplicity
options that caused hard errors for some underlying Lisps.

Fixed a bug in the interaction of trace$ and :comp, which caused error
as comp tried to re-trace functions that it temporarily untraced.

*NEW AND UPDATED BOOKS AND RELATED INFRASTRUCTURE*

See `http://code.google.com/p/acl2-books/wiki/BooksSince35' for a list
of books in Version  3.6 of ACL2 but not Version  3.5.  For _changes_ to
existing books rather than _additions_, see the log entries at
`http://code.google.com/p/acl2-books/source/list' starting with revision
r286 up through revision r329.

It is no longer required to specify a value for environment (or `make')
variable ACL2_SYSTEM_BOOKS when running make in the distributed book
directory, even when that directory is not under the directory
containing the ACL2 executable.  Thanks to Peter Dillinger for
providing this improvement, by modifying books/Makefile-generic and, as
needed, distributed book Makefiles.

Thanks to Peter Dillinger, some books in support of the ACL2 Sedan
(ACL2s) are more easily available for ACL2 users who do not use ACL2s.
See ACL2-SEDAN.

*EMACS SUPPORT*

If the following form is evaluated before the load of
emacs/emacs-acl2.el, then variables are now set to reflect the directory
containing that file.

     (if (boundp '*acl2-sources-dir*)
         (makunbound '*acl2-sources-dir*))

Fixed info-dir-entry line in generated info file (by patching
doc/write-acl2-texinfo.lisp).  Thanks to Alan Dunn for providing this
patch.

*EXPERIMENTAL HONS VERSION*

Bob Boyer and others have contributed numerous changes for the
experimental "hons" version of ACL2 (see HONS-AND-MEMOIZATION).
A number of these have been crafted to work specifically with CCL
(Clozure Common Lisp, formerly OpenMCL), which is now required as the
underlying Lisp for the "hons" version of ACL2.

A heuristic (source function too-many-ifs has been made more scalable
(for the non-HONS version as well, in fact), but with no functional
change.  Thanks to Jared Davis for noticing performance issues and
suggesting fixes.

Other changes including the following, quoting Bob Boyer:

     The CCL CASE macro now does better than a dumb linear search in
     some CASEes.

     SH and CSH are functions to talk to the underlying Gnu-Linux from
     CCL.  Good for repeated calling when you simply cannot afford the
     copying cost of a FORK because you are using, say, a dozen
     gigabytes.

     Added CCL compiler-macros for IF and OR, to support some
     'coverage' analysis, cf. IF-REPORT, extending the profiling.

     Introduced the type 'mfixnum' so that things like counting honses
     and counting calls to memoized or profiled functions can run fast
     in CCL 64 bits and yet still run at all under 32 bits.

     Moved all HONSes to CCL's newish static space, which permits the
     address of a cons to be used as a hash key, as in most Lisps.
     (CCL moves most conses and most everything when it does a
     compacting-gc.)

     Quite a few changes in the memoize-fn reporting.

     Added a timer facility, cf. call-with-timeout.  Good for running
     under throttle some gross thoughts like 'Is it true that you can't
     fit 12 pigeons into 11 holes' on some propositional calculus
     systems/functions.

     Added rwx-size, pid-owner-cmdlines, rss, and proc-stat to help see
     what is really going on virtually in Gnu-Linux.

     Fixed at least one bug in compact-print-file and helped make its
     integration into ACL2's read-object$ a little more sound.  Still
     worried some about *print-readably* vs. readtable-case.  Does
     anyone else stay awake late at night worrying about readtable-case?

     Revised how the *watch-dog-process* interrupts the main process
     for the thousandth time, cf. watch.  Haven't changed it in weeks,
     which means that (a) it is getting tolerable or (b) I've run out
     of gas.

NOTE-3-6(R)    ACL2 Version  3.6(r) (August, 2009) Notes

Please also see NOTE-3-6 for changes in Version  3.6 of ACL2.

NOTE-3-6-1    ACL2 Version  3.6.1 (September, 2009) Notes

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

The essential changes to ACL2 since Version  3.6 are the two bug fixes
described below.  There was also some functionality-neutral code
refactoring, as requested by Daron Vroon in support of the ACL2 Sedan
(see ACL2-SEDAN).  Also see
`http://code.google.com/p/acl2-books/wiki/BooksSince36' for a list of
books in Version  3.6.1 of ACL2 but not Version  3.6.  For _changes_ to
existing books rather than _additions_, see the log entries at
`http://code.google.com/p/acl2-books/source/list' starting with
revision r329 up through revision 350.

Fixed a soundness bug in the handling of ruler-extenders, specifically
in the handling of LET-expressions.  Thanks to Pete Manolios, who sent
us a proof of nil, essentially as follows.  In the termination proof for
foo below, the binding of x to (cons t x) was not substituted into the
recursive call of foo for purposes of the termination proof.

     (defun foo (x)
       (declare (xargs :ruler-extenders :all))
       (let ((x (cons t x)))
         (if (endp (cdr x))
             x
           (cons t (foo (cdr x))))))

     (defthm foo-bad
       nil
       :hints (("Goal"
                :use ((:instance foo (x '(3))))
                :in-theory (disable foo (foo))))
       :rule-classes nil)

Fixed a typo in code supporting ruler-extenders (specifically, swapped
arguments in a recursive call of ACL2 source function
get-ruler-extenders2, which could cause problems for functions defined
using mutual-recursion).  Thanks to Daron Vroon for bringing this bug
to our attention, pointing out the swapped arguments.