ACL2 Version 7.1 (May, 2015) 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.0 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.
The default build is hons-enabled, as for the previous release; but
the generated executable is now
See also note-7-1-books for a summary of changes made to the ACL2 Community Books since ACL2 7.0, including the build system.
For both add-include-book-dir and add-include-book-dir!,
the second argument is no longer evaluated (which we think could perhaps have
been exploited to get unsound behavior, by arranging for the value of the
second argument to depend on state). Moreover, that argument can not
only be a string, but also can be a sysfile: an object
The event summary had not been printed when a proof is interrupted (that is, with Control-C). Now, summary information is printed for two summary types (see for example set-inhibited-summary-types): rules and hint-events.
Type declarations for let and mv-let forms are now guard-checked. Consider for example the definition:
The ld special
A "Theory" warning is still printed when definitions of
certain built-in functions, such as mv-nth, are disabled;
similarly for some built-in executable-counterpart rules. However, we
now print such warnings only when the disabling occurs, rather than every time
an in-theory event or hint is evaluated. For example, if you evaluate
(SBCL only) ACL2 built on SBCL now reports bytes usage, both in time$ and in memsum, essentially exactly as has already been done for ACL2 built on CCL. Thanks to Jared Davis for suggesting this enhancement.
(SBCL only) Fast-alists can now be garbage collected (we believe) in SBCL, as they had already been done in CCL. (Implementation note: The change was to use weak hash tables in the implementation of SBCL fast-alists.) Thanks to Jared Davis for suggesting this enhancement.
The utility ec-call can now be applied to calls of symbols
introduced with defun-inline, or with define using keyword
(defun-inline foo (x) (cons x x)) (defun bar (x) (ec-call (foo x)))
The proof-builder is now sensitive to the current case-split-limitations.
The Common Lisp function sleep is now defined in ACL2. Thanks to Jared Davis for requesting this addition.
Custom error messages may now be created for guard violations. See set-guard-msg.
The new macro assert* is like assert$, except that
We fixed an inefficiency that could occur in calls of program-mode functions that update stobjs. See the discussion of invariant-risk in the documentation topic, program-wrapper. Thanks to Jared Davis for bringing this issue to our attention.
We improved the ``worse-than'' heuristic, providing modest speed-up and
eliminating the use of memoization for it. Thanks to Jared Davis for useful
discussions on the topic, and to Camm Maguire for an observation that led us
to do some investigations that led to this improvement. For more information
see comments in source function
We avoid the cost of translating ACL2 terms (see term) to user-level
syntax after applying the ``preprocess'' simplifier (see hints-and-the-waterfall), and also after applying either
We fixed an inefficiency that could occur in processing of make-event forms. Thanks to Sol Swords for reporting and diagnosing the
problem. (Technical note: The fix involves avoiding, in most cases, looking
up world global
We changed the heuristics for equality substitution so that so-called
cross-fertilization, where an equality substitution is made on only one
side of the goal's conclusion, is not made when generalization is turned off,
as with the hint
Some clause-building (essentially, goal-building) operations already avoided duplication, but now consider clauses to be ``duplicates'' when the only difference is commuted arguments of equal or iff. (Note: This change was made in support of assert* and mbt*, mentioned above.)
(SBCL only) It had been the case for host Lisp SBCL that the use of defun-inline to define functions in books had failed to result in inlined code, when those functions were called after including those books. This has been fixed (and appears not to have been a problem for host Lisp CCL). Thanks to Jared Davis for bringing this issue to our attention.
A potential soundness issue could result from the application of metafunctions and clause-processors: although ACL2 checked that their
outputs contain only legal terms, it did not check for the absence of
calls of certain ``forbidden'' function symbols. For example, sys-call
should be prohibited unless there is an active trust tag (see defttag),
but a metafunction was able to introduce a call of
The edited log below illustrates a bug that we have fixed, involving the
processing of include-book events in the certification world whose filename starts with the tilde (
~/temp/incl$ cat sub/bad.acl2 (include-book "~/acl2/acl2/books/arithmetic/top") ~/temp/incl$ acl2h [[.. output elided ..]] ACL2 !>(ld "sub/bad.acl2") [[.. output elided ..]] ACL2 !>(certify-book "foo" 1) HARD ACL2 ERROR in ABSOLUTE-PATHNAME-STRING-P: Implementation error: Forgot to apply expand-tilde-to-user-home-dir before calling absolute- pathname-string-p. Please contact the ACL2 implementors. ACL2 Error in TOP-LEVEL: Evaluation aborted. To debug see :DOC print- gv, see :DOC trace, and see :DOC wet. ACL2 !>
Fixed several issues with the
Fixed a bug in the proof-builder's
(Allegro CL only) Fixed a bug in trace!, which for example was
evidenced when evaluating
Fixed a bug in the printing of user-level terms that failed to account for
untrans-table entries for nth, update-nth, and update-nth-array, when printing the first argument as a symbolic constant
corresponding to a stobj argument. Thanks to Warren Hunt for reporting
this issue with an example much like the following. When submitting the forms
below, ACL2 output for the final form displayed the user-level term
(defstobj st fld) (defmacro !nth (x y z) `(update-nth ,x ,y ,z)) (add-macro-fn !nth update-nth) (thm (equal (update-fld v st) xxx) :hints (("Goal" :in-theory (disable update-nth))))
Fixed a failure to guard-check type declarations for let and mv-let forms. Consider for example:
(defun foo (x) (let ((a (car x))) (declare (type string a)) a))
Previously, the call
Fixed a bug in redundancy checking for mutual-recursion events that
The following bug was probably not observable, but violated our claim that
the system behaves as logically specified. When a guard check failed
during execution, the error message that was printed could differ slightly
from what is logically specified. (Technical detail: the error actually
printed by source function
We fixed the following two bugs in the processing of backchain limits stored for rules. Thanks to Dave Greve for bringing these to our attention.
Fixed a bug in the processing of certain operations on pathnames containing
By default, the ACL2 executable once again is named
Links from the home page to user's manual topics now point to the ACL2+Books combined manual, not the ACL2 (only) User's Manual, except for the one link that explicitly points to the latter. Thanks to David Hardin for feedback leading to this change, which was incorporated into the ACL2 Version 7.0 home page several days after the release of that version.
Garbage collection notification has been turned off by default, not only for ACL2(c) as before, but also for (the default build) ACL2(h). Thanks to Eric Smith for suggesting this change. See ACL2-customization and see gc-verbose for how to turn such notification back on in your own environment.
It is now possible to move the system books directory after certifying its
books, without invalidating their status as certified. Users should generally
not notice this change. We thank Harsh Raju Chamarthi and Camm Maguire for
reporting problems with hacks we have produced over the years to support
distribution of books with their certificate files. Those hacks are no
longer necessary: as a byproduct of this change, we have deleted both the
(SBCL only) Modified the handling of environment variable
Intended compiler optimizations are now guaranteed to be in place. We observed, thanks to communication from Jared Davis, that when ACL2 is built using SBCL 1.2.10, ACL2 starts up without the compiler optimizations that had been installed during the build. Perhaps that has been true for other SBCL versions or even other Lisps. Now, ACL2 explicitly restores those optimizations when it starts up. We observed a 5% time reduction for SBCL-based regression after this change.
(GCL only) A few tweaks were made in support of GCL changes starting with
pre-releases of GCL 2.6.13 in late April 2015 (but these tweaks are backward
compatible with older GCL releases). Resulting ACL2 builds for a new GCL show
dramatic speed-ups for a single user, perhaps cutting between a third and half
the time, with less dramatic improvements when running regressions with
We installed the following two patches to file
We made several improvements to the ACL2-doc Emacs browser for ACL2 documentation.
(For ACL2(p) users only; see parallelism) If parallel execution is
enabled (see set-parallel-execution), as it is by default in ACL2(p),