		Search-engine friendly clone of the ACL2 documentation.

Release-notes

Note-8-7

ACL2 Version 8.7 (xxx, 20xx) 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 8.6 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. See also note-8-7-books for a summary of changes made to the ACL2 Community Books since ACL2 8.6, including the build system.

Changes to Existing Features

The output generated by the induction routine has been slightly changed. Now, if term t0 suggested the induction scheme but other terms, t1, ... tk, either suggested the same scheme or schemes that merged with t0's to create the selected scheme, the induction output includes the sentence ``We will induct according to a scheme suggested by t0, while accommodating t1, ..., tk''. The terms mentioned are all preferentially expanded by the simplifier when they arise in the subgoals produced by that induction. The fact that the terms are preferentially expanded is not new. What's new is that ACL2 now lists all the accommodated terms.

When the summary prints “Modified system attachments”, it now sorts that information before printing it.

Improved the error message when the package name is missing immediately after `#!', as in #!(foo).

New Features

The new function symbol strict-table-guard returns its single argument unchanged, but has a special meaning when a table's :guard is a call of that function symbol. In that case, a term supplied for updating the table — that is, for the :put and :clear operations — must have no free variables, even though variables WORLD and ENS are normally permitted. See table.

A new feature provides ways to stop certain infinite loops in the waterfall. It is now possible to specify a limit on how many times the waterfall can produce a new subgoal along a branch. It is also possible to specify that the prover should check for ``simple'' loops in the waterfall. The default setting for this new feature limits the branch length to 1000 and enables checking for duplicate goals. See set-subgoal-loop-limits for details. Thanks to Eric Smith for suggesting that we consider supporting loop detection at the goal level.

A new feature provides help in debugging failed proofs involving functional instantiation. In particular, it helps you answer the question ``where did this subgoal come from?'' when looking at a subgoal produced by functionally instantiating a constraint. See set-constraint-tracking.

Heuristic and Efficiency Improvements

Applications that use functions with floating-point inputs or outputs (see df) may generate less memory usage, at least in SBCL releases strictly after SBCL Version 2.9 and SBCL github versions after mid-October, 2024. Thanks to Stas Boukarev for enhancing SBCL to support this improvement (made by adding suitable proclaiming in ACL2).

Avoided a potential quadratic blowup in guard generation by improving how guard obligations are simplified. Specifically, improved the simplification of ground subterms so that (if x y y) can simplify to y; other uses in ACL2 of ground subterm simplification similarly benefit. Thanks to Eric Smith for sending the following example, which now generates a simpler guard proof obligation.

(defun foo (x y)
  (declare (xargs :guard t))
  (let ((x (+ 1 x)))
    (case x
      (1 (natp x))
      (2 (consp x))
      (3 (rationalp x))
      (otherwise (+ x y)))))

Sped up include-book by significantly reducing time in translating calls of with-output and some other macros (for some technical details see ACL2 source function macroexpand1*-cmp and in creatiion of the so-called post-alist in a certificate (for relevant code, which shows the use of fast-alists, see ACL2 source function accumulate-post-alist.) For examples showing reduction by about 1/3 in include-book time, see the comment “Here are sample time reports (...) for include-book speedups due to...” in the form (defxdoc note-8-7 ...) in community-book books/system/doc/acl2-doc.lisp. Thanks to Eric Smith for sending an example book for which to speed up include-book.

When a function, constant, or macro was defined within an encapsulate form, its definition was evaluated in Lisp with each pass of evaluating the encapsulate form, and similarly for the definition of its executable-counterpart (see evaluation). For CCL and SBCL, that implies that such function definitions were compiled with each pass. Now, with a few exceptions, these definitions are saved in the first pass of evaluating the encapsulate form and retrieved, rather than re-evaluated, in the second pass. The exceptions include the following.

No definition is stored or retrieved that is within the scope of an encapsulate form with a non-empty list of signatures.
No definition of the executable-counterpart of a function symbol is retrieved when that symbol has a non-redundant logic-mode definition in the scope of local that was evaluated within the first pass of the same encapsulate.
No local definition is stored that is within two or more nested encapsulate events.

Thanks to Eric Smith for asking if a function defined within an encapsulate can be expected to be compiled twice, once for each pass of the encapsulate. Implementation-level details are explained in the section entitled “Appendix 2: Extension for Encapsulate” in the ACL2 source code comment, “Essay on Hash Table Support for Compilation”.

Bug Fixes

Fixed a soundness bug in the proof-builder that could cause goals from forced hypotheses to be created incorrectly. (This bug has been around for at least 10 years and probably for 30 years!)

Fixed a soundness bug based on the use of swap-stobjs on two stobjs of which one is “live”. See live-stobj-in-proof. Thanks to Sol Swords for reporting this bug, including an example and analysis of possible fixes in his report.

Fixed a soundness bug due to the interaction of stobjs and defattach. The fundamental problem was that defattach events can cause a stobj recognizer to become false; see community-book books/system/tests/stobj-attach-unsoundness.lisp. The solution is to disallow attachments for certain supporters of stobj primitives; see stobj-attachment-restrictions. Thanks to Sol Swords for reporting the bug, analyzing it quite thoroughly, contributing the book mentioned above, modifying other books as necessary, and providing preliminary code to fix the bug, and for helpful conversations.

A Lisp error is now avoided when saving event-data (see saving-event-data and submitting certain ill-formed attempts at events. Thanks to Eric Smith for sending the following example.

(assign event-data-fal 'event-data-fal)
(defuns foo (x) x)

Fixed a bug in the interaction of memoize-partial with utilities save-and-clear-memoization-settings and restore-memoization-settings. The latter utilities no longer have an effect on functions created by memoize-partial (or, and this is quite obscure, on memoization from calls of memoize with a non-nil value of the keyword, :total).

An attachable stobj (see attach-stobj) was created by the executable (:EXEC) function associated with its stobj creator (see defabsstobj), even when that stobj was given an attachment. This bug has been fixed: the stobj is now created by the :EXEC of the attachment's creator.

Fixed a bug in trans* when its use encounters a call of make-event with the :on-behalf-of keyword. Thanks to Grant Jurgensen for reporting this bug using a simple example.

According to the documentation for table, the variable ENS is allowed in both the key and value expressions when updating the table, that is, using the :put and :clear operations. However, ENS was not being allowed in the key expression. That has been fixed.

(SBCL only) Fixed a bug, for ACL2 hosted on SBCL, that was preventing inlining of functions whose name ends in "$INLINE", such as those generated by defun-inline. Thanks to Grant Jurgensen for reporting this bug with a helpful example.

A defabsstobj event contains function specs that are each either a symbol or a list of the form (fn :kwd1 val1 ... :kwdn valn). Each vali must be a symbol, but when this was not the case, a raw Lisp error could occur. Now a clean error message is printed, and this requirement on the vali has been made explicit in the documentation for defabsstobj.

ACL2 rejected some valid :type fields in defstobj forms. This has been fixed; see defstobj, where the “Remark on SATISFIES” has been extended to describe the requisite guard verification. Thanks to J. David Taylor for reporting this issue (as Issue 1852 in the ACL2 GitHub repository) and including the following examples that ACL2 rejected (but now accepts).

(defstobj st
  (a :type (complex rational)
     :initially #c(0 1)))

(defstobj st (a :type (string 1)
                :initially "a"))

The following additional example from Issue 1852 is still rejected, because evenp has a non-trivial guard; its argument must be an integer.

(defstobj st (a :type (satisfies evenp)
                :initially 0))

However, the following variant produces a term, (and (integerp x) (evenp x)), that is trivially guard-verifiable, so it is accepted by ACL2 (but was not accepted before the bug fix).

(defstobj st (a :type (and integer (satisfies evenp))
                :initially 0))

Fixed a bug that was causing errors for stobjs introduced with defstobj keyword argument :non-executable t in the presence of large arrays. This should not have caused an error, since that keyword argument prevents attempts at contructing the stobj (with its arrays).

Fixed a bug in :pr to work on function symbols introduced by defstobj (GitHub Issue 1851). Thanks to David Taylor for reporting this bug.

Fixed a proof-builder bug that could occasionally cause two goals to exist with the same name.

The :native option of trace! and trace$ did not work as one would reasonably expect when SBCL is the host Lisp; now it does.

Some ill-formed hard errors, for example from calls of er, caused raw Lisp errors. This has been fixed. Thanks to Eric Smith for reporting this bug with an example.

Changes at the System Level

Modifications have been made that allow ACL2 to be hosted on GCL Version 2.7.0 and presumably later gcl versions; previously only GCL versions before 2.7.0 could host ACL2. Essentially the only user-visible change (other than error prevention) is the introduction of list$, a macro equivalent to list that can be used without a GCL 2.7.0 restriction on the number of arguments. The most sweeping implementation-level change is the replacement of an array in support of so-called static honses, the sbits array, by a structure that avoids a reduced bound on array dimensions imposed by GCL 2.7.0. Details may be found in a Lisp comment in the form (defxdoc note-8-7 ...) in community-books file books/system/doc/acl2-doc.lisp. Thanks to Camm Maguire for his help with this project, including (but by no means limited to) his contribution of a new sbits implementation.

The ACL2-only manual is no longer advertised on the ACL2 home page. The ACL2+Books manual is favored both because it does not have the broken links found in the ACL2-only manual and because the ACL2+Books manual is helpful for informing new users about the libraries provided by the community-books. Thanks to Eric Smith for encouraging this change. Note that the ACL2-only manual may continue to be built in directory doc/manual/ when certifying books/system/doc/acl2-manual.lisp. (Directory doc/manual/ is not to be confused with books/doc/manual/, where the ACL2+Books manual is built.)

For the built-in :doc command at the terminal: changed the top topic of that “acl2-only” manual from ACL2 to TOP. The structures of the documentation trees for that version of the manual and the usual ACL2+Books manual are now consistent. Thanks to Eric Smith for suggesting that those two manual structures be consistent.

Replaced information about mailing lists in the installation instructions using a link to a corresponding, new documentation topic, mailing-lists. So now, the community can make suitable updates to that page. Thanks to Eric Smith for suggesting this change.

The installation instructions have been moved into the manual; see installation. Thanks to Eric Smith for suggesting this change, which will allow the ACL2 community (specifically, the acl2-books community) to improve those instructions.

By default, the directory where an ACL2 executable is to be built must not have a pathname that contains spaces, as before. However, now there is a variable, ACL2_ALLOW_SPACES_IN_DIRECTORIES, that may be set to a non-empty value in order to build an ACL2 executable in such a directory, as noted in the error message. That message points out that there may be errors, however, when certifying books. Thanks to Eric Smith for a discussion leading to this change.

References to the old “bleeding edge” manual (https://www.cs.utexas.edu/users/moore/acl2/manuals/latest/') have been replaced by references to the new one (https://acl2.org/doc/).

The documentation for do-loop$ has been extended to illustrate how to signal a soft error from within the body of a DO loop$ expression.

EMACS Support

Experimental Versions

Subtopics

Note-8-7-books: Release notes for the ACL2 Community Books for ACL2 8.7
Whats-new-in-ACL2-2025: Notes for “What's New in ACL2” at ACL2 Workshop 5/12/2025