NOTE-2-5

Major Section:  RELEASE-NOTES

Important Changes:

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.

The 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 books/README.html.

Improved Unix Makefile support for book certification has also been written. See books/README.html.

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 all :logic mode functions as of Version 2.5, as well as all documented macros and all built-in theorem names.

Include-book and certify-book were modified to have some additional keyword arguments. It is possible to certify a book containing defaxiom and/or skip-proofs events and get warning messages or errors signaled, according to the settings of these new flags. In addition, it is possible to specify in 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 defaxiom and/or skip-proofs events.

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 with 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 DEFAXIOM or SKIP-PROOFS events. (Technically, 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 warning! to set-inhibit-output-lst.

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 defstobj events. 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 concluding equality.

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 as (< 0 X), and more generally, any hypotheses involving a comparison with 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.

The event 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 include-book command.

Certain redefinition warnings generated by Allegro Common Lisp have been eliminated.

A new key has been implemented for the acl2-defaults-table, :bogus-mutual-recursion-ok, set with :set-bogus-mutual-recursion-ok. 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 certain defun-sk events to be rejected. That problem has been fixed, and an "Infected" warning has also been eliminated.

The command 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 interrupting a local event.

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.

The functions position and position-equal formerly 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!

The macro let* no longer requires the bound variables to be distinct.

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 hard-error and prog2$, 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 sublis.

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 existing mechanism.

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 (set-verify-guards-eagerness 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 argument :raw.

Rewrite rule nth-of-character-listp was removed from source file axioms.lisp since it is essentially subsumed by characterp-nth.

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 print-object$ now print characters in lower case for a symbol when the ACL2 state global variable print-case has value :downcase and vertical bars are not necessary for printing that symbol. See IO for a discussion of the macros acl2-print-case and 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 :maximum-length of 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 corresponding :definition rune, as it has done in earlier versions of ACL2, but also the corresponding :induction rune. 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 event foo, and bar is recursively defined. The latter in-theory 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 bar was 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 (rationalp x). See type-spec.

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-cbd may now take a relative pathname as an argument.

(3) When the macro ld is 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 ld specials standard-co and proofs-co.

(declare (xargs :stobjs state))

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 with ``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 encapsulate or include-book event did not include the summary strings for warnings generated by subsidiary events. This has been fixed.

Macro cw has been documented and now expands to a call of a ;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.

Functions duplicates, add-to-set-equal, intersection-eq, evens, and odds are now :logic mode functions.