Major Section: RELEASE-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.
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
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
Made a change to allow
(time$ FORM) and
(with-prover-time-limit TIME FORM) when
make-event calls that change the ACL2 world. Thanks to Jared
Davis for requesting such support for
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
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
that directory for simple examples.
o The hint
:OR (hints-1 ... hints-k)causes an attempt to prove the specified goal using each
hints-iin 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
:CONSIDERhint implemented in distributed book
books/hints/consider-hint.lisp. With this hint, you can for example give the equivalent of a
:USEhint without the need to supply an instantiation. Include that book in order to see documentation online with
:doc consideration, and see the book
A new hint,
reorder, allows the specification of which subgoals
are to be considered first. Thanks to Sandip Ray for putting forward this
set-saved-output by supporting a second argument of
which avoids changing which output is inhibited.
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
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
Sandip Ray has contributed a book,
provides a collection of macros to aid in reasoning about ACL2 functions via
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
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-soft-right-margin are not alone sufficient to extend the right
margin in all cases.
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
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.
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
pr for displaying rules of class
meta. Thanks to Jared Davis for finding this bug and providing a
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-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
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
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
now prints ``
***'' regardless of the current package.
Fixed a bug that allowed
certify-book to succeed without specifying
t for keyword argument
:skip-proofs-okp, even with
include-book events in the certification world depending on
events executed under
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.
:framesreported for a rule are categorized as ``useful'' and ``useless'' according to whether they support ``useful'' or ``useless''
:triesof that rule, respectively. See accumulated-persistence for further explanation.
make-event so that the reported time and warnings include
those from the expansion phase. In analogy with
progn, the rules reported still do not include those from subsidiary
events (including the expansion phase). A related change to
resetting summary information (time, warnings) with each top-level form
evaluation; events already handle this information themselves.
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.
doc/HTML/ now again includes installation instructions
(which was missing in Version_3.2.1), in
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-lsthas been called with argument
o Fixed a bug in Xemacs support for proof-tree help keys
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).
:load-compiled-file argument of a call of
: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
Fixed a bug that was avoiding compilation of some executable counterparts
(sometimes called ``*1* functions'') during
certify-book, and also
:load-compiled-file value of
: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
note-3-3 in the ACL2 source code.
o Reduced the size of
.certfiles by eliminating some unnecessary
defpkgevents 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-bookcaused by a subtle interaction between
defpkgevents 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
Improved ACL2's heuristics for relieving hypotheses, primarily to use linear
reasoning on conjuncts and disjuncts of the test of an
For example, given a hypothesis of the form
(if (or term1 term2) ...),
ACL2 will now use linear reasoning to attempt to prove both
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
mv-let subterms (i.e.
lambda subterms) rewrites to
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.
Added documentation on how to use
make-event to avoid duplicating
expensive computations, thanks to Jared Davis.
Modified the error message for calls of undefined functions to show the arguments. Thanks to Bob Boyer for requesting this enhancement.
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
o An additional rewrite stack entry is made when entering non-linear arithmetic (see non-linear-arithmetic).
ADD-POLYNOMIAL-INEQUALITIESentry is printed with a counter, to show how often this process is called.
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.
make-event expansion so that changes to
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
Output from the proof-checker is now always enabled when invoking
verify, even if it is globally inhibited
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
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
(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
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.