ACL2 Version 2.8 Notes on Bug Fixes
We have fixed a soundness bug in the tautology checker's handling
of expressions of the form
The preceding version (2.7) introduced a soundness bug in handling of ACL2
arrays, in which functions compress1 and compress2 were
returning the input alist rather than compressing it appropriately. Here is a
proof of
(defthm bad (not (let* ((ar2 (aset1 'my-array ar1 3 10)) (ar3 (compress1 'my-array ar2)) (ar4 (reverse (reverse ar2))) (ar5 (compress1 'my-array ar4))) (and (equal ar2 ar4) (not (equal ar3 ar5))))) :rule-classes nil) (defthm contradiction nil :rule-classes nil :hints (("Goal" :use ((:instance bad (ar1 (compress1 'my-array '((3 . 5) (:HEADER :DIMENSIONS (5) :MAXIMUM-LENGTH 6 :DEFAULT 0 :NAME MY-ARRAY)))))))))
On a related note, a new function flush-compress can be used for subtle control of under-the-hood raw Lisp support for fast array access, although we expect it to be very rare that users need this extra support.
Previous versions have had two soundness bugs that can occur when using the proof-builder:
A soundness bug could be provoked in some Lisps by applying defpkg to the empty string. This has been disallowed.
We fixed a soundness bug related to packages caused by a failure to track axioms introduced locally on behalf of defpkg events. See hidden-death-package.
We fixed a soundness bug caused by a failure to check that a
We fixed a potential soundness bug relating to reclassifying a
It was possible to get a raw Lisp error by introducing a locally defined function with guard verification inhibited and then subsequently introducing the same definition non-locally without that inhibition. The following example will clarify.
(encapsulate nil (local (defun foo (x) (declare (xargs :guard t :verify-guards nil)) (car x))) (defun foo (x) (declare (xargs :guard t)) (car x))) ; The following causes a raw lisp error because ACL2 runs the Common Lisp ; definition of foo, because it thinks that foo's guard of t was verified. (thm (equal (foo 3) xxx))
Thanks to Jared Davis for bringing this problem to our attention. We are
particularly grateful to Jared because his example exploited this bug by
applying it to a function defined using mbe (introduced in this same
version, 2.8), in order to prove
The sort of error message shown below can legitimately occur when certifying a book in a certification world where there was an include-book command with a relative pathname (see pathname). However, it was occurring more often than necessary. This has been fixed.
ACL2 Error in (CERTIFY-BOOK "foo" ...): The certification world has include-book commands for book "bar" that correspond to different full pathnames, namely "/u/dir1/bar" and "/u/dir2/bar". ACL2 cannot currently certify a book in such a world. To work around this problem, use an absolute pathname for at least one of these books (see :DOC pathname).
Bugs were fixed in with-output, in particular related to the use of
values
Fixed a lisp error occurring when
We added an appropriate guard to find-rules-of-rune, which will avoid hard lisp errors when this function is called on non-rune arguments. Thanks to Eric Smith for pointing out this issue.
It was possible for a redundant include-book form (see redundant-events) to leave a command in the ACL2 logical world
and to cause (re-)loading of a compiled file. These behaviors have been
fixed. In particular, if
The summary printed at the end of a proof had not listed
The use of proof trees in emacs redefined `
Source function
A number of proof-builder atomic macros caused a hard error when all goals have already been proved. This has been fixed. Thanks to John Erickson for sending an example of the issue.
A bug has been fixed in add-match-free-override. Formerly, a
table guard violation occurred when calling add-match-free-override more than once with first argument other than
Definitions of functions involving large constants could cause stack
overflows. This has been fixed, at least in some of the most egregious cases
(by making a source function
Evaluation of computed hints could cause stack overflows. This has been fixed. Thanks to Eric Smith for bringing this problem to our attention.
Evaluation of
Fixed a bug in
Duplicate rule names have been eliminated from warnings generated upon the
use of enabled
The trace utilities (see trace), as modified for GCL and Allegro
Common Lisp, had failed to show more than the first return value for so-called
``
Uses of hide introduced during proofs by failed attempts to
evaluate constrained functions (see hide) are now tracked, so that the
rune
The following bug, introduced back in Version 2.7, has been fixed. The bug
applied only to GCL and may well not have affected anyone. But the function
proclamation computed by ACL2 for compilation usually had an output type of
The macro gc$ had a bug exhibited when it was supplied one or more arguments. This has been fixed.
The macro defabbrev broke when supplied a string and no
documentation, e.g.,
For ACL2 executables built on Allegro Common Lisp, a Lisp error occurred when trace$ was called on other than a defined function symbol. Now ACL2 prints a more useful error message.
The proof-builder no longer accepts a
The function
The handling of free variables in hypotheses (see free-variables) of
rewrite and linear rules had a bug that prevented some proofs from going
through. Here is a simple example, essentially provided by Diana Moisuc, who
we thank for bringing this issue to our attention. The proof of the thm below had failed, but now will succeed. This particular bug prevented,
for example, the
(defstub foo1 (* ) => *) (skip-proofs (defthm aux-foo1 (implies (and (integerp a) (integerp i) (equal (foo1 0) (list 0 i))) (equal (foo1 a) (list 0 (+ a i)))) :rule-classes ((:rewrite :match-free :all)))) (thm (implies (and (integerp i) (integerp a) (equal (foo1 0) (list 0 i))) (equal (foo1 a) (list 0 (+ a i)))))
Formerly, creation of large arrays could cause an error in the underlying
Common Lisp implementation without helpful messages for the user. Now, we
check Common Lisp restrictions on arrays and print a helpful error message if
they are violated, namely: each dimension must be less than the value of
Common Lisp constant
The default-hints in the current logical world were ignored by verify-guards. This has been fixed. Thanks to Jared Davis for pointing out this bug and sending a helpful example.
The brr mechanism has been cleaned up in order to avoid hard errors
and infinite loops that can arrive when typing interrupts (
We have eliminated structural flaws in the HTML documentation pages that could make them unreadable in some browsers. Thanks to Bill Young for bringing this issue to our attention and to Joe Hendrix for diagnosing the problem.
The proof-builder could run very slowly after many instructions in a given session. This has been fixed; thanks to Art Flatau for bringing this problem to our attention. (Implementation detail: We now keep tag-trees duplicate-free when we accumulate them into state. This change could have minor speed advantages for some top-level proofs too, not just in the proof-builder.)
The printing of accesses to stobjs using nth or update-nth has been done using symbolic constants since ACL2 Version_2.6. However, there was a bug that prevented this feature from working for update-nth except at a top-level call. This has been fixed. Thanks to Julien Schmaltz for bringing this problem to our attention. For example, consider these events:
(defstobj st field0 field1) (thm (equal (nth 1 (update-nth 0 17 st)) (car (cons xxx yyy))) :hints (("Goal" :in-theory (disable nth update-nth))))
Before the fix, the proof attempt of the above silly thm printed the following.
(NTH 1 (UPDATE-NTH *FIELD0* 17 ST))
After the fix, we instead see the following.
(NTH *FIELD1* (UPDATE-NTH *FIELD0* 17 ST))
It is now possible to certify and subsequently include books that
require guard-checking to be off. For example, the book can contain the form
Fixed a proof-builder bug that could cause probably cause strange error, ``Attempt to access the plist field''. Thanks to Bill Young for bringing this problem to our attention.
Fixed a proof-builder bug that was failing to record applications of
rewrite rules using the proof-builder's
Modernized some of the proof-tree emacs and infix printing stuff, thanks to suggestions made by Camm Maguire.