This is documentation for ACL2 Version 3.4
Copyright (C) 2008  University of Texas at Austin

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

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

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

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

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

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

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

*NEW FEATURES*

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

     o C-z o      Switch to another frame

     o C-z b      Switch to prooftree buffer

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

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

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

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

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

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

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

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

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

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

*BUG FIXES*

Fixed defstobj to inhibit a potentially useless theory warning.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Some fixes have been made for proof-tree support.

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

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

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

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

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

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

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

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

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

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

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

*PROVER ALGORITHM ENHANCEMENTS*

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

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

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

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

*MISCELLANEOUS*

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

NOTE-3-3(R)    ACL2 Version  3.3(r) (xxx, 20xx) Notes

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

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

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

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

*CHANGES TO EXISTING FEATURES*

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

*NEW FEATURES*

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

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

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

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

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

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

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

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

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

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

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

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

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

We now allow arbitrary packages in raw mode (see SET-RAW-MODE)
-- thanks to Jared Davis for requesting this enhancement -- and more
than that, we allow arbitrary Common Lisp in raw mode.

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

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

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

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

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

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

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

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

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

*BUG FIXES*

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

*NEW AND UPDATED BOOKS*

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

*EMACS SUPPORT*

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

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

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

NOTE-3-4(R)    ACL2 Version  3.4(r) (xxx, 20xx) Notes

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

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

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.