ACL2 Version 2.5 (June, 2000) Notes
Concurrent with the release of ACL2 Version 2.5 is the publication of two books about ACL2. See the ``Books and Papers about ACL2 and Its Applications'' on the ACL2 Home Page.
The list of symbols in
Include-book and certify-book were modified to have some
additional keyword arguments. It is possible to certify a book containing
defaxiom and/or skip-proofs events and get warning messages or
errors signaled, according to the settings of these new flags. In addition,
it is possible to specify in
The above change involved altering the form of certificate files. When
books certified under previous versions are included, more warnings will be
generated because these books are considered possibly to contain
We anticipate further changes to this aspect of books and consider the current mechanisms (for controlling whether warnings or errors are signaled) just a prototype. See also the discussion below of ``soundness related'' warnings. Your suggestions are welcome.
A discrepancy between ACL2 and Common Lisp was fixed, having to do with
ACL2 can now be built in releases 5.0 and later of Allegro Common Lisp. (Other releases of Allegro Common Lisp and of other lisps continue to be supported as well.) This includes Allegro Common Lisp running on Windows 98 platforms. John Cowles helped us do some testing and answered questions for us. Thanks John!
We incorporated Ruben Gamboa's changes to allow the building of a variant, ACL2(r), of ACL2, in which the user can reason about the real numbers using non-standard analysis. See real. Note that ACL2(r) and ACL2 have different underlying theories, and books certified in one system may not be included in the other. For backward compatibility and to ensure a smooth transition, ACL2 is built by default, not ACL2(r). This is a compile-time switch; see the makefile for instructions. There should be no changes to ACL2 resulting from the capability of building ACL2(r) from the same sources. Also see acknowledgments for more on the history of ACL2(r).
A large number of bugs (some affecting soundness) were fixed, and many small new features were added. See below.
Less Important Changes:
Some warnings are now considered ``soundness related,'' namely, those that
advise you that an uncertified book has been included or that a book
Several bugs in defstobj were fixed, relating to the possibility
that some of the subfunctions introduced by the
A soundness bug was fixed. The bug might have been exercised if you had an alternative definition (implies hyps (equiv (fn ...) body)) in which equiv is an equivalence relation other than EQUAL. In this case, calls of fn might have been expanded to body in places that were not equiv-hittable.
An obscure soundness bug was fixed. The bug was exercised only if you had a metafunction with a computed hypothesis (i.e., a ``meta hypothesis function''), the hypothesis contained a free variable, i.e., a variable not involved in the term being rewritten, and the free variable occurred in the output of the metafunction. The possibility of this bug was brought to our attention by Robert Krug.
We fixed a bug in the handling of
The handling of
The printing of runes (rule names; see rune) used has been made "deterministic," both in proof output and in proof attempt summaries, by sorting the runes before printing.
The handling of free variables has been improved for hypotheses such as
A new value,
Certain redefinition warnings generated by Allegro Common Lisp have been eliminated.
A bug was fixed in defun-sk that prevented its generated events from being accepted when guard verification is being performed. Thanks to Bill Young for bringing this problem to our attention. A second bug was brought to our attention by Pete Manolios, which was causing certain defun-sk events to be rejected. That problem has been fixed, and an "Infected" warning has also been eliminated.
The command good-bye now works with Allegro Common Lisp.
A low-level bug was fixed that could, for example, cause an error such as
"Error: Expected 5 args but received 4 args" when interrupting a
A bug has been fixed in the proof-builder related to definition expansion. Thanks to Pete Manolios for bringing this to our attention with a simple example.
The functions position and position-equal formerly required the second argument to be a true list. In accordance with Common Lisp, we now also allow the second argument to be a string. This could cause earlier proofs about these functions to fail unless true-listp is known to hold where necessary.
Robert Krug wrote a patch, which has been incorporated, to prevent certain infinite loops that can arise in linear arithmetic. Thanks, Robert!
The macro let* no longer requires the bound variables to be distinct.
An obscure bug was fixed related to congruence rules. The bug would sometimes cause ACL2 to behave as though no rules (other than equality) were available for some argument positions. Thanks to Pete Manolios for bringing this bug to our attention.
Documentation topics have been added for hard-error and prog2$, and the documentation for illegal has been improved. Thanks
to Rob Sumners for a useful suggestion in the examples in documentation for
The event form certify-book was made more secure, in that it can now catch attempts to write a book to disk during its certification. Thanks to Rob Sumners for pointing out the insecurity of the existing mechanism.
A Y2K problem was fixed with our applicative handling of dates.
Accessors and updaters for stobjs have been made more efficient when the underlying lisp is Allegro Common Lisp, by the use of appropriate simple array declarations.
A raw Lisp break had been possible when a certified book that had no guard
verification was included in a session after
The keyword command
Printing has been sped up. In one example the improvement was over 50% in both Allegro and GCL.
We now allow printing in a "downcase" mode, where symbols are printed in
lower case. All printing functions except
A low-level printing function (
The definition of array1p was fixed so that the
In the context of theories, a name now represents not just the
We now translate type declarations of
The theorem prover now behaves reasonably under the combination of
specifying a value of
We changed slightly the definition of round. However, we believe that the new definition is equivalent to the old.
The definition of Common Lisp function substitute has been added.
The following changes have been made in the use of file names within ACL2. We thank Warren Hunt and John Cowles for running some tests of these changes on Macintosh and Windows 98 platforms (respectively).
(1) Names of directories and files now use a syntax like that used for Unix (trademark of AT&T), where directories are separated using the ``
/'' character even when the operating system is not Unix or Linux. See pathname. ACL2 also continues to support its notion of structured pathnames from Version 2.4 and before, but might not do so in future releases and hence no longer documents such syntax.
(2) The command
:set-cbd may now take a relative pathname as an argument.
(3) When the macro ld is given a file name as a value for standard-oi, then if that file name is a relative pathname it refers to the result of prepending the connected book directory (see pathname, see cbd, and see set-cbd) in order to obtain an absolute pathname. Similarly for the
ldspecials standard-co and proofs-co.
The proof-builder has been cleaned up a bit, including the documentation and the capability (once again) to define pc-macro commands (see define-pc-macro) and proof-builder meta commands (see define-pc-meta).
Recall that events generate summaries that include a line beginning with
Macro cw has been documented and now expands to a call of a