ACL2 Version 2.9.3 (August, 2005) Notes
Also see note-2-9-1 and see note-2-9-2 for other changes since the last non-incremental release (Version_2.9).
We fixed a soundness bug that exploited the ability to define
:set-guard-checking nil ; execute before certifying the book below (in-package "ACL2") (encapsulate () (local (defun f1 () (declare (xargs :mode :program)) (char-upcase (code-char 224)))) (local (defconst *b* (f1))) (defun f1 () (char-upcase (code-char 224))) (defconst *b* (f1)) (defthm bad (not (equal *b* (code-char 224))) :rule-classes nil)) (defthm ouch nil :hints (("Goal" :use bad)) :rule-classes nil)
We fixed a soundness hole due to the fact that the "LISP" package does not exist in OpenMCL. We now explicitly disallow this package name as an argument to defpkg. Thanks to Bob Boyer and Warren Hunt for bringing an issue to our attention that led to this fix.
ACL2 now requires all package names to consist of standard characters (see standard-char-p, none of which is lower case. The reason is that we have seen at least one lisp implementation that does not handle lower case package names correctly. Consider for example the following raw lisp log (some newlines omitted).
>(make-package "foo") #<"foo" package> >(package-name (symbol-package 'FOO::A)) "foo" >(package-name (symbol-package '|FOO|::A)) "foo" >
Distributed book
Added
Added a line to
The executable scripts for saved ACL2 images now include
(For GCL profiling only) Fixed a colon (
The documentation for
Fixed a bug in the guard for function
For those who want to experiment with an alternate implementation of mv and mv-let, there is now support for under-the-hood implementation
of these in terms of raw Lisp functions
A change related to the one just above is that we now limit the maximum number of arguments to any call of mv to 32. Thanks to Bob Boyer for raising a question that lead to this change.
Eliminated some compiler warnings in OpenMCL.
In the rtl library (
A new function time$ permits timing of forms, by using (under the
hood) the host Common Lisp's
We fixed an infinite loop that could occur during destructor elimination (see elim). Thanks to Sol Swords to bringing this to our attention and sending a nice example, and to Doug Harper for sending a second example that we also found useful.
The method of speeding up GCL-based builds (see note-2-9-2) has changed slightly from Version_2.9.2. Now, in the `make' command:
LISP='gcl -eval "(defparameter user::*fast-acl2-gcl-build* t)"
We improved the pretty-printer's handling of keywords. For example, before this change one might see the following printed by ACL2.
(MODIFY TH S :KEY1 VAL1 :KEY2 (IF (IF X Y Z) AAAAAAAAAA BBBBBBB))
Now, the above might print as follows. Notice that we have avoided breaking after a keyword (see keywordp) that is preceded by other forms on the same line.
(MODIFY TH S :KEY1 VAL1 :KEY2 (IF (IF X Y Z) AAAAAAAAAA BBBBBBB))
See note-2-9-3-ppr-change for a detailed discussion of this change.
(GCL ONLY) Evaluation in a break is no longer inhibited by ACL2 when built on top of GCL, so GCL now matches other Common Lisps in this respect.
For ACL2 built on most host Common Lisps, you will see the string
Jared Davis suggested improvements to lemmas
The proof-builder command
Fixed downcase printing so that the package name of a symbol is also
downcased. For example, after execution of
It is now possible to control the output so that numbers are printed in
binary, octal, or hex, though the default is still radix 10. See set-print-base. Note that in support of this change, built-in functions
explode-nonnegative-integer and
Built-in axiom
Lemmas about alphorder (
ACL2 has, for some time, printed a space in the event summary after the
open parenthesis for a defthm event, in order to ease backward
searching for the original form, for example
Form: ( DEFTHM BAR ...)
The intention was that this extra space should be printed for every event form; but it was missing in some cases, for example, for verify-guards. This has been fixed.
In analogy to include-book, now ld takes the (optional)
keyword argument
We fixed a bug in include-book that could cause an error when redefinition is on, for example:
(set-ld-redefinition-action '(:warn! . :overwrite) state) (include-book "/u/acl2/books/arithmetic/top")
The behavior of include-book now matches the documentation: handling of compiled files for uncertified books will follow the same rules as for certified books. In particular, if you create an object file in raw Lisp for some book, then including that book will load that object file. Thanks to Jared Davis for bringing this issue to our attention.
New documentation explains the interaction of redefinition and redundancy. See redundant-events — the ``Note About Unfortunate Redundancies'' is new. Thanks to Grant Passmore for providing examples that led us to write this additional documentation.
Solutions to exercises in
How To Prove Theorems Formally are now available in distributed book