		Search-engine friendly clone of the ACL2 documentation.

Release-notes

Note-6-4

ACL2 Version 6.4 (January, 2014) Notes

NOTE! New users can ignore these release notes, because the documentation has been updated to reflect all changes that are recorded here.

Below we roughly organize the changes to ACL2 since Version 6.3 into the following categories of changes: existing features, new features, heuristic improvements, bug fixes, changes at the system level, Emacs support, and experimental versions. Each change is described in just one category, though of course many changes could be placed in more than one category.

See also note-6-4-books for a summary of changes made to the ACL2 Community Books since ACL2 6.3, including the build system.

Changes to Existing Features

Gag-mode no longer saves prover output when PROVE output is inhibited (see set-inhibit-output-lst). This may improve performance slightly when certifying community books using their Makefile or build::cert.pl; in particular, GCL 2.6.8 running on a Mac can now certify the book books/tau/bounders/elementary-bounders.lisp without running out of space, even without explicitly turning off gag-mode (which had been done shortly before the Version 6.3 release).

When include-book fails to find a readable certificate (.cert) file, the error message now distinguishes between the case that this file is missing and the case that read permission is missing.

(GCL only) Time reporting has been improved when the host Lisp is Gnu Common Lisp. A key change was made in the computation of runtime (for example, to report in event summaries), so that it includes the ``child runtime''. See get-internal-time. Also, the utility time$ now gives improved information by including child runtime information, which can be significant; for example, it probably includes compile time, while the ``seconds runtime'' statistic (still) does not. Recent versions of GCL might also provide system runtime and child system runtime. See time$. Thanks to Camm Maguire for suggesting these improvements to time$ and providing an initial implementation for them.

Fixed a bug in an ACL2 system function, our-truename, which returns the ``true name'' for a file name, when supplied with an optional second argument. Thanks to Camm Maguire for bringing this bug to our attention.

The wording in theory warnings has been improved, to avoid giving the impression that you are newly disabling a built-in rule in the case that it merely remains disabled.

As requested by Sol Swords, erroneous evaluations of system function magic-ev-fncall that had produced a message, msg, will now also return that message. The following example, sent by Sol, illustrates the fix: before, evaluation of (magic-ev-fncall 'cons '(a) state nil nil) printed a message (to the comment window) and then returned (mv t nil), but now it returns mv t <msg>, where <msg> denotes the message (printed with the fmt ~@ directive).

Fixed :pbt to avoid printing the bodies of defconst forms. Thanks to Jared Davis for pointing out the large output when the body is a large character string.

A new output type, history, now controls the printing of history-related information; see set-inhibit-output-lst. The unused output type, expansion, is no longer supported, i.e., is no longer a member of the list *valid-output-names*. Because of this change, printing of information when undoing, as by :u, will now take place even when event output is inhibited (if history output is not inhibited); we thank Sol Swords for requesting that change.

The :loop-stopper field of a rule of class :rewrite, should still be a list of lists (var1 var2 fn1 fn2 ... fnk), where var1 and var2 are variables and the fni are symbols. But formerly each fni was required to be a function symbol; now, it can be a macro alias for a function symbol (see add-macro-alias). For example, the following is a valid :loop-stopper field: ((x y +)).

The restrictions on utilities oracle-apply and oracle-funcall have been updated in order to avoid potentially confusing or inappropriate results, by imposing the following new requirements on their first argument, which must still be a function symbol. That symbol must not be if (formerly the illegal symbol was return-last); it must not be a key of the alist, *ttag-fns-and-macros*; it must not be untouchable (see remove-untouchable); and it must not be a stobj creator (see defstobj).

The table guard on dive-into-macros-table has been strengthened in order to avoid calling untouchable functions (see remove-untouchable).

New Features

We have added a tool for writing out useful information about a book's event names when certifying the book. See bookdata. Thanks to Dave Greve for requesting this tool and participating in its specification.

There are new analogues of add-include-book-dir and delete-include-book-dir: add-include-book-dir! and delete-include-book-dir!, respectively. The new utilities are similar to their existing counterparts, except that their effects are not local to enclosing books or encapsulate events. Thanks to Shilpi Goel for requesting this enhancement.

