Note-2-9-1
ACL2 Version 2.9.1 (December, 2004) 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 defcong specifies 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 symbol-package-name
above). Thanks to Dave Greve for sending a helpful example in his report of
this problem.
(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-Reina 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.
The function verbose-pstack has been enhanced to allow specified
prover functions not to be traced. See verbose-pstack.
Added lp, wet, and set-non-linearp to
*acl2-exports*, and hence to the "ACL2-user"
package.
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
bad-atom<=, 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 and 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 alphorder to require both
arguments to be atoms.
For forms (local x) that are skipped during include-book, or
during the second pass of certify-book or encapsulate, ACL2
had nevertheless checked that x is a legal event form. This is no longer
the case.
The proof-builder 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 {obsolete
after Version 4.3} 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 x bound to -1. While such matching
is sound, it leads to an infinite loop since it allows foo-axiom to
rewrite (foo 0) to (foo -1), and then (foo -1) to (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-count than 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))
Added macro find-lemmas in books/misc/find-lemmas.lisp (see 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
:restrict hints.
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,
formerly in books/finite-set-theory/osets-0.81/ but now in
books/finite-set-theory/osets/.
Fixed a bug in the (under-the-hood) raw Lisp definition of defchoose, which had been causing a warning in CMU Common Lisp.
[Technical improvements related to the use of ``make dependencies''
for certifying distributed books:]
File books/Makefile-generic
now does a better job with ``make dependencies,'' specifically with
respect to handling *.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 dependencies would generate the following line:
basic.cert: $(ACL2_SRC_BOOKS)/arithmetic/top-with-meta.cert
Thus, if :dir :system is used with include-book, the
corresponding Makefile should define the variable ACL2_SRC_BOOKS. A
standard Makefile header 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 = ../../../../../..
ACL2_SRC_BOOKS = $(ACL2_SRC)/books
include $(ACL2_SRC_BOOKS)/Makefile-generic
ACL2 = $(ACL2_SRC)/saved_acl2h
Finally, the ``-s'' flag may now be omitted when running ``make
dependencies.''
