ACL2 Version 8.6 (xxx, 20xx) 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 8.5 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
Note that only ACL2 system changes are listed below. See also note-8-5-books for a summary of changes made to the ACL2 Community Books
since ACL2 8.5, including the build system. Also note that with each release,
it is typical that the value of constant *ACL2-exports* has been
extended, and that some built-in functions that were formerly in :program mode are now guard-verified :logic mode
Changes to Existing Features
The connected book directory (that is, the cbd) now elaborates
relative pathnames to absolute pathnames not only for book operations,
but for all file operations. For example, (open-input-channel
"foo" :character state) now interprets filename "foo" relative to
the cbd, where formerly it was generally interpreted relative to the directory
in which ACL2 was invoked. (Technical note: ACL2 accomplishes the new
behavior by arranging that set-cbd modifies not only the cbd but also
the Lisp global, *default-pathname-defaults*.) Thanks to Alessandro
Coglio, Eric McCarthy, and Eric Smith for suggesting consideration of such a
change and for helpful discussions.
The function hons-enabledp is no longer defined, and :hons has
been removed from the Lisp global, *features* (so, readtime conditionals
#+hons and #-hons should be avoided, especially since #+hons is
always false even though the system is hons-enabled). These were both
deprecated in the preceding release (ACL2 Version 8.5). Note that the hons-enabled features of ACL2 have been included in all builds by default
since Version 7.0 (January, 2015) and in all builds since Version
7.2 (January, 2016).
The proof-builder now takes into account various aspects of
rewriting specified by the logical world that it formerly
ignored (pertaining to match-free, case-split-limitations, untouchable functions, non-linear arithmetic (see set-non-linearp),
the backchain-limit for rewriting, and the rw-cache-state).
The utilities set-inhibit-er-soft, set-inhibit-er-soft!,
toggle-inhibit-er-soft, and toggle-inhibit-er-soft! have been
renamed by dropping the suffix ``-soft'', hence they are now the
following, respectively: set-inhibit-er, set-inhibit-er!,
toggle-inhibit-er, and toggle-inhibit-er!. The relevant table has
similarly been renamed from inhibit-er-soft-table to
inhibit-er-table. These changes reflect their relevance for the new
utilities, er-hard and er-hard, in addition to er-soft.
The macro warrant now forces the warrants listed.
:Induction rules now support the use of syntaxp
The utility read-file-into-string has been improved in the
- The value of the :start argument may now be any natural number less
than the length of the input file. (Formerly one needed to use this utility
to read the preceding bytes first, which can be much slower.) Thanks to Eric
McCarthy, Eric Smith, and Grant Jurgensen for requesting this improvement and
for helpful discussions.
- While the default behavior is the same for when the corresponding Lisp
stream is closed, a new keyword argument, :close, can be supplied to
control that behavior.
- Miscellaneous clean-up has been made in the implementation.
The trace$ option :evisc-tuple :print, which continues to use
raw Lisp printing, has undergone the following improvements when printing
entry and exit values. Thanks to Eric McCarthy for a query that led to these
- Values are now pretty-printed.
- Array values are no longer displayed as stobjs. (This includes
stobjs themselves, since they are arrays.)
The use of (:executable-counterpart rewrite-lambda-modep) to control
the behavior of lambda object rewriting by the prover (see rewrite-lambda-object) has been elaborated.
Warnings for non-recursive functions in left-hand sides of rewrite rules
(similarly for linear, forward-chaining, and type-prescription rules) now
consider bodies of lambda objects that could be rewritten (see rewrite-lambda-object).
The output is more informative when :pr is applied to an
undefined primitive, such as car or binary-+, or a macro-alias for
one of those, such as +. Thanks to Eric Smith for pointing out odd
output for examples like :pr binary-+.
The definition of pseudo-termp has been simplified by dropping a
superfluous true-listp check. Thanks for the suggestion from Eric
Smith. A new lemma, pseudo-termp-consp-forward, has been added to
prevent some existing proofs from failing due to the change.
The failure message regarding useless-runes (see useless-runes-failures) has been restricted to the case that a proof was
attempted by the event (though there may be rare exceptions). Thanks to Eric
Smith for requesting such a change.
Certain guard proof obligations for DO loop$s (so-called
special conjectures (e), (f), and (g)) have been combined into one conjecture
with a conjunction of three conditions in the conclusion to speed up proofs.
See the comment starting with ``Special conjectures (e), (f), and (g)'' in the
function special-conjectures in the source file
The rewriter has been changed to handle certain calls of ev$ faster.
A few new lemmas have been added to the standard apply$ book to
simplify applications of assoc-equal-safe faster.
The new zero-ary attachable system function, heavy-linear-p, allows
for enhanced use of linear-arithmetic during rewriting, specifically
with the test (first) argument of a call of IF. Thanks to Eric Smith for
suggesting the development of such a feature, which can be useful in
There is a new `make' target to build an ACL2 executable using
save-exec. See save-exec, in particular the new discussion at the
end of that topic. Thanks to Eric Smith for requesting such a utility.
New utilities get-cpu-time and get-real-time return the cpu
time and real (wall clock) time that has elapsed since the start of the ACL2
session. Thanks to Eric McCarthy for suggesting the addition of such
The new utility er-hard is analogous to er-soft, but for
hard errors instead of soft errors (see er). At the moment the only
summary string used for inhibiting hard errors is "Call depth", for
rewriter stack overflows. On a related note, a new soft error summary string
is used for inhibiting soft errors, "Evaluation".
A new command, :tc (translate and clean), has been added. It
translates a given form and then ``cleans it up'', returning a logically
equivalent but often simpler term in which logically irrelevant but
operationally important tags have been removed. The variants :tca and :tcp use different degrees of ``cleaning.'' These are
particularly useful for seeing the logical meanings of loop$ terms as
well as terms involving mbe and return-last.
A directory of books may now be relocated so that those books are
still treated as certified. This is supported by a new project-dir-alist, which associates keywords with ``project directories'' and
is set using environment variable ACL2_PROJECTS; see project-dir-alist. By default, the project-dir-alist has only one
entry, which associates the keyword :SYSTEM with the community-books directory, books/. The project-dir-alist
generalizes the notion of system books directory, assigning meaning to the
:dir argument of include-book and ld and to sysfile arguments of add-include-book-dir and add-include-book-dir!. Thanks to Sol Swords for requesting such a capability
and for helpful design discussions. (Technical Note: Implementation-level
changes are summarized in comments in the form (defxdoc note-8-6 ...) in
A new break-rewrite command, :pot-list, shows the list of the
polynomials that are assumed in the current context. See brr-commands
and see brr@. Thanks to Alessandro Coglio and Eric Smith for
conversations leading to this enhancement.
It is now possible to cause make-event to do proofs during its
expansion phase even in a context where proofs are generally skipped (see
ld-skip-proofsp). See make-event, in particular the discussion
there labeled as “(4)”. Thanks to Eric Smith for requesting such
The induction mechanism in the prover can now deduce induction suggestions
from some DO loop$s. See loop$-proofs for a brief
A new :linear rule, acl2-count-car-cdr-linear, is now
built into ACL2, as follows. Thanks to Eric Smith for suggesting this
improvement (slightly renamed here) to what we originally added.
(implies (consp x)
(equal (acl2-count x)
(+ 1 (acl2-count (car x))
(acl2-count (cdr x)))))
The Common Lisp utility, macrolet, is now supported in ACL2.
Thanks to Alessandro Coglio for discussion leading us to make this addition.
Heuristic and Efficiency Improvements
Fixed a bug in system function bounded-integer-listp, which may have
allowed illegal proof-builder commands to be attempted. Thanks to
Grant Jurgensen for pointing out this bug.
Consider calls of defthm and thm that create subgoals
before reverting to prove the original goal by induction. The Rules summary
printed at the end should exclude rules used only before the start of that
induction proof. That was formerly the case for defthm but not thm,
but now it is the case for both. You can see the change for the following
call, whose Rules summmary formerly included (:ELIM CAR-CDR-ELIM) but no
longer does so.
(equal (append (append x y) z)
(append x y z))
:expand ((:free (b) (append x b))
(:free (a b) (append (cons (car x) a) b))))))
Fixed bugs in the definition of source macro position-ac. Thanks
to Eric Smith for pointing them out.
Fixed translation of DO loop$ expressions, so that the
next-to-last argument of the resulting do$ call quotes the
untranslated measure instead of the translated measure.
Several improvements were made to the FOR loop$ utility (also
see for-loop$, to reflect more accurately the Common Lisp loop
utility. This matters because in guard-verified code, loop$
becomes loop. Here are the most user-visible such changes.
- Run-time guard-checking for loop$ operators SUM and
APPEND did not include a check that the value produced at each iteration
is a number or true list, respectively. That has been fixed so that, for
example, the expression (loop$ for v in '(1 a 2) sum v) now causes a
guard violation (because a is not a number), where previously it did
- For a form (loop$ for tail on lst ...), the target term, lst, no
longer needs to satisfy true-listp. For example, the form (loop$
for tail on '(a b . c) collect tail) no longer causes a @(see guard)
<li>Run-time @(see guard)-checking for an expression @('(loop$ for tail on lst
...) now includes a check for the target, lst, that its final
tail (i.e., , (last-cdr lst) satisfies the declared type of the
corresponding iteration variable. For example, evaluation of the loop$ expression below now produces a guard violation as shown, but it
formerly did not produce a guard violation.
ACL2 !>(loop$ for tail of-type cons on '(a b c) collect tail)
ACL2 Error [Evaluation] in TOP-LEVEL: The guard condition
(CONSP LOOP$-LAST-CDR), which was generated from a type declaration,
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.
To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.
Corresponding run-time checking was added for the types of the lower and upper
bounds lo and hi, the increment inc, and the last value tested,
in expressions (loop$ for i from lo to hi by inc ...).
Fixed a low-level bug in source function
translate-declaration-to-guard1-gen that was incorrectly creating
untranslated terms in some cases from type declarations of the
form (type (signed-byte _) _) or (type (unsigned-byte _) _). Here
is an example of an event that is rejected without the bug fix.
(defun foo (n)
(apply$ (lambda$ (x)
(declare (type (signed-byte 8) x)
(xargs :guard (signed-byte-p 8 x) :split-types t))
(+ 3 x))
Changes at the System Level
The `make' target, save-exec, now builds custom-saved_acl2
unconditionally. Thanks to Grant Jurgensen for pointing out (in GitHub Issue
#1422) that there can be untracked implicit dependencies that make this
Implementations underlying the functions sys-call, sys-call+, and sys-call* have been cleaned up. In particular, we now
expect them to indicate precisely the case of a non-error process return as
follows: 0 for sys-call-status, and nil for the first return
value of sys-call+ and sys-call*. Also, a bug has been fixed for
sys-call+ in the case of GCL as the host Lisp. Thanks to Eric Smith
for queries leading to these changes.
Significantly extended documentation topic system-attachments, which
now lists all built-in system attachments, many with brief documentation.
Thanks to Eric Smith for suggesting this enhancement.
- Release notes for the ACL2 Community Books for ACL2 8.6