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
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
The default build is hons-enabled, as for the previous release; but
the generated executable is now saved_acl2, as discussed below. Please
note that ACL2(c) (``classic ACL2'', i.e., ACL2 that is not hons-enabled) now builds as saved_acl2c, is deprecated, and will likely
be unsupported or even eliminated in future releases.
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.
Changes to Existing Features
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 (:system
. filename), where filename is a file name. When filename is a
relative pathname, the meaning of such an object is the file with that
pathname under the system books directory.
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
By default, (memsum) is now truncated to 100 entries rather than to 20
entries. (Implementation note: raw Lisp variable *memoize-summary-limit*
is 100 instead of 20.)
Calls of THE no longer cause a guard violation when
guard-checking is nil. Also see the and see set-guard-checking.
Type declarations for let and mv-let forms are now guard-checked. Consider for example the definition: (defun
foo () (let ((x t)) (declare (type integer x)) x)). Previously, evaluation
of the call (foo) had failed to result in a guard violation error; now,
it does, provided guard-checking is on (i.e., not nil or :none; see
The symbols ctx, hist, pspv, unquote, and value
have been added to *ACL2-exports*. Thanks to Jared Davis for
suggesting these additions.
Consider :use or :by hints in which a variable bound using
the :instance keyword is in the wrong package. For example, for the hint
:use ((:instance foo (x 3))), suppose that the lemma foo mentions
the variable bar::x, but not x. This situation formerly caused an
error, but now, x indicates the variable bar::x from the lemma
foo. See lemma-instance, in particular Condition (4), which has
been updated accordingly. Thanks to David Rager for a remark that led us to
implement this enhancement.
The ld special ld-error-action may now have a value (:exit
N), where N is a natural number. If an error occurs for a call of
ld, then this value causes the ACL2 process to quit with exit status
N. See ld-error-action. Note that ld-error-action is set to
this new value when using the cert.pl utility provided with the community
books; see build::pre-certify-book-commands. Thanks to David Rager for
presenting an example showing how this change can make it easier to locate
certain certification failures, and thanks to Sol Swords for helping in the
design of this enhancement.
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
(in-theory (disable mv-nth)) followed by (in-theory (disable
append)), then the second event will no longer produce a warning about
mv-nth. Thanks to Eric Smith for (most recently) suggesting such a
(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
argument :inline t, thanks to a request from Jared Davis. For example,
the following is now legal.
(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
assert* only generates a guard proof obligation, not a runtime
check. Assert* is defined using a new macro mbt*, which is a
variant of mbt: a call of mbt* logically returns t, but
generates the same guard proof obligation as mbt. Thanks to
Shilpi Goel for a query that led us to add these macros.
Heuristic and Efficiency Improvements
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 worse-than-builtin-clocked (source file
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 :use or
:by hints. Thanks to David Rager for helpful discussions towards
this change. Note: On rare occasions, this might change the prover flow as
- Consider the case that the input goal, "Goal", simplifies with the
``preprocess'' simplifier to a new goal that prints the same as "Goal".
Formerly, this case avoided labeling the new goal as "Goal'"; it was as
though the new goal was actually the user input. The new criterion for
avoiding "Goal'" is somewhat weaker: the internal syntax must suitably match
for "Goal" and its simplification, rather than their displayed forms.
- Consider the application of a :use or :by hint. In such cases,
the resulting constraint (if any) is simplified with the ``preprocess''
simplifier. Formerly, the rules used by that simplifier were not recorded if
the printed version of the simplified constraint was equal to the original
constraint, which was really a bug since the comparison was between the
user-level syntax of the simplified constraint and the internal syntax of the
original constraint. Now, ACL2 compares the internal syntax of each.
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 'boot-strap-flg by using a new state global instead of
the same name.)
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 :do-not '(generalize). Instead, the equality is used
throughout the goal in that case. Thanks to David Hardin for bringing an
example to our attention that led us to make this change.
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
(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 sys-call. We have
added the necessary checks, in a way that we hope has negligible impact on
performance. To avoid that impact or to learn more about this issue, see
set-skip-meta-termp-checks; this new utility, which requires a trust
tag, avoids not only the new checks but even the above-mentioned checks for
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 (~) character.
~/temp/incl$ cat sub/bad.acl2
[[.. 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.
Fixed several issues with the :puff command, and updated its
documentation accordingly. See puff.
Fixed a bug in the proof-builder's wrap command. Thanks to
Keshav Kini for sending a simple example that illustrated this bug.
(Allegro CL only) Fixed a bug in trace!, which for example was
evidenced when evaluating (trace! (nth :native t)).
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
(update-nth *fld* v st) instead of the expected form, (!nth *fld* v
(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)
: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))
Previously, the call (foo '(3 4)) did not cause a guard violation,
even though it should have done so. (Indeed, the event (verify-guards
foo) failed, and continues to fail.)
Fixed a bug in redundancy checking for mutual-recursion events that
specify :ruler-extenders in an xargs declare
form. Thanks to Sol Swords for sending an example that illustrates the bug: a
mutual-recursion event that, when executed twice, caused an error the
second time rather than being redundant (see redundant-events). The
bug was actually in how ACL2 stores information about the ruler-extenders used in definitions: the :ruler-extenders specified for
the first defun was being mistakenly stored for the second defun.
This mishandling of redundancy for mutual-recursion events appears to
be the only consequence of that bug.
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 ev-fncall-rec was appropriately showing the
original guard, but the specification function ev-fncall-rec-logical was
showing the untranslation of the translated guard.) This has been fixed.
The save and retrieve commands for the proof-builder (see
ACL2-pc::save and ACL2-pc::retrieve) now cause an error when the
supplied name is not a symbol; similarly for the :event-name argument of
verify. The behavior wasn't as expected for non-symbol names; for
example, after issuing the instruction (save 'abc) in the proof-builder, the command (retrieve 'abc) failed to resume the
proof-builder session. (Notice the erroneous use of the quoted symbol
'abc, i.e., (quote abc), rather than of the symbol abc.)
Thanks to Keshav Kini for bringing this problem to our attention.
We fixed the following two bugs in the processing of backchain limits
stored for rules. Thanks to Dave Greve for bringing these to our
Fixed a bug in the processing of certain operations on pathnames containing
Changes at the System Level
By default, the ACL2 executable once again is named saved_acl2, though
unlike previous versions, this executable is hons-enabled.
Correspondingly, the ACL2(c) executable (that is, the executable that is not
hons-enabled) is by default saved_acl2c. Thanks to David Hardin
for suggesting these changes.
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
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
community-books directory books/fix-cert/ and the source function
make-certificate-file-relocated. For a bit more detail see the final
remark in the topic full-book-name. We also thank Eric Smith, Jared
Davis, and Sol Swords for reporting bugs in our initial implementations of
The certify-books target for make now excludes other expensive
directories in addition to workshops.
(SBCL only) Modified the handling of environment variable SBCL_HOME.
Thanks to Jared Davis for pointing out a problem leading to this change,
namely, failure on his platform when evaluating (require :sb-sprof) in
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.
Environment variable ACL2_WRITE_PORT is now ignored when doing provisional-certification. Thanks to Sol Swords for discussing this issue,
which arose from a failure in community-books directory
books/workshops/2011/verbeek-schmaltz/sources/, which uses provisional-certification.
(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 -j
8. Thanks to Camm Maguire for pointing us to the changes and for improving
The commands Control-t e and Control-t Control-e, defined in file
emacs/emacs-acl2.el, now check that the *acl2-shell* buffer exists,
has a live process, and has a last line matching the specification in
*acl2-insert-pats*, which has Emacs documentation (using Control-h
v) but is set to a default based on shell prompts. Thanks to David Rager,
Jared Davis, and Shilpi Goel for helpful discussions leading to this
We installed the following two patches to file emacs/emacs-acl2.el,
both contributed by Keshav Kini.
- Emacs highlighting for forms starting with "(def" now works when
the "def" symbol has a package prefix, for example,
- The Control-d character is no longer explicitly bound to the default,
delete-char, but instead is unbound in comint-mode-map, so that the
global binding of Control-d will take effect. Thus, users who bind Control-d
themselves will no longer have that binding overridden in shell-mode (or
We made several improvements to the ACL2-doc Emacs browser for ACL2
- Fixed a bug that could occur when Emacs variable
large-file-warning-threshold is nil. Thanks to Bob Boyer for
bringing this bug to our attention.
- Links are now in color (blue, by default). See ACL2-doc for
instructions on how to change or remove this color. Thanks to Jared Davis for
suggesting the use of color. We are open to suggestions for improvements;
this might be just a first step.
- Allow limiting search and index commands to ancestors (sub-topics,
sub-sub-topics, etc.) of a command (including the command itself), by
supplying a prefix argument.
- New "p", "<", and Control-TAB commands are analogues of
"n", ",", and TAB — for search, index, and next-link
commands, respectively — to go backward instead of forward.
(For ACL2(p) users only; see parallelism) If parallel execution is
enabled (see set-parallel-execution), as it is by default in ACL2(p),
then hons-wash and hons-clear may be no-ops (other than to print a
warning), in order to avoid thread-unsafe behavior. (However, In CCL you are
unlikely to see this restriction unless you are running more than one thread.)
To get around this restriction, you can instead use hons-wash! or
hons-clear!, which however require a trust-tag. Thanks to Bob
Boyer for bringing this issue to our attention.
- Release notes for the ACL2 Community Books for ACL2 7.1 (May 2015)