NOTE-2-9-4

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 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-checker). 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 to 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-checker, 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 book-makefiles) 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-checker'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.