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-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 (see 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 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.  See WET.  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 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 foo (x) x)
            (my-defun g (x) (foo 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-METAFUNCTIONSand 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.

NOTE1    Acl2 Version 1.1 Notes

The new features are extensively documented.  The relevant topics are:

Related topics other than immediate subtopics:

It is especially important to read all of of the documentation for books
before trying to use books.  However, the new :more keyword command is
so handy for reading long documentation strings that we recommend you
start with :doc more if reading at the terminal.  Some documentation has
been written for guards which you might find interesting.

NOTE2    Acl2 Version 1.2 Notes

Hacker mode has been eliminated and programming mode has been added.
Programming mode is unsound but does syntax checking and permits
redefinitions of names.  See :doc load-mode and :doc g-mode.

The arguments to ld have changed.  Ld is now much more sophisticated.
See LD.

For those occasions on which you wish to look at a large list structure
that you are afraid to print, try (walkabout x state), where x is an
Acl2 expression that evaluates to the structure in question.  I am
afraid there is no documentation yet, but it is similar in spirit to the
Interlisp structure editor.  You are standing on an object and commands
move you around in it.  E.g., 1 moves you to its first element, 2 to its
second, etc.; 0 moves you up to its parent; nx and bk move you to its
next sibling and previous sibling; pp prettyprints it; q exits returning
nil; = exits returning the thing you're standing on; (= symb) assigns
the thing you're standing on to the state global variable symb.

Several new hints have been implemented, including :by and :do-not.  The
old :do-not-generalize has been scrapped in favor of such new hints as
:do-not (generalize elim).  :By lets you say "this goal is subsumed by"
a given lemma instance.  The :by hint also lets you say "this goal can't
be proved yet but skip it and see how the rest of the proof goes." See
HINTS.

NOTE3    Acl2 Version 1.3 Notes

Programming mode has been eliminated.  Instead, all functions have a
"color" which indicates what can be done with the function.  For
example, :red functions can be executed but have no axioms describing
them.  Thus, :red functions can be introduced after passing a simple
syntactic check and they can be redefined without undoing.  But nothing
of consequence can be proved about them.  At the other extreme are :gold
functions which can be executed and which also have passed both the
termination and the guard verification proofs.  The color of a function
can be specified with the new xargs keyword, :color, which, if omitted
defaults to the global setting of ld-color.  Ld-color replaces
load-mode.  Setting ld-color to :red causes behavior similar to the old
:g-mode.  Setting ld-color to :gold causes behavior similar to the old
:v-mode.  It is possible to prototype your system in :red and then
convert :red functions to :blue individually by calling
verify-termination on them.  They can then be converted to :gold with
verify-guards.  This allows us to undertake to verify the termination
and guards of system functions.  See :doc color for an introduction to
the use of colors.

Type prescription rules have been added.  Recall that in Nqthm, some
rewrite rules were actually stored as "type-prescriptions."  Such rules
allow the user to inform Nqthm's primitive type mechanism as to the
kinds of shells returned by a function.  Earlier versions of Acl2 did
not have an analogous kind of rule because Acl2's type mechanism is
complicated by guards.  Version 1.3 supports type-prescription rules.
See TYPE-PRESCRIPTION.

Three more new rule-classes implement congruence-based rewriting.  It is
possible to identify a binary relation as an equivalence relation (see
EQUIVALENCE), to show that one equivalence relation refines
another (see REFINEMENT) and to show that a given equivalence
relation is maintained when rewriting a given function call, e.g., (fn
...xk...), by maintaining another equivalence relation while rewriting
the kth argument (see CONGRUENCE).  If r has been shown to be an
equivalence relation and then (implies hyps (r (foo x) (bar x))) is
proved as a :rewrite rule, then instances of (foo x) will be replaced by
corresponding instances of (bar x) provided the instance occurs in a
slot where the maintainence of r-equivalence is known to be sufficient
and hyps can be established as usual.

In Version 1.2, rule-classes were simple keywords, e.g., :rewrite or
:elim.  In Version 1.3, rule-classes have been elaborated to allow you
to specify how the theorem ought to be used as a rule.  That is, the new
rule-classes allows you to separate the mathematical statement of the
formula from its interpretation as a rule.  See RULE-CLASSES.

Rules used to be named by symbols, e.g., car and car-cons were the names
of rules.  Unfortunately, this was ambiguous because there are three
rules associated with function symbols: the symbolic definition, the
executable counterpart, and the type-prescription; many different rules
might be associated with theorems, depending on the rule classes.  In
Version 1.3 rules are named by "runes" (which is just short hand for
"rule names").  Example runes are (:definition car),
(:executable-counterpart car), and (:type-prescription car . 1).  Every
rule added by an event has a different name and you can enable and
disable them independently.  See RUNE and see THEORIES.

The identity function force, of one argument, has been added and given a
special interpretation by the functions responsible for establishing
hypotheses in backchaining: When the system fails to establish some
hypothesis of the form (force term), it simply assumes it is true and
goes on, delaying until later the establishment of term.  In particular,
pushes a new subgoal to prove term in the current context.  When that
subgoal is attacked, all of the resources of the theorem prover, not
just rewriting, are brought to bear.  Thus, for example, if you wish to
prove the rule (implies (good-statep s) (equal (exec s n) s')) and it is
your expectation that every time exec appears its first argument is a
good-statep then you might write the rule as (implies (force
(good-statep s)) (equal (exec s n) s')).  This rule is essentially an
unconditional rewrite of (exec s n) to s' that spawns the new goal
(good-statep s).  See FORCE.  Because you can now specify
independently how a theorem is used as a rule, you need not write the
force in the actual theorem proved.  See RULE-CLASSES.

Version 1.3 supports a facility similar to Nqthm's break-lemma.  See
BREAK-REWRITE.  You can install "monitors" on runes that will
cause interactive breaks under certain conditions.

Acl2 also provides "wormholes" which allow you to write functions that
cause interaction with the user but which do not require that you have
access to state.  See WORMHOLE.

The rewriter now automatically backchains to stronger recognizers.
There is no user hook to this feature but it may simplify some proofs
with which older versions of Acl2 had trouble.  For example, if the
rewriter is trying to prove (rationalp (foo a b c)) it is now smart
enough to try lemmas that match with (integerp (foo a b c)).

NOTE4    Acl2 Version 1.4 Notes

Once again ld only takes one required argument, as the bind-flg has been
deleted.

Three commands have been added in the spirit of :pe.  :Pe! is similar to
:pe but it prints all events with the given name, rather than just the
most recent.  The command :pf prints the corollary formula corresponding
to a name or rune.  The command :pl (print lemmas) prints rules whose
top function symbol is the given name.  See PE!, see PF,
and see PL.

Book naming conventions have been changed somewhat.  The once-required
.lisp extension is now prohibited!  Directories are supported, including
a notion of "connected book directory".  See BOOK-NAME.  Also,
the second argument of certify-book is now optional, defaulting to 0.

Compilation is now supported inside the Acl2 loop.  See COMPand
see SET-COMPILE-FNS.

The default color is now part of the Acl2 world; see :doc default-color.
Ld-color is no longer an ld special.  Instead, colors are events; see
the documentation for red, pink, blue, and gold.

A table exists for controlling whether Acl2 prints comments when it
forces hypotheses of rules; see :doc force-table.  Also, it is now
possible to turn off the forcing of assumptions by disabling the
definition of force; see FORCE.

The event defconstant is no longer supported, but a very similar event,
defconst, has been provided in its place.  See DEFCONST.

The event for defining congruence relations is now defcong (formerly,
defcon).

Patterns are now allowed in :expand hints.  See the documentation for
:expand inside the documentation for hints.

We have improved the way we report rules used by the simplifier.  All
runes of the same type are reported together in the running commentary
associated with each goal, so that for example, executable counterparts
are listed separately from definitions, and rewrite rules are listed
separately from linear rules.  The preprocessor now mentions "simple"
rules; see SIMPLE.

The mechanism for printing warning messages for new rewrite rules,
related to subsumption, now avoids worrying about nonrecursive function
symbols when those symbols are disabled.  These messages have also been
eliminated for the case where the old rule is a :definition rule.

Backquote has been modified so that it can usually provide predictable
results when used on the left side of a rewrite rule.

Time statistics are now printed even when an event fails.

The Acl2 trace package has been modified so that it prints using the
values of the Lisp globals *print-level* and *print-length*
(respectively).

Table has been modified so that the :clear option lets you replace the
entire table with one that satisfies the val and key guards (if any);
see TABLE.

We have relaxed the translation rules for :measure hints to defun, so
that the the same rules apply to these terms that apply to terms in
defthm events.  In particular, in :measure hints mv is treated just like
list, and state receives no special handling.

The loop-stopper test has been relaxed.  The old test required that
every new argument be strictly less than the corresponding old argument
in a certain term-order.  The new test uses a lexicographic order on
term lists instead.  For example, consider the following rewrite rule.

       (equal
        (variable-update var1
                         val1 (variable-update var2 val2 vs))
        (variable-update var2
                         val2 (variable-update var1 val1 vs)))

This rule is permutative.  Now imagine that we want to apply this rule
to the term

       (variable-update u y (variable-update u x vs)).

Since the actual corresponding to both var1 and var2 is u, which is not
strictly less than itself in the term-order, this rule would fail to be
applied in this situation when using the old test.  However, since the
pair (u x) is lexicographically less than the pair (u y) with respect to
our term-order, the rule is in fact applied using our new test.

Messages about events now contain a space after certain left
parentheses, in order to assist emacs users.  For example, the event

       (defthm abc (equal (+ (len x) 0) (len x)))

leads to a summary containing the line

       Form:  ( DEFTHM ABC ...)

and hence, if you search backwards for "(defthm abc", you won't stop at
this message.

More tautology checking is done during a proof; in fact, no goal printed
to the screen, except for the results of applying :use and :by hints or
the top-level goals from an induction proof, are known to Acl2 to be
tautologies.

The ld-query-control-alist may now be used to suppress printing of
queries; see LD-QUERY-CONTROL-ALIST.

Warning messages are printed with short summary strings, for example the
string "Use" in the following message.

       Acl2 Warning [Use] in DEFTHM:  It is unusual to :USE an enabled
       :REWRITE or :DEFINITION rule, so you may want to consider
       disabling FOO.

At the end of the event, just before the time is printed, all such
summary strings are printed out.

The keyword command :u has been introduced as an abbreviation for :ubt
:max.  Printing of query messages is suppressed by :u.

The keyword :cheat is no longer supported by any event form.

Some irrelevant formals are detected; see IRRELEVANT-FORMALS.

A bug in the application of metafunctions was fixed: now if the output
of a metafunction is equal to its input, the application of the
metafunction is deemed unsuccessful and the next metafunction is tried.

An example has been added to the documentation for equivalence to
suggest how to make use of equivalence relations in rewriting.

The following Common Lisp functions have been added to Acl2:
alpha-char-p, upper-case-p, lower-case-p, char-upcase, char-downcase,
string-downcase, string-upcase, and digit-charp-p.

A documentation section called proof-checker has been added for the
interactive facility, whose documentation has been slightly improved.
See in particular the documentation for proof-checker, verify, and
macro-command.

A number of events that had been inadvertently disallowed in books are
now permitted in books.  These are: defcong, defcor, defequiv,
defrefinement, defstub, and verify-termination.