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.
Gag-mode no longer saves prover output when
When include-book fails to find a readable certificate
(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
Fixed a bug in an ACL2 system function,
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
A new output type,
The restrictions on utilities
The table guard on dive-into-macros-table has been strengthened in order to avoid calling untouchable functions (see remove-untouchable).
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
(None to report this time.)
Fixed a soundness bug in the handling of hypotheses of conditional
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
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
(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
(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
Attempts to submit congruence rules had unfortunate consequences in
the case that the function ``symbol'' is if or quote: for
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:
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.
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
Fixed community books
The guard for system function
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.
(None to report this time.)