The class of congruence rules has been broadened considerably, so that one can restrict to patterns. For example, a congruence rule can now state that an equivalence is maintained for the term (mv-nth 1 (f (cons u v) y 'a)) when rewriting y. See patterned-congruence. Thanks to Sol Swords for requesting this feature.

Heuristic Improvements

(None to report this time.)

Bug Fixes

Fixed a soundness bug in the handling of hypotheses of conditional :definition rules invoked during rewriting by applying :expand hints. See (defxdoc note-6-4 ...) in community book system/doc/acl2-doc.lisp for a proof of nil in ACL2 Version_6.3 that exploits this bug.

It had been possible to update a stobj (either an ordinary stobj or an abstract stobjs) so that it no longer satisfies its recognizer predicate. This soundness bug has been fixed. Thanks to Jared Davis and Sol Swords for pointing out this bug, making useful observations about the issue, and sending proofs of nil, one of which may be found in a Lisp comment in the defxdoc form for note-6-4.

Fixed a long-standing soundness bug (found at least as far back as Version 1.9!) in the checking done for congruence rules. There had failed to be a check that the new variable on the right-hand side of the conclusion is indeed new. The following example is shown in detail as a comment in function interpret-term-as-congruence-rule, ACL2 source file defthm.lisp, where it is used to prove nil in Version 6.3.

(implies (e y1 y2)
         (equal (h y2 y1)
                (h y2 y2)))

Fixed a bug in the ACL2 character reader that was causing an end-of-file error when reading from a string ending in "#\c", for c a character or non-terminating sequence of characters. Thanks to Jared Davis for sending the following example, whose evaluation in raw Lisp had caused an error.

(let* ((*readtable* *acl2-readtable*)
       (stream (make-string-input-stream "#\\a"))
       (x1 (read stream nil :EOF))
       (x2 (read stream nil :EOF)))
  (list x1 x2))

(GCL only) Improved the automatic proclaiming mechanism used for GCL builds, in particular to avoid computing a return type when a term is detected that could come from a call of non-exec, and to do a more complete job for calls of return-last.

(CCL only) A CCL bug was treating filenames of the form "~/user/..." as "~/...". Thanks to Gary Byers for sending us a CCL-specific form that is now included in the ACL2 sources, which avoids this problem.

Attempts to submit congruence rules had unfortunate consequences in the case that the function ``symbol'' is if or quote: for if, rules were appropriately ignored because of the special handling that ACL2 already gives to calls of if for congruence-based reasoning, while for quote, it was possible to get a hard Lisp error. Now, attempts to submit such rules will result in a clear ACL2 error.

It had been possible to get a confusing raw Lisp error when submitting a defstobj event whose first argument is not a symbol, as in: (defstobj (fld :type integer :initially 0)). That user error is now reported gracefully by ACL2.

When an include-book form is executed for a non-existent book, we no longer get a bogus warning about a missing compiled file. (Of course the compiled file is missing when the book itself is missing! So there's no need to report this fact.) Thanks to Caleb Eggensperger for bringing this issue to our attention.

Changes at the System Level

The ACL2 system documentation has been reworked for the xdoc framework developed by Jared Davis. While the ACL2 User's Manual can still be built, it is now possible for the ACL2 community to contribute to the ACL2 system documentation, in community book books/system/doc/acl2-doc.lisp; see comments near the top of that book. Now that both the ACL2 system documentation and much of the community books documentation are written in xdoc format, we hope the ACL2 community will add links from the ACL2 system documentation topics to book documentation topics. Note that :doc still works at the terminal, but it is based on the new system, and other terminal-based access to the documentation has been eliminated (for example :more). Thanks to Jared for all his work contributing to this enhancement.

Fixed community books books/Makefile-generic and also books/Makefile, which now has filename books/GNUmakefile, to work with Cygwin (Windows). Thanks to Harsh Raju Chamarthi for his substantial help.

The guard for system function ev-fncall-w now includes an arity check.

EMACS Support

There is now an Emacs utility for browsing the hypertext documentation for ACL2 and the community books. This browser, ACL2-Doc, essentially serves as a replacement for Emacs Info, which can no longer be used to browse the documentation. ACL2-Doc can be used not just for the ACL2 User's Manual but also for the ACL2+Books Manual. It is loaded automatically into Emacs if you load the file emacs/emacs-acl2.el. See ACL2-doc and documentation.

Experimental/Alternate Versions

(None to report this time.)

Subtopics

Note-6-4-books: Release notes for the ACL2 Community Books for ACL2 6.4 (January, 2013).