Note-2-9-4
ACL2 Version 2.9.4 (February, 2006) 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 local events.
Specifically, a local defevaluator event is insufficient for
supporting a :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 encapsulate event.
Fixed problem with parallel make for workshop books by adding a dependency
line to books/workshops/2003/Makefile.
Default hints (see set-default-hints) no longer prevent the use of
:INSTRUCTIONS (see proof-builder). Thanks to Jared Davis for
pointing out this problem.
New functions remove-eq and remove-equal have been defined,
in analogy to 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-eq
and 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 remove1 and remove1-equal.
The symbol 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 :sb-thread is
present.
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 defun-sk
and defchoose to have difficulties handling ignored variables in
let forms. Thanks to Sandip Ray for bringing this issue to our
attention with a helpful example.
The form (push :acl2-mv-as-values *features*) has been added in source
file 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-builder, but no longer. Thanks to John Erickson for bringing
this problem to our attention and providing a simple example of it.
Modified the TAGS "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 workshops/2003/ray-matthews-tuttle/support/
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
this problem.
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 books/rtl/rel5/.
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
cbd 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. See set-let*-abstractionp.
It is now allowed for two definitions to be considered the same from the
standpoint of redundancy (see redundant-events) when one specifies a
:guard of t and the other has no explicit :guard
(hence, 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 distributed file emacs/emacs-acl2.el (skip this paragraph if you
don't use that file):
o Control-t q continues 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).
o Control-t Control-l has been defined to be similar to Control-t
l, except that proofs are skipped and output is suppressed.
o Control-t u has 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.
o Meta-x new-shell now 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)
and (<= term2 term1) in the case that we would have to force both
term1 and term2 to be ACL2-numberps. Thanks to Dave Greve
for providing a motivating example and to Robert Krug for providing a fix.
The event delete-include-book-dir had not been allowed inside books and encapsulate forms. This was an oversight, and has been
fixed.
Sandip Ray has contributed a new library of books to support proofs of
partial and total correctness of sequential programs based on assertional
reasoning, in 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 defsimulate, which 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 ld and
include-book. This change will not affect you if you build an ACL2
executable in the normal manner, leaving in place the books/ subdirectory
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 ACL2_SRC_BOOKS
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, evaluate (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 books-certification-classic) will however delete all files
TMP*.*.
The TMP files discussed just above now generally include the current
process ID in their names, e.g., TMP@16388@1.lisp instead of
TMP1.lisp. Thanks to Bob Boyer for suggesting this measure, which will
reduce the possibility that two different processes will attempt to access the
same temporary file.
Now, :pe will print the information formerly printed by
:pe!, 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 that :pe nth print the definition of nth.
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, 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-rewrite
is encountered by the rewriter, its argument will be rewritten twice. This
solves certain problems encountered in congruence-based rewriting. Warnings
for :rewrite and :linear rules will suggest when
calls of double-rewrite on variables in hypotheses are likely to be a
good idea. See double-rewrite.
o Hypotheses of the form (equiv var (double-rewrite term)), where
equiv is a known equivalence relation and var is a free
variable (see free-variables), will bind var to the result of
rewriting term twice. Previously, hypotheses of the form (equal var
term) would bind a free variable var, but the call had to be of
equal rather 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 :mcl in 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 WET.
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_DIRECTORY in 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 :DOC
set-brr-term-evisc-tuple.
A new directory books/defexec/ contains books that illustrate the use
of mbe and defexec. Thanks to the contributors of those books
(see the README file in that directory).
The directories books/rtl/rel2 and 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
distributed.)
Added book 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.
The commands (exit) and (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.
The macro 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. 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
our attention.
Made a small fix for handling of free variables of :forward-chaining rules, which had erroneously acted as though a hypothesis
(equal var term) can bind the variable var.
A small change has been made for :type-prescription rules for
hypotheses of the form (equal var term), where var is a free
variable and no variable of term is free (see free-variables). As
with :rewrite and :linear rules, we now bind
var to term even if (equal u term) happens to be known in the
current context for some term u. Also as with :rewrite and
:linear rules, similar handling is given to hypotheses (equiv var
(double-rewrite term)) where equiv is a known equivalence
relation.
We changed the handling of free variables in hypotheses of :rewrite rules being handled by the proof-builder's rewrite
(r) command, in complete analogy to the change described just above for
:type-prescription rules.
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 gettext
dependency.
The macro comp is now an event, so it may be placed in books.
Previously, a 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
library, books/finite-set-theory/osets/. See file CHANGES.html in
that directory.
A new function, reset-kill-ring, has been provided for the rare
user who encounters memory limitations. See reset-kill-ring.
