ACL2 Version 2.9.2 (April, 2005) Notes
Also see note-2-9-1 for other changes since the last non-incremental release (Version_2.9).
There was a bug in non-linear arithmetic (see non-linear-arithmetic) that caused the following error:
ACL2 !>(include-book "rtl/rel4/lib/top" :dir :system) .... ACL2 !>(set-non-linearp t) T ACL2 !>(thm (implies (and (bvecp a 77) (bvecp b 50)) (bvecp (fl (/ (* a b) (expt 2 23))) 104)) :hints (("Goal" :in-theory (enable bvecp)))) [Note: A hint was supplied for our processing of the goal above. Thanks!] By the simple :definition BVECP, the :executable-counterparts of EXPT and UNARY-/ and the simple :rewrite rule ASSOCIATIVITY-OF-* we reduce the conjecture to Goal' (IMPLIES (AND (INTEGERP A) (<= 0 A) (< A 151115727451828646838272) (INTEGERP B) (<= 0 B) (< B 1125899906842624)) (BVECP (FL (* A B 1/8388608)) 104)). HARD ACL2 ERROR in VARIFY: This should not have happened. The supposed variable, '1/8388608, is instead a constant. ACL2 !>
Thanks to Robert Krug for providing a fix for the above error.
Guard-checking was being inhibited (since v2-9) for calls of built-in
primitives on explicit values, e.g.,
Guard-related warnings could be printed during proofs (this bug was introduced in Version_2.9.1). These warnings have been eliminated.
(Allegro CL users only) Support is now provided for building an Allegro CL
application, provided you have an Allegro CL dynamic runtime license. (Our
belief is that with such a license, many users can use the same application,
rather than each user needing a separate license.) See new GNUmakefile target
The new home page now contains a link to a new page
We thank Erik Reeber for suggesting a solution to output redirection using sys-call, which we have described at the end of its documentation.
A new documentation topic fixes the flawed argument for conservativity of the defchoose event that appears in Appendix B of Kaufmann and Moore's paper, ``Structured Theory Development for a Mechanized Logic'' (Journal of Automated Reasoning 26, no. 2 (2001), pp. 161–203). See conservativity-of-defchoose. Thanks to John Cowles and Ruben Gamboa for helpful feedback on drafts of this note.
The solution to exercise 6.15 in
A new documentation topic defun-sk-example gives a little more help in using defun-sk effectively. Thanks to Julien Schmaltz for presenting this example as a challenge.
(GCL only) There is now a way to speed up GCL builds of ACL2, at the cost of perhaps a percent or so in performance of the resulting image. Using `make' one supplies the following.
LISP='gcl -eval "(defparameter user::*fast-acl2-gcl-build* t)"
Various makefiles have been improved in several ways.
(1) Parallel book certification, using GNU make's
-joption, can be used.
(2) Book certifications now stops at the first failure if
books/Makefileor books/Makefile-genericis used, and returns non-zero exit status. However, the various make targets in the ACL2 source directory ( regression, certify-books, etc.) still continue past failures unless you provide ACL2_IGNORE=' 'on the `make' command line.
(3) The build process has been modified (file
GNUmakefile) so that it stops upon a failed compile or a failed initialization.
(4) The automatic dependency generation (from ``
make dependencies'' has been improved so that commands of the form (ld "my-book.lisp")in .acl2files cause the appropriate dependencies to be generated.
Thanks to comments from several users that led to the above Makefile
improvements: Ray Richards, Doug Harper, and the Rockwell ACL2 users for (1)
and (2) (and inspiring (4)), and David Rager for (2) and (3). In particular,
Doug Harper sent a replacement for the
A mechanism has been added for saving output. In particular, you can now call ld on a file with output turned off, for efficiency, and yet when a proof fails you can then display the proof attempt for the failed (last) event. See set-saved-output. Another new command — see set-print-clause-ids — causes subgoal numbers to be printed during proof attempts when output is inhibited.
Documentation has been added for using ACL2's makefile support to automate the certification of collections of books. See books-certification-classic.
Fixed a bug in sys-call-status that was causing hard Lisp errors.
Improved cw-gstack to allow a
Fixed a bug in proof-builder command
We have provided a mechanism for saving an executable image. See saving-and-restoring and see save-exec. We have eliminated obsolete
Modified the ground-zero theory so that it contains all of
the built-in rules (in ACL2 source file
A new event, set-enforce-redundancy, allows the enforcement of defthm, defun, and most other events during book development. See set-enforce-redundancy.
A bug has been fixed that had allowed deftheory events to cause a hard Lisp error when calling union-theories on ill-formed theories after, for example:
:set-guard-checking nil (in-theory (union-theories '((:rewrite no-such-rule)) (current-theory 'ground-zero)))
The handling of guard checking has been modified somewhat in a way that should only very rarely affect users. (An ``Essay on Guard Checking'' in the ACL2 source code explains this point to anyone interested in implementation details.)
(GCL ONLY) Removed the -dir setting in the ACL2 wrapper script for GCL. This should generally have no effect for most users, but it eliminates a potential source of error down the road.
Several interesting new definitions and lemmas have been added to the rtl
library developed at AMD, and incorporated into
The macro real/rationalp may now be referred to in in-theory events and hints, thanks to a new add-macro-alias event. Thanks to Jared Davis for this suggestion.
ACL2 terms of the form
(GCL ONLY) Added profiling support, based heavily on code supplied by Camm
Maguire. See file
Added support for preprocessing before printing (untranslating) a term.
See user-defined-functions-table, in particular the discussion of
The documentation has been improved for explaining how runes are assigned; see rune. Thanks to Robert Krug for pointing out inaccuracies in the existing documentation.