Major Section: RELEASE-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.
books subdirectory now contains many new certifiable books,
including solutions to the exercises in the two published books and
full scripts for the case studies. See
Makefile support for book certification has also been
The list of symbols in
*acl2-exports* has been considerably expanded.
If you have packages built by importing
*acl2-exports* you might want
to look carefully at the new value of that constant. The new value includes
:logic mode functions as of Version 2.5, as well as all documented
macros and all built-in theorem names.
certify-book were modified to
have some additional keyword arguments. It is possible to
certify a book containing
events and get warning messages or errors signaled, according to
the settings of these new flags. In addition, it is possible to
include-book whether the book must be certified
(under penalty of error if not). The default values of these new
arguments cause warnings to be printed rather than errors signaled.
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
declare ignore. In past versions of ACL2, a formal
parameter of a
defun was considered ignored if it was not used
in the body, the guard or the measure of the
defun. That meant
that a variable used only in the guard could not be declared ignored
in ACL2; but some Common Lisp compilers would complain because the
variable was not used in the body. Now, ACL2 considers a variable
ignored if it is not used in the body.
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 containing
DEFAXIOMs do not imperil soundness in the proof-
theoretic sense, though they may imperil the validity of theorems.
But you sould know when a book has added an axiom to your logic!) In
previous versions of ACL2, all warnings were inhibited if the token
warning was included in the argument to
set-inhibit-output-lst. Now, soundness related warnings are
printed even if
warnings have been inhibited. To inhibit all
warnings, supply the token
Several bugs in
defstobj were fixed, relating to the
possibility that some of the subfunctions introduced by the
defstobj were already defined.
Puff no longer tries to expand
Previously, the attempt would cause a hard error.
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
hide related to the question
of whether a variable symbol occurs in a term. The old code did not
find the variable and could cause the system to throw away a
hypothesis about it on the grounds that it was never mentioned. Rob
Sumners helped discover this problem.
The handling of
elim rules was generalized, permitting arbitrary
known equivalence relations instead of merely
equal in the
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
(< 0 X), and more generally, any hypotheses involving a
0 (even for example
(< X 1) where
X is known to be
an integer, which is handled as
(<= X 0)). Thanks to Robert Krug
for bringing relevant examples to our attention.
A new value,
:comp, has been implemented for the
:load-compiled-file keyword of
include-book. If this
value is supplied, then a compiled file will always be loaded, even
if that requires creating the compiled file first.
include-book now generates a warning when a compiled
file is expected but not found (see include-book). Formerly,
it only did so when executed at the top level; it failed to generate
the warning when executed on behalf of a surrounding
Certain redefinition warnings generated by Allegro Common Lisp have been eliminated.
A new key has been implemented for the
:bogus-mutual-recursion-ok, set with
Thanks to David Russinoff for pointing out the utility of such a key.
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
defun-sk events to be rejected. That problem has been
fixed, and an "Infected" warning has also been eliminated.
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
A bug has been fixed in the proof-checker related to definition expansion. Thanks to Pete Manolios for bringing this to our attention with a simple example.
A bug has been fixed related to the
:bdd hint in the presence of
equivalence relations. Thanks to Pete Manolios for bringing this to our
attention with a simple example.
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!
let* no longer requires the bound variables to be
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
and the documentation for
illegal has been improved. Thanks to Rob
Sumners for a useful suggestion in the examples in documentation for
prog2$ and a fix 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
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
2). This has been fixed.
The keyword command
comp can now be used to compile only raw
Lisp functions, excluding executable counterparts, by supplying the
nth-of-character-listp was removed from source file
axioms.lisp since it is essentially subsumed by
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
now print characters in lower case for a symbol when the ACL2 state
print-case has value
:downcase and vertical bars are
not necessary for printing that symbol. See IO for a discussion of
set-acl2-print-case. The default
printing remains unchanged, i.e., symbols are printed in upper case
when vertical bars are not required.
A low-level printing function (
prin1$) was modified so that it is
not sensitive to various Common Lisp globals related to printing. So
for example, the function
fmt is no longer sensitive to the value
of Common Lisp global
*print-case*. (The preceding paragraph
explains how to control the case for printing in ACL2.)
The definition of
array1p was fixed so that the
an array must be strictly greater than the number specified in the
:dimensions field; they may no longer be equal. This was always the
intention; the documentation (see arrays) has remained unchanged.
The corresponding change was also made to
array2p. Allegro Common
Lisp formerly caused an error when
compress1 was called on an array
where the numbers above were equal; now, we get a guard violation
instead, which is appropriate.
In the context of theories, a name now represents not just the
:definition rune, as it has done in earlier versions
of ACL2, but also the corresponding
See theories for a discussion of runic designators. Most users
will rarely, if ever, notice this change. One situation where this
change will make a difference is after executing
(in-theory (current-theory 'foo)) followed by
(in-theory (enable bar)), where function
bar is introduced after
bar is recursively defined. The latter
form now enables the rune
(:induction bar), which implies that the
prover can use the induction scheme stored at definition time for
bar. Formerly, the rune
(:induction bar) was not enabled by
(in-theory (enable bar)), and hence the induction scheme for
ignored even when explicit
:induct hints were supplied.
You may now supply
xargs keyword pair
:normalize nil in order to
prevent certain definitions from ``hanging'' when there are many
if-subexpressions. see defun.
We now translate type declarations of
real into guards, as we have
already done for other types such as
rational. For example,
(declare (type real x)) generates the guard
The theorem prover now behaves reasonably under the combination of
specifying a value of
t both for
otf-flg and for a hint
:do-not-induct. Previously, it aborted the first time it would have
otherwise pushed a goal for induction, but now, it will continue and
wait until all induction subgoals have been pushed before it aborts.
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-cbdmay now take a relative pathname as an argument.
(3) When the macro
ldis 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. Simiarly for the
It is no longer necessary to issue
t if you
include a stobj declaration for
state, for example:
(declare (xargs :stobjs state))See declare-stobjs.
The proof-checker 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-checker meta commands (see define-pc-meta).
Recall that events generate summaries that include a line beginning
Warnings:'', which is followed (on the same line) by zero or
more brief strings that summarize the warnings generated by that
event. Formerly, this warnings summary for an
include-book event did not include the summary strings for
warnings generated by subsidiary events. This has been fixed.
cw has been documented and now expands to a call of
logic mode function. See cw for a way to print to the screen
without having to involve the ACL2
state. Thanks to Rob Sumners
for suggesting that we document this useful utility.
odds are now
logic mode functions.