Note-7-4
ACL2 Version 7.4 (March, 2017) 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 7.3 into the
following categories of changes: existing features, new features, heuristic
and efficiency 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.
Note that only ACL2 system changes are listed below. Changes to the books can be found by browsing the ACL2+Books GitHub repository, in
particular, the raw commit log. Also note
that with each release, some built-in functions that were formerly in
:program mode are now guard-verified :logic
mode functions.
Changes to Existing Features
The utility read-file-into-string is now a macro, not a function.
It no longer takes state as an argument (though its expansion reads the
state), and it has new keyword arguments that allow one to read successive
segments of the file. See read-file-into-string.
The test has been slightly relaxed for determining whether any supporting
events are missing for defabsstobj. Thanks to Sol Swords for sending
an example to illustrate the issue, together with analysis of the problem.
New Features
Heuristic and Efficiency Improvements
We now avoid the invariant-risk slowdown in the case of a
:logic mode function with guard t. For relevant examples
see program-wrapper.
A technical change in the handling of type-set computations can, in
rare cases, result in better built-in type-prescription rules for
functions.
Bug Fixes
Fixed a soundness bug, introduced about 10 years ago, that could occur with
:use or :by lemma-instances when a variable occurs free in a
lambda of a functional substitution. For an explanation see a comment in
(defxdoc note-7-4 ...) in community book
books/system/doc/acl2-doc.lisp; also, a proof of nil (in Version
7.3) that exploits this bug can be found in a comment in the definition of
function remove-capture-in-constraint-lst in the ACL2 source code. This
may be the first time that a proved ``theorem'' in the community-books
has been discovered to be a non-theorem (tr-to-array-of-array-to-tr in
books/projects/legacy-defrstobj/typed-records.lisp). Thanks to Sol
Swords for pointing out that this directory of books isn't used elsewhere; we
temporarily excluded it from the regression by adding a cert_pl_exclude
file, until Sol Swords repaired the proof a couple of days later. Also thanks
to Ruben Gamboa for fixing proofs in the nonstd/ books that failed after
the bug fix.
Fixed a bug in proof-builder commands x and expand, which
usually gave a misleading error message when attempting to expand a
constrained function.
Fixed bugs in the tracking and disabling of compound-recognizer
rules. Thanks to Dmitry Nadezhin for pointing out this bug, indeed, sending
an example and analyzing it to point to system function
term-and-typ-to-lookup, which was indeed the one that had the bug.
Avoided a rare error in hons-wash that has happened when there is a
second garbage collection after hons-wash has commenced. Thanks to
Keshav Kini for telling us about the problem and providing a patch, which we
used almost verbatim.
Changes at the System Level
An ACL2 customization file is no longer loaded by default (when it exists)
when invoking `make' from the top-level ACL2 directory. This change is
not necessary for `make regression' because the build system for the
books already takes care of it. However we need this change for `make
DOC', at the least; thanks to Eric Smith for bringing our attention to a
failure of `make DOC'.
(Really a books change, but affects building the manual:) By default, it is
now an error if when saving the ACL2+books or ACL2-only manuals (web-based or
text-based), a syntax error (marked by ``xdoc error'') is encountered. See
xdoc::save and xdoc::save-rendered: both now have an error
argument with default nil so that by default, those new errors are not
signaled; but in accordance with the change above, that new error argument is
t for the standard ways of building the ACL2+books and ACL2-only manuals.
Also, two arguments have been eliminated for xdoc::save-rendered.
An invocation of `make update' to build an ACL2 executable initiates a
build only when necessary (that is, when at least one source file or
supporting file, like GNUmakefile, has changed). Thanks to Eric Smith
for the suggestion. Removed the following `make' targets, which were
suspect after this change (the first definitely no longer worked) and are
unnecessary: saved_acl2, saved_acl2p, saved_acl2r, and
saved_acl2pr. WARNING: make update should be used with care, since
it does not rebuild the desired executable when it already exists and is more
recent than the sources. For example, if you change Lisp implementations
without changing the PREFIX variable — perhaps even only changing
the version of your Lisp — then use make or make large, not
make update.
New `make' target clean-all removes all generated files in the
main ACL2 directory and its doc/ subdirectory, while existing target
clean, which has been renamed clean-lite, cleans all of those except
files *saved_acl2* (and doc.lisp.backup), essentially as before.
Thanks to Eric Smith for suggestions leading to this change, and to Keshav
Kini for suggesting consideration of target distclean as an alias for
clean-all, which it now is. The target clean is deprecated but,
consistent with prior usage, acts as clean-lite for now.
A successful build using `make' shows only four lines for 'fgrep -i
compiler make.log' instead of five.
(GCL only) Installed a patch from Camm Maguire (GCL maintainer) to fix a
GCL compiler bug. Also turned off SGC to avoid an ``mprotect failure'' error
(community book books/centaur/fty/tests/deftagsum-scale.lisp).
Fixed a bug that was causing an assertion failure, instead of a clean
error, when attempting to apply :monitor to undefined primitives,
e.g., :monitor cons t. Thanks to Keshav Kini for reporting this bug and
sending us an initial fix.
Fixed a bug in the break-rewrite commands :go! and :go$,
which was causing an error message to be printed.
EMACS Support
Made minor ACL2-doc improvements: fixed a bug in `u' command's
error message when already at the top topic; fixed a bug that was displaying
the "Parent list:" field in reverse order; and eliminated the warning when
loading a large manual (combined manual is at about 70M bytes now; new
threshold is 80M bytes).
Improved ACL2-doc to work with other manuals; see ACL2-doc,
specifically Section ``Selecting a Manual''. Note that the command for
initially bringing up the ACL2 User's Manual, instead of the ACL2+Books
manual, has changed from (defvar *acl2-doc-top-default* 'TOP) to
(defvar *acl2-doc-manual-name* 'acl2-only).
Added new ACL2-doc commands, `/' and `W', to go to an ACL2
definition. By default the search is through both the ACL2 sources and books.
The search can be continued even outside acl2-doc by using a numeric prefix
argument with control-t /, which is just the `/' command made
available outside acl2-doc. These two commands differ only in the defaults
presented in the minibuffer. The default for `/' is based on the text at
the cursor. (This is much like the similar built-in Emacs command,
meta-.; indeed, `/' is next to `.' on standard keyboards.) For
`W', the default is based on the page's topic name (as shown by the
`w' command). See ACL2-doc for details.
Installed a patch for control-t control-e from Keshav Kini, so that
when there are more than two windows and one has the ACL2 shell buffer
showing, then that one receives the form. Consider for example windows A, B,
and C, where the cursor is showing in A and the shell buffer is showing in C.
Previously, the shell buffer could be placed in B to receive the form. Now,
the form will go into C.
The :evisc-tuple keyword for trace$ was being ignored when
:native t was also supplied. Since the use of :native t sends the
tracing command to raw Lisp, this wasn't really a bug, since no raw Lisp we
know of supports the :evisc-tuple keyword. However, we have improved our
custom modifications of the native trace for host Lisps CCL and Allegro
CL so that :evisc-tuple is no longer ignored for these Lisps.
Experimental Versions
A new rewrite rule for ACL2(r), realp-implies-acl2-numberp, is
analogous to the existing rule rationalp-implies-acl2-numberp. Thanks to
Dmitry Nadezhin for suggesting the addition of this rule, which he observed is
necessary for some ACL2(r) proofs.
