Major Section: RELEASE-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))))Thanks to Robert Krug for providing a fix for the above error.
[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.
Guard-checking was being inhibited (since v2-9) for calls of built-in
primitives on explicit values, e.g.,
(car 3). This has been fixed.
Guard-related warnings could be printed during proofs (this bug was introduced in Version_2.9.1). These warnings have been eliminated.
posp-compound-recognizer are now built into ACL2 for predicates
posp, and hence have been deleted from book
natp-posp.lisp (where they were called
file-clock-p, which recognizes a component of the ACL2
state, is now defined using
natp instead of
Thanks to Jared Davis for suggesting this change. (Technical explanation
about functions in ACL2 source file
axioms.lisp: With a
-1, the call of
open-input-channel will create
a channel that can't be closed; see the guard of
(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
allegro-app and file
build-allegro-exe.cl for more
The new home page now contains a link to a new page
which contains information about other ACL2 releases. (This is in one's
local home page, but may not show up on the central ACL2 home page until the
next non-incremental release.) Thanks to Warren Hunt for suggesting this
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
been fixed. Thanks to Aaron Smith for pointing out the problem.
A new documentation topic defun-sk-example gives a little more help in
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'sThanks 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
-joption, can be used.
(2) Book certifications now stops at the first failure if
books/Makefile-genericis used, and returns non-zero exit status. However, the various make targets in the ACL2 source directory (
certify-books, etc.) still continue past failures unless you provide
ACL2_IGNORE=' 'on the
(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
.acl2files cause the appropriate depedencies to be generated.
.datemechanism, which was interfering with
make -n; so, these files are no longer written.
A mechanism has been added for saving output. In particular, you can now
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 book-makefiles.
Fixed a bug in
sys-call-status that was causing hard Lisp errors.
cw-gstack to allow a
:frames argument to specify a range
of one or more frames to be printed. see cw-gstack.
Fixed a bug in proof-checker command
forwardchain. Thanks to
Ming-Hsiu Wang for bringing this bug to our attention.
We have provided a mechanism for saving an executable image.
See saving-and-restoring and see save-exec. We have eliminated obsolete
ground-zero theory so that it contains all of the
built-in rules (in ACL2 source file
axioms.lisp). It had formerly failed
to include rules from some definitions and theorems near the end of
A new event,
set-enforce-redundancy, allows the enforcement of
defun, and most other events during book development.
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
Other book changes include a change to lemma
books/ihs/quotient-remainder-lemmas.lisp, as suggested by Jared Davis.
real/rationalp may now be referred to in
events and hints, thanks to a new
Thanks to Jared Davis for this suggestion.
ACL2 terms of the form
(if p 'nil 't) are now printed as
where in some setting they had been printed as
(and (not p) t). Thanks
to Robert Krug for this improvement.
(GCL ONLY) Added profiling support, based heavily on code supplied by Camm
Maguire. See file
save-gprof.lsp for instructions. Thanks to Camm, and
also to David Hardin for inspiring this addition.
Added support for preprocessing before printing (untranslating) a term.
See user-defined-functions-table, in particular the discussion of
untranslate-preprocess. Thanks to Jared Davis for inspiring this
addition, and for providing a book that takes advantage of it
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.