Major Section: RELEASE-NOTES
(GCL only) A bug in
symbol-package-name has been fixed that could be
exploited to prove
nil, and hence is a soundness bug. Thanks to Dave
Greve for sending us an example of a problem with
defcong (see below)
that led us to this discovery.
ACL2 now warns when
equal as the first
equivalence relation, e.g.,
(defcong equal iff (member x y) 2). The
warning says that the rule has no effect because
equal already refines
all other equivalence relations. Formerly, this caused an error unless
:event-name was supplied (see defcong), and in fact the error was a
nasty raw Lisp error on GCL platforms due to some mishandling of packages by
ACL2 that has been fixed (see the paragraph about
above). Thanks to Dave Greve for sending a helpful example in his report of
(GCL only) The build process was broken for GCL 2.6.0 (and perhaps some earlier versions), and has been fixed. Thanks to Jose Luis Ruiz-Reyna for bringing this problem to our attention.
(GCL only) We have increased the hole size to at least 20% of max-pages, which may eliminate some garbage collection at the expense of larger virtual memory (not larger resident memory or larger image). Thanks to Camm Maguire for helpful explanations on this topic.
We have clarified the guard warning message that is printed during evaluation of recursively-defined functions whose guards have not been verified, for example:
ACL2 Warning [Guards] in TOP-LEVEL: Guard-checking may be inhibited on some recursive calls of executable counterparts (i.e., in the ACL2 logic), including perhaps EVENLP. To check guards on all recursive calls: (set-guard-checking :all) To leave behavior unchanged except for inhibiting this message: (set-guard-checking :nowarn)And, ACL2 no longer prints that message when the guard was unspecified for the function or was specified as
T. Thanks to Serita Nelesen for bringing the latter issue to our attention. Finally, ACL2 now prints such a warning at most once during the evaluation of any top-level form; thanks to Bill Young for pointing out this issue.
verbose-pstack has been enhanced to allow specified prover
functions not to be traced. See verbose-pstack.
and hence to the
The distributed book
books/arithmetic-3/bind-free/integerp.lisp has been modified in order to prevent
potential looping; specifically, the definition of function
reduce-integerp-+-fn-1. Thanks to Robert Krug for providing this change.
A small improvement was made in the
wet failure message when the error
occurs during translation to internal form. Thanks to Jared Davis for
pointing out the obscurity of some
wet error messages.
We have improved ACL2's evaluation mechanism for the function
which now is specified to return
nil if neither argument is a so-called
``bad atom'' (as recognized by function
bad-atom). The following events
had caused a hard error, for example. (We're sorry that
bad-atom<= are not documented, but we also consider it unlikely that
anyone needs such documentation; otherwise, please contact the implementors.)
(defun foo (x y) (declare (xargs :guard t)) (bad-atom<= x y)) (defun bar (x y) (declare (xargs :guard t)) (foo x y)) (thm (equal (bar 3 4) 7))We have also changed the guard on
alphorderto require both arguments to be atoms.
(local x) that are skipped during
include-book, or during
the second pass of
encapsulate, ACL2 had
nevertheless checked that
x is a legal event form. This is no longer the
The proof-checker now does non-linear arithmetic when appropriate. It
had formerly ignored
set-non-linearp executed in the ACL2 command loop.
Incremental releases are now supported. See version and see set-tainted-okp. Thanks to Hanbing Liu for discovering a flaw in our original design.
The pattern-matching algorithm for
rewrite rules has been made
slightly more restrictive, thanks to a suggestion and examples from Robert
Krug. For example, previously one could get an infinite loop as follows.
(defstub foo (x) t) (defaxiom foo-axiom (equal (foo (+ 1 x)) (foo x))) (thm (foo 0)) ; or replace 0 by any integer!That is because the term
(foo 0)was considered to match against the pattern
(foo (+ 1 x)), with
-1. While such matching is sound, it leads to an infinite loop since it allows
(foo -1), and then
(foo -2), and so on. The fix is to insist that the new value, in this case
-1, is no larger in size according to
acl2-countthan the old value, in this case
0. Since that test fails, the match is considered to fail and the loop no longer occurs. An analogous fix has been made for multiplication, where now we only match when the new term is still a non-zero integer. That change avoids a loop here.
(defstub foo (x) t) (defaxiom foo-axiom (equal (foo (* 2 x)) (foo x))) (thm (foo 0)) ; or try (thm (foo 4))
brief documentation there) for finding all lemmas that mention all function
symbols in a given list.
:Restrict hints now work for
definition rules, though
they continue to be ignored by the preprocessor and hence you may want to use
:do-not '(preprocess) with any restrict hints. Thanks to John Matthews
for pointing out the lack of support for
:definition rules in
Some books have been updated. In particular, there is a new directory
books/workshops/2004/ in workshops distribution, for the 2004 ACL2
workshop. There is also a new version of Jared Davis's ordered sets library,
books/finite-set-theory/osets-0.81/ but now in
Fixed a bug in the (under-the-hood) raw Lisp definition of
which had been causing a warning in CMU Common Lisp.
[Technical improvements related to the use of ``
make dependencies'' for
certifying distributed books:]
books/Makefile-generic now does a
better job with ``
make dependencies,'' specifically with respect to
*.acl2 files and handling
include-book commands with
:dir :system. Regarding the latter, suppose for example that book
basic.lisp contains the line:
(include-book "arithmetic/top-with-meta" :dir :system)Then
make dependencieswould generate the following line:
basic.cert: $(ACL2_SRC_BOOKS)/arithmetic/top-with-meta.certThus, if
:dir :systemis used with
include-book, the corresponding
Makefileshould define the variable
ACL2_SRC_BOOKS. A standard
Makefileheader for a books directory could thus be as follows.
# The following variable should represent the ACL2 source directory. It is the # only variable in this Makefile that may need to be edited. ACL2_SRC = ../../../../../..Finally, the ``
ACL2_SRC_BOOKS = $(ACL2_SRC)/books include $(ACL2_SRC_BOOKS)/Makefile-generic ACL2 = $(ACL2_SRC)/saved_acl2
-s'' flag may now be omitted when running ``