Major Section: RELEASE-NOTES
Also see note-2-9-1, see note-2-9-2, and see note-2-9-3 for other changes since the last non-incremental release (Version_2.9).
A soundness bug has been fixed that was due to inadequate checking of
meta rules in the presence of
defevaluator event is insufficient for
:meta rule (an example is shown in source function
chk-acceptable-rules). Thanks to Dave Greve and Jared Davis for bringing
this bug to our attention, by sending a proof of
nil that exploited this
bug. The fix is to check legality of
:meta rules even when skipping
proofs during an
include-book event or the second pass of an
Fixed problem with parallel make for workshop books by adding a dependency
Default hints (see set-default-hints) no longer prevent the use of
:INSTRUCTIONS (see proof-checker). Thanks to Jared Davis for pointing
out this problem.
remove-equal have been defined, in
remove. These two symbols have also been added to
*acl2-exports*. Thanks to David Rager for pointing out that
remove-equal was missing. Moreover, the definitions of
delete1-equal have been eliminated. Function
remove1-eq, now in
logic mode in source file
axioms.lisp, serves in place of
delete1-eq, with corresponding new function definitions for
assert$ has been added to
*acl2-exports*. Thanks to
Jared Davis for the suggestion.
Added SBCL support. Thanks to Juho Snellman for significant assistance with
the port. Thanks to Bob Boyer for suggesting the use of feature
:acl2-mv-as-values with SBCL, which can allow thread-level parallelism
in the underlying lisp; we have done so when feature
We have continued to incorporate suggestions for wording improvements in documentation and error messages. Thanks to all who send these suggestions, especially to Eric Smith, who has suggested the vast majority of them.
Made a small improvement to errors and warnings caused on behalf of set-enforce-redundancy, to indicate when an event of the same name already exists.
Fixed a bug in
books/misc/rtl-untranslate.lisp that was causing a guard
violation when adding a new entry for an existing key.
Fixed a bug in translation to internal form that caused
defchoose to have difficulties handling ignored variables in
forms. Thanks to Sandip Ray to bringing this issue to our attention with a
(push :acl2-mv-as-values *features*) has been added in source
acl2-init.lisp for SBCL and OpenMCL only, in order to support
parallel execution (looking to the future...).
Default-hints (see set-default-hints) were being ignored inside the proof-checker, but no longer. Thanks to John Erickson for bringing this problem to our attention and providing a simple example of it.
"make" target (specifically, function
make-tags) so that it is gracefully skipped if the
etags program is
not found. Thanks to David Rager for pointing out this issue.
Sandip Ray has re-worked the supporting materials for his ACL2 Workshop 2003
talk (originally with John Matthews and Mark Tuttle), to run in a few
minutes. The result is in
and is included in the full ACL2 regression suite. Thanks, Sandip.
Debian releases of ACL2 had created superfluous
.cert.final files when
certifying books. This has been fixed; thanks to Jared Davis for noticing
Jared Davis has pointed out that ``If you add a
:backchain-limit-lst 0 to
a rewrite rule whose hypotheses are all forced, then ACL2 `really assumes them'
without trying to relieve them right there through rewriting.'' Relevant
documentation has been added for
:backchain-limit-lst; see rule-classes.
A new version of the rtl library has been included in
Thanks to David Russinoff for contributing hand proofs for the new lemmas,
and to Matt Kaufmann for carrying out their mechanization.
Fixed a bug in
save-exec that was failing to set the initial
according to the current directory when starting up ACL2. Thanks to Camm
Maguire for bringing our attention to this problem.
Variables introduced during
let* abstraction are now in the current
package. Thanks to Jared Davis for suggesting such a change.
It is now allowed for two definitions to be considered the same from the
standpoint of redundancy (see redundant-events) when one specifies a
t and the other has no explicit
the guard is implicitly
t). Thanks to Jared Davis for bringing this
issue to our attention.
(For users of
emacs/emacs-acl2.el) There have been a few enhancements to
emacs/emacs-acl2. el (skip this paragraph if you don't
use that file):
Control-t qcontinues to compare windows ignoring whitespace, but now, a prefix argument can be given to control case is also ignored (ignore case if positive, else use case).
Control-t Control-lhas been defined to be similar to
Control-t l, except that proofs are skipped and output is suppressed.
Control-t uhas been defined to print, to the shell buffer, a
ubt!form for the command containing the cursor.
o Control-t Control-f buries the current buffer.
Meta-x new-shellnow puts the new shell buffer in
shell-mode(thanks to David Rager for noticing this issue).
Linear arithmetic has been modified so that we do not generate the equality
(equal term1 term2) from the pair of inequalities
(<= term1 term2)
(<= term2 term1) in the case that we would have to
term2 to be
acl2-numberps. Thanks to Dave Greve for
providing a motivating example and to Robert Krug for providing a fix.
delete-include-book-dir had not been allowed inside
encapsulate forms. This was an oversight, and has been
Sandip Ray has contributed a new library of books to support proofs of
partial and total correctness of sequential programs based on assertional
books/symbolic/. This work is based on the paper
J. Matthews, J S. Moore, S. Ray, and D. Vroon, ``A Symbolic Simulation
Approach to Assertional Program Verification,'' currently in draft form.
In particular, the books include the macro
automatically transforms inductive assertion proofs of correctness of
sequential programs to the corresponding interpreter proofs. See the
README in that directory.
We have changed the implementation of
:dir :system for
include-book. This change will not affect you if you build an ACL2
executable in the normal manner, leaving in place the
of the source directory; nor will it affect you if you download a GCL Debian
binary distribution. The change is that if environment variable
ACL2_SYSTEM_BOOKS is set, then it specifies the distributed books
directory, i.e., the directory determined by
:dir :system. You may find
it convenient to set this variable in your ACL2 script file (typically,
saved_acl2). If it is set when you build ACL2, the generated script for
running ACL2 will begin by setting
ACL2_SYSTEM_BOOKS to that value.
Thanks to various people who have discussed this issue, in particular Jared
Davis who sent an email suggesting consideration of the use of an environment
variable, and to Eric Smith who helped construct this paragraph. (Note that
this use of
ACL2_SYSTEM_BOOKS replaces the use of
described previously; see note-2-9-1.)
ACL2 now automatically deletes files
TMP*.lisp created during the build
process and created by
comp. If you want these to be saved,
(assign keep-tmp-files t) in the ACL2 loop or in raw Lisp. The
clean target for the standard
make process for certifying books
(see book-makefiles) will however delete all files
TMP files discussed just above now generally include the current process
ID in their names, e.g.,
TMP@email@example.com instead of
Thanks to Bob Boyer for suggesting this measure, which will reduce the
possibility that two different processes will attempt to access the same
pe will print the information formerly printed by
slightly enhanced to work for logical names that are strings, not just
symbols. Thanks to Warren Hunt for leading us to this change by suggesting
:pe nth print the definition of
We eliminated spurious warnings that could occur in raw mode in OpenMCL or CMUCL when stobjs are present. We thank Juho Snellman for pointing out the relevant bug and appropriate fix.
Mfc-rw now takes a third argument that can specify an arbitrary known
equivalence relation; see extended-metafunctions. Thanks to Dave Greve for
discussions suggesting this improvement.
A small modification to a symbol-reading function allows documentation string processing on Windows systems that use CR/LF for line breaks. Thanks to William Cook for bringing this issue to our attention.
The documentation has been improved on how to control the printing of ACL2 terms. See user-defined-functions-table. Thanks to Sandip Ray for asking a question that led to the example presented there.
We fixed an inefficiency that could cause an
ld command to seem to hang
at its conclusion. Thanks to Sandip Ray for pointing out this problem.
We checked that ACL2 runs under Lispworks 4.4.5 (last checked before 4.3), and have inhibited redefinition warnings.
Two changes have been made on behalf of congruence-based reasoning. Thanks to Dave Greve for examples and discussions that have led to these changes, and to Eric Smith and Vernon Austel, who also sent relevant examples.
o When a call of the new unary function
double-rewriteis encountered by the rewriter, its argument will be rewritten twice. This solves certain problems encountered in congruence-based rewriting. Warnings for
linearrules will suggest when calls of
double-rewriteon variables in hypotheses are likely to be a good idea. See double-rewrite.
o Hypotheses of the form
(equiv var (double-rewrite term)), where
equivis a known equivalence relation and
varis a free variable (see free-variables), will bind
varto the result of rewriting
termtwice. Previously, hypotheses of the form
(equal var term)would bind a free variable
var, but the call had to be of
equalrather than of an arbitrary known equivalence relation.
The following improvements were made in support of ACL2 on top of OpenMCL.
o New versions of OpenMCL that do not have
:mclin Lisp variable
*features*will now work with ACL2. Thanks to David Rager for bringing this issue to our attention.
o Added support for OpenMCL 1.0 for 64-bit DarwinPPC/MacOS X, thanks to Robert Krug.
o Fixed tracing in OpenMCL so that the level is reset to 1 even if there has been an abort.
o Added support in OpenMCL for
o Incorporated suggestions from Gary Byers for printing the ``Welcome to OpenMCL'' prompt before initially entering the ACL2 loop and, and for setting useful environment variable
CCL_DEFAULT_DIRECTORYin the ACL2 script.
Fixed a long-standing bug in forward-chaining, where variable-free hypotheses were being evaluated even if the executable-counterparts of their function symbols had been disabled. Thanks to Eric Smith for bringing this bug to our attention by sending a simple example that exhibited the problem.
Improved reporting by the break-rewrite utility upon failure to relieve hypotheses in the presence of free variables, so that information is shown about the attempting bindings. See free-variables-examples-rewrite. Thanks to Eric Smith for requesting this improvement. Also improved the break-rewrite loop so that terms, in particular from unifying substitutions, are printed without hiding subterms by default. The user can control such hiding (``evisceration''); see set-brr-term-evisc-tuple.
A new directory
books/defexec/ contains books that illustrate the use of
defexec. Thanks to the contributors of those books (see
README file in that directory).
books/rtl/rel3 are no longer
distributed. They are still available by email request. (Subdirectory
rel1/ supports some of the optional
workshop/ books, so it is still
books/misc/sticky-disable.lisp to manage theories that
might otherwise be modified adversely by
include-book. Thanks to Ray
Richards for a query that led to our development of this tool.
(quit) may now be used to quit ACL2 and Lisp
completely; in fact they macroexpand to calls of the same function as does
good-bye (which is now a macro). Thanks to Jared Davis for suggesting
the new aliases. (OpenMCL-only comment:) These all work for OpenMCL even
inside the ACL2 loop.
wet now hides structure by default on large expressions.
However, a new optional argument controls this behavior, for example avoiding
such hiding if that argument is
nil. See wet. Thanks to Hanbing Liu for
pointing out that
wet was not helpful for very large terms.
We have fixed a bug in the forward-chaining mechanism that, very rarely, could cause a proof to be aborted needlessly with an obscure error message. Thanks to Jared Davis for sending us an example that evoked this bug.
Fixed a bug that was causing proof output on behalf of
:functional-instance to be confusing, because it failed to mention that
the number of constraints may be different from the number of subgoals
generated. Thanks to Robert Krug for pointing out this confusing output.
The fix also causes the reporting of rules used when silently simplifying the
constraints to create the subgoals.
Fixed a bug in handling of leading
./ in pathnames, as in:
(include-book "./foo"). Thanks to Jared Davis for bringing this bug to
Made a small fix for handling of free variables of
rules, which had erroneously acted as though a hypothesis
(equal var term) can bind the variable
A small change has been made for
type-prescription rules for
hypotheses of the form
(equal var term), where c[var] is a free variable
and no variable of
term is free (see free-variables). As with
linear rules, we now bind
term even if
(equal u term) happens to be known in the current
context for some term
u. Also as with
rules, similar handling is given to hypotheses
(equiv var (double-rewrite term)) where
equiv is a known
We changed the handling of free variables in hypotheses of
rules being handled by the proof-checker's
in complete analogy to the change described just above for
The installation instructions have been updated for obtaining GCL on a
Macintosh. Thanks to Robert Krug for supplying this information and to Camm
Maguire for simplifying the process by eliminating the
comp is now an event, so it may be placed in books.
save-exec call could fail because of file permission
issues, yet ACL2 (and the underlying Lisp) would quit anyhow. This has been
fixed. Thanks to Peter Dillinger for bringing this problem to our attention.
Jared Davis, with assistance from David Rager, has updated his ordered sets
books/finite-set-theory/osets/. See file
A new function,
reset-kill-ring, has been provided for the rare user
who encounters memory limitations. See reset-kill-ring.