This is documentation for ACL2 Version 3.0
Copyright (C) 2006  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-OTHER    ACL2 Version  2.7 Notes on Miscellaneous Changes

Made several minor documentation improvements.  We are grateful to Eric
Smith for suggesting (most of) these.

Improved (show-bdd) (see BDD) to give more useful feedback when
there are "leaf" terms not known to be Boolean.

Sped up processing of large mutual-recursion nests.  In one large
example the speedup was roughly two orders of magnitude.

Modified event printing so that if both 'prove and 'event are inhibited,
then events are no longer printed on behalf of certify-book,
encapsulate, or defstobj.  Thanks to Eric Smith for prompting
consideration of such a change.

The following technical change was made to support with-error-trace and
wet (see NOTE-2-7-NEW-FUNCTIONALITY), but may be of interest to
those who do low-level programming using the ACL2 logical world.  The
'unnormalized-body property is now stored not only for functions defined
in :logic mode, but also for functions defined by the user in :program
mode.  (:Program mode Functions built into ACL2 still have their
'unnormalized-body property omitted, in order to save space.)

The handling of "invisible" functions for purposes of controlling
rewriting (see LOOP-STOPPER) has been moved to a new table; see
INVISIBLE-FNS-TABLE.  Macros that access and modify this table
are called "...-invisible-fns-table" in place of their former names,
"...-invisible-fns-alist."  This feature was formerly implemented in the
acl2-defaults-table, which prevented a book from exporting lists of
invisible functions intended to work with the rewrite rules developed in
the book.  Thanks to Eric Smith and Rob Sumners for suggesting this
change.  See SET-INVISIBLE-FNS-TABLE (formerly
set-invisible-fns-alist), and also see ADD-INVISIBLE-FNS and see
REMOVE-INVISIBLE-FNS, which provides ways to incrementally add
to and remove from this table, respectively.  The handling of printing
binary function call nests using macros (See ADD-BINOP) has also
been moved out of the acl2-defaults-table as suggested by Eric and Rob,
but this feature didn't work anyhow (see NOTE-2-7-BUG-FIXES).
Incidentally, the symbols binop-table, add-binop, and remove-binop have
all been added to the list *acl2-exports* (see ACL2-USER),
add-invisible-fns and remove-invisible-fns have been added to that list,
and set-invisible-fns-alist has been replaced in that list by
set-invisible-fns-table.  Function invisible-fns-alistp is no longer
defined and has been removed from *acl2-exports*.

We now enforce the stated restriction on the pairings in
macro-aliases-table (see MACRO-ALIASES-TABLE), namely, that it
associates names of macros with names of funcions (with respect to the
current ACL2 logical world).  We make a similar requirement on
invisible-fns-table.

The theory-invariant event has been modified so that the default action
is an error rather than a warning.  Thanks to Eric Smith for suggesting
this change.  Also, the value returned upon successful execution of a
theory-invariant event is now the key.

Proof output that reports destructor elimination no longer uses the word
"generalizing".  This small change may help in browsing proof output,
since now "generaliz" takes you to true uses of generalization.  Thanks
to Matyas Sustik for suggesting such a change.

The command :pl now prints an abbreviated controller-alist for
;definition rules.  Formerly the output from :pl could be overwhelming
when the supplied function was part of a large mutual-recursion nest.

The defaults for keyword parameters of certify-book have changed.  See
NOTE-2-7-BUG-FIXES, in particular, the discussion there of two
modifications to certify-book.

Technical changes have been made to compress1 and compress2 that should
usually be invisible to users.  The next paragraph describes them in
detail, only for competeness (i.e., that description can be ignored by
most users).  But first, here is an example showing an effect on users.
The slow array warning was not there previously.  Notice that the
warning only arises if the event form is changed.  The solution is to be
sure that redundant defconst forms are syntactically identical.

     ACL2 !>(defconst *a* (compress1 'demo
                                     '((:header :dimensions (5)
                                                :maximum-length 15
                                                :default uninitialized
                                                :name demo)
                                       (1 . one)
                                       (0 . zero))))

     Summary
     Form:  ( DEFCONST *A* ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      *A*
     ACL2 !>(aref1 'demo *a* 0)
     ZERO
     ACL2 !>(defconst *a* (compress1 'demo
                                     '((:header :dimensions (5)
                                                :maximum-length 15
                                                :default uninitialized
                                                :name demo)
                                       (1 . one)
                                       (0 . zero))))

     This event is redundant.  See :DOC redundant-events.

     Summary
     Form:  ( DEFCONST *A* ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      :REDUNDANT
     ACL2 !>(aref1 'demo *a* 0)
     ZERO
     ACL2 !>(defconst *a* (compress1 'demo
                                     '((:header :dimensions (5)
                                                :maximum-length 15
                                                :default uninitialized
                                                :name demo)
                                       (0 . zero)
                                       (1 . one))))

     This event is redundant.  See :DOC redundant-events.

     Summary
     Form:  ( DEFCONST *A* ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      :REDUNDANT
     ACL2 !>(aref1 'demo *a* 0)

     **********************************************************
     Slow Array Access!  A call of AREF1 on an array named
     DEMO is being executed slowly.  See :DOC slow-array-warning
     **********************************************************

     ZERO
     ACL2 !>

As before, the von Neumann structure stored in the 'acl2-array property
of the array name contains the array list object in its car.  However,
previously it was the case that compress1 and compress2 did not update
that car when its new value would be equal to its old value.  This was
done largely in support of some type-set tables defined using defconst
in type-set-b.lisp.  The new versions of compress1 and compress2 are
simpler in that no such exception is made in the case of equal lists,
although instead the entire compression process is short-circuited when
the input array list object is eq to the car of the 'acl2-array
property.  This change was made because the equality test was causing a
"slow array access" warning to be printed in rare cases during proofs,
as described elswhere (see NOTE-2-7-BUG-FIXES).

We no longer distribute documentation specific to Lucid Emacs.  The Info
documentation in directory doc/EMACS/ works well both for Gnu Emacs and
XEmacs.

A little-advertised macro, value, has long been allowed for top-level
forms in books; see EMBEDDED-EVENT-FORM.  This has been replaced
by a new macro, value-triple.  The two have the same semantics at the
top-level of books, where state is "live".  However, value-triple should
be used at the top-level of a book, while value should be used in
function definitions (as before).  This change eliminates a warning put
out by the Allegro Common Lisp compiler for top-level value forms in
books.

NOTE-2-7-PROOF-CHECKER    ACL2 Version  2.7 Notes on Proof-checker Changes

Output from the proof-checker can now be inhibited by supplying the
symbol proof-checker in the list given to set-inhibit-output-lst.

NOTE-2-7-PROOFS    ACL2 Version  2.7 Notes on Changes in Proof Engine

An improvement in the linear arithmetic heuristics has been provided by
Robert Krug.  For information about this change, search for the comment
in add-linear-lemma (file rewrite.lisp) that begins as follows.

     ; Previous to Version_2.7, we just went ahead and used the result of

Thanks, Robert!  Also thanks to Eric Smith for providing a motivating
example.

The non-linear-arithmetic addition (see NON-LINEAR-ARITHMETIC)
led to several small changes in the linear-arithmetic decision procedure
(see LINEAR-ARITHMETIC).  Two of these changes could affect
existing proofs.

     First, when we are setting up the initial arithmetic data-base
     (which we call the "pot-lst"), we have always scanned it to see if
     there were any pairs of inequalities from which we could derive a
     previously unknown equality.  In some cases we added this equality
     to the clause and in others we used it to rewrite the clause,
     substituting one side of the equality for the other throughout the
     clause.  Previously, the heuristics that we used to determine
     whether we performed the substitution differed from those used in
     several other places in the code.  This has now been regularized,
     and similar heuristics are now used throughout the code.

     The second change to the linear-arithmetic decision procedure is
     that we now explicitly add inequalities derived from type reasoning
     to the pot-lst.  Previously, we performed cancellations against
     these inequalities without adding them to the pot-lst.  This change
     results in there being more inequalities in the pot-lst than
     before, and so more chances for there to be a pair of inequalities
     from which an equality can be derived.  In effect, certain simple
     consequences of the current goal (see TYPE-SET) may now be
     added as hypotheses of the goal or used to peform equality
     substitutions.

A slight improvement has been made to the way certain rewrite rules are
stored.  It was already the case that a rewrite rule rule whose
conclusion C is not a call of a known equivalence relation (or eq, eql,
or =) is stored as (iff C t), except that if ACL2 can determine (using
its type-set mechanism) that C is Boolean, then the rule is stored as
(equal C t).  The iprovement is that if C and C' are Boolean, then a
rule stated as (iff C C') is stored as (equal C C').  Thanks to Pete
Manolios for providing an example that led us to consider this
improvement.

The heuristic use of equalities (fertilization) has been modified.
Previously, ACL2 would sometimes substitute using an equality but keep
the equality, and then undo the substitution by using the equality
again.  Now, when ACL2 keeps an equality after using it, it puts the
equality inside a call of hide.  Descendents of that goal that are
unchanged by simplification will have this call of hide removed so that
the equality can once again contribute to the proof.  This change can
cause some proofs to succeed that otherwise would fail.  In the unlikely
event that a proof fails that formerly succeeded, the following hint on
"Goal" may fix the problem (see HINTS):

     :expand ((:free (x) (hide x)))

We have refined the heuristics employed when an IF form is assumed true
or false.  Our previous attempt (see note-2-6-proofs for the original
announcement) was not as general as we had believed.  We have also
improved some low-level code responsible for rewriting IF expressions.
In earlier versions of ACL2, it was possible to have the truth or
falsity of an IF expression explicitly recorded in the type-alist, and
yet not use this information during rewriting.  This problem has been
corrected.  Thanks to Robert Krug for noticing this problem and
implementing the fix.

We have sped up the rewriter in some cases where there are large
collections of mutually-recursive functions (see
MUTUAL-RECURSION).  (Implementation notes: technically, we have
modified the way function being-openedp operates on the fnstack, and we
have modified *current-acl2-world-key-ordering* as described in the
essay above its definition.)

Forward-chaining is now done in the preprocessing phase of proof
attempts (see the discussion of :DO-NOT -- see HINTS).  This is
part of a technical change, made in support of translation of type
declarations to guards (see NOTE-2-7-GUARDS).  Previously,
whenever ACL2 checked for built-in-clauses, it then looked for a
contradiction using type-set reasoning if it did not find a suitable
built-in clause.  The change is to perform forward-chaining in such
cases (i.e., when a built-in clause is not found).

A couple of changes have been made in the generation of goals for
forcing-rounds.  Thanks to Eric Smith for bringing issues to our
attention that led to these changes.  For one, guards are no longer
relevant in such goal generation.  Formerly, the addition of a guard
could make a proof fail that otherwise succeeded.  Secondly, contextual
information is now always kept when it involves a constrained constant,
i.e., a zero-ary function introduced in the signature of an encapsulate.

NOTE-2-7-RULES    ACL2 Version  2.7 Notes on Changes in Rules and Constants

The defcong macro has been slightly changed.  The difference is that the
variable generated with suffix -EQUIV will now be in the same package as
the name of the variable from which it is generated, rather than always
belonging to the ACL2 package.  Thanks to Hanbing Liu for suggesting
this change.  (Note that a couple of books have been modified to
accommodate this change, e.g., books/finite-set-theory/set-theory.)

In Version_2.6, a change was made for rules of class :rewrite whose
conclusion is a term of the form (EQV lhs rhs), where EQV is =, eq, or
eql: the rule was stored as though EQV were equal.  (See
NOTE-2-6-RULES.)  This change has been extended to rules of class
:definition.

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 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-OTHERfor 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.