ACL2 Wizard's Workshop. March 29-31, 1999. University of Texas at Austin.
ACL2 Version 2.3 (and earlier versions back to 2.1) has a soundness bug! The
bug may bite if the system applies a rule with a forced hypothesis while the
rune (:EXECUTABLE-COUNTERPART IMMEDIATE-FORCE-MODEP) is enabled.
The rune just mentioned controls the ``immediate forcing'' feature, which is
supposed to make ACL2 immediately attack unrelieved forced hypotheses instead
of delaying them until the end of the proof. The bug causes ACL2 to ignore
such hypotheses altogether! The rune may be enabled inadvertently by enabling
the ``universal theory'' or some user defined theory that includes that rune.
Rewrite rules with forced hypotheses occur in several of our distributed
books, including structures.lisp and the ihs books.
We recommend that you load the following patch into the raw Lisp under ACL2
(i.e., exit the ACL2 command loop with :q, define and compile
the function as shown below, and reenter the loop with (LP)).
(compile
(defun immediate-forcep (fn ens)
(cond ((eq fn 'case-split) 'case-split)
((enabled-numep *immediate-force-modep-xnume* ens) t)
(t nil))))
We are truly sorry and embarrassed by this bug and apologize to our users
for it. Please let us know if this affects any of the proofs you've
depended on. We know that the books we distribute with ACL2, our AMD K5
division proof, and Russinoff's floating point library (below) are not
affected.
Bill Schelter reports that GCL 2.3 had a change in it that caused trouble for ACL2: si::break-call took three arguments in GCL 2.3 but only two in GCL 2.2. He has changed GCL 2.3 to support both. But ACL2 users running gcl-2.3-beta.tgz should load the following redefine:
top.lsp:
(in-package 'system)
(defun break-call (key args &optional (prop 'si::break-command) &aux fun)
(setq fun (complete-prop key 'keyword prop))
(or fun (return-from break-call nil))
(setq fun (get fun prop))
(if fun
(evalhook (cons fun args) nil nil *break-env*)
(format *debug-io* "~&~S is undefined break command.~%" key)))
It has been brought to our attention that the demise of Computational Logic, Inc., has caused some potential users to shy away from ACL2 because of the fear that it would not be maintained. Don't worry about that. The ``Boyer-Moore'' theorem prover has been maintained by its two authors (with the help of a dedicated user community) for a quarter of a century without any formal organization behind it. Indeed, that personal stake in the ``product'' is part of the reason Nqthm is rugged and reliable. Matt Kaufmann and I have brought the same dedication and commitment to ACL2 (which celebrates its 9th birthday on August 14, 1998.) We have been lucky to have inherited many Nqthm users with their high expectations of reliability. We see no reason why ACL2 will not continue to be maintained. There are many reasons not to choose ACL2 as your theorem prover -- its relatively weak logic, its style of user interaction, its syntax, etc., -- but its continued maintenance is not among them.