Whats-new-in-ACL2-2025
Notes for “What's New in ACL2” at ACL2 Workshop 5/12/2025
These release notes are derived from documentation topics note-8-6 and note-8-7 that were added between the November 2023 and
May 2025 ACL2 Workshops. Each release note included below is included in its
entirety, with this color providing emphasis and
this color used for text that has been added.
Part 1 (Matt Kaufmann)
In gag-mode (which is on by default), when the prover notes that a
forcing round is pending, it now lists the names of the rules that are
responsible.
Example:
Forcing Round 1 is pending (caused first by applying ACL2P-IS-ACL2
and ZMIRROR-IS-MIRROR to Goal).
ACL2 versions of Lisp ‘fixnum’ notions have been made more
generous. Specifically, the value of *fixnum-bits* has been increased
from 30 to 61, which has increased the value of (fixnum-bound) from
2^29-1 to 2^60-1. Thanks to Eric Smith for requesting an increase. One
effect of this change is to increase the value of *default-step-limit*
accordingly, so that the steps computed by with-prover-step-limit will
no longer be limited to fewer than 2^29.
NOTE. The previous such “fixnum” behavior can be obtained
by building ACL2 with environment variable ACL2_SMALL_FIXNUMS set to a
non-empty value. In fact, such a setting is necessary for a 32-bit Lisp such
as CMUCL. However, such ACL2 builds are not as fully tested as the usual
builds and thus may be less reliable, and they are not guaranteed to work
compatibly with ordinary ACL2 builds on the same set of books.
Similarly increased the maximum lengths of
arrays:
Changed the bound *maximum-positive-32-bit-integer* that was used for
array lengths (and eliminated that constant), replacing it by the larger value
from macro call (array-maximum-length-bound), which is the same as
(fixnum-bound), i.e., 1152921504606846975. Thanks to Eric Smith for
suggesting that we consider such a change and for updating books under
books/kestrel/. Note: For CMUCL (or any 32-bit Lisp) the bound has
actually decreased, since (fixnum-bound) is 2^30-1 in that case.
The guards for functions that operate on characters or strings
sometimes insisted that the inputs contain only standard characters. That
restriction has been lifted, and the definitions of alpha-char-p,
upper-case-p, lower-case-p, char-downcase, and char-upcase have been adjusted to handle non-standard characters.
The message for evaluation failures during proofs has been modified
slightly, clarifying the case of substitution and, especially, suggesting
:DOC comment for explanations (which has been updated accordingly).
Thanks to David Russinoff for an acl2-help list query leading to this
improvement.
Example:
(defstub f (x) t)
(defund g (x) (f x))
(thm (equal (g 3) y))
*** Key checkpoint at the top level: ***
Goal'
(EQUAL
(HIDE
(COMMENT "Failed attempt to call constrained function F;
see :DOC comment"
(G 3)))
Y)
ACL2 now supports floating-point operations. See df. Regarding
this new feature: Release was approved by DARPA with “DISTRIBUTION
STATEMENT A. Approved for public release. Distribution is unlimited.”
Note for system programmers: the new df expressions affect translation
as well as stobjs-in and stobjs-out; see system-utilities, specifically
discussion mentioning “df”. Thanks to Warren Hunt for his
encouragement and support in this effort, towards ACL2 usage in scientific
computations.
The next item supports :element-type
t.
(defstobj st1
(ar1 :type (array double-float (*ar-size*))
:element-type t ; possibly faster execution but more space
:initially 0)
;; optional:
:inline t)
A new stobj field keyword, :element-type, is legal for an array
field. It specifies the raw Lisp element type of the array. Its value can be
the element type specified by the value of the :type for that array
field. That is the default value, and the other legal value is t, but
these may change in the future. See defstobj and see defstobj-element-type.
Now defabsstobj accepts the :non-executable keyword, in
analogy to support for that keyword by defstobj. Thanks to Yahya Sohail and
Warren Hunt for discussions leading to this enhancement.
New functions add-global-stobj and remove-global-stobj
change whether there is a global (“live”) stobj for a given stobj
name, thus modifying the effect of the keyword :non-executable of events
defstobj and defabsstobj. Thanks to Yahya Sohail and Warren
Hunt for discussions leading to the addition of these utilities.
A new defabsstobj keyword, :attachable, allows a single
abstract stobj to have more than one foundation and associated
functions for execution, without the need to recertify the book that
introduces the stobj. See attach-stobj. Thanks to Warren Hunt and
Yahya Sohail for requesting this feature. We thank Sol Swords, Warren, and
especially Yahya for helpful input on its high-level design.
The next item mentions defattach-system. We may look at that topic
and follow links from it to system-attachments and efficiency.
The ACL2 type-reasoning mechanism has been strengthened slightly for
an if expression being assumed true or false, when that expression has a
subterm of the form (equal term 'c), or (equal 'c term) and c
is 0, 1, t, or nil. Thanks to Warren Hunt for sending an
example involving forward-chaining that led to this improvement.
IMPORTANT NOTE: If this change causes a proof to fail that formerly
succeeded, you can fix it by preceding it with the following (implicitly local) event.
(defattach-system use-enhanced-recognizer constant-nil-function-arity-0)
The next item is quite technical but can be important
for efficiency. It's an example of the maturation of ACL2 for
industrial-strength usage.
For a book's event of the form (defconst *NAME* (quote VAL)) that
results from make-event expansion, VAL is no longer duplicated
between that book's certificate file and its compiled file. Thanks to
Sol Swords for requesting this enhancement. This lack of duplication also
applies to any such defconst event in a book that is in the scope of a
progn or encapsulate event when there is at most one
make-event call in that scope; similarly for such defconst events
within calls of skip-proofs, with-output, with-guard-checking, or with-prover-step-limit.
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.
Part 2 (J Moore)
The break-rewrite facility will now cause an interactive break on a
monitored rewrite rule if the rule's equivalence relation fails to refine any
of the equivalence relations known to be permitted while rewriting the target.
See geneqv for a discussion of how congruence rules are used to
compute permitted equivalence relations and refinement-failure for
advice about how to investigate and fix refinement failures during
rewriting.
The new documentation topic, induction-coarse-v-fine-grained,
discusses how appropriately setting ruler-extenders can sometimes improve the
induction scheme suggested by a recursive function, especially one involving
let and let* bindings containing conditional recursive calls.
For that new topic, new related books books/demos/ppr1-experiments.lisp
and books/demos/ppr1-experiments-thm-1-ppr1.lisp, and related edits of
existing :DOC topics (advanced-features, definductor, defun, induction, rulers, verify-termination, and xargs): Release was approved by DARPA with “DISTRIBUTION STATEMENT
A. Approved for public release. Distribution is unlimited.”
Example: The ppr1-experiments.lisp mentioned
above summarizes coarse and fine schemes generated for the system function
ppr1.
(assert-event ; proof time: 2165.19 seconds
(equal (about-imach 'coarse-induction-scheme (w state))
'(76 ;; 76 cases in the induction scheme
(0 . 6) ;; no induction hyps in 6 cases, i.e., Base Cases
(1 . 8) ;; 1 induction hyp in 8 cases
(2 . 2) ;; 2 induction hyps in 2 cases
(3 . 16) ;; ...
(4 . 32)
(8 . 4)
(9 . 8) ;; 9 induction hyps in 8 cases
)))
(assert-event ; proof time: 65.00 seconds
(equal (about-imach 'fine-induction-scheme (w state))
'(256 ;; 256 cases in the induction scheme
(0 . 6) ;; no induction hyps in 6 cases, i.e., Base Cases
(1 . 8) ;; 1 induction hyp in 8 cases
(2 . 82) ;; 2 induction hyps in 82 cases
(3 . 80) ;; 3 induction hyps in 80 cases
(4 . 80) ;; 4 induction hyps in 80 cases
)))
A new brr command, :explain-near-miss, when issued in a
break caused by a near miss, will try to pinpoint how the rule's pattern
failed to match the current target.
A new utility, compare-objects, highlights the differences between
two cons-trees.
Example:
ACL2 !>(compare-objects '(f x y (g x '(a b c)))
'(f y x (g x '(a b c . d))))
((:OBJ (F :|<s1>|
:|<s2>|
(G X '(A B C . :|<s3>|))))
(:LEGEND ((:|<s1>| X Y)
(:|<s2>| Y X)
(:|<s3>| NIL D))))
A new documentation topic and its subtopics describe uses of ACL2 and its
predecessor, Nqthm, in modeling state machines. See operational-semantics, which notes that others are welcome to add to these
topics; see the discussion of “Request for Suggestions from ACL2
Users”. The new topic incorporates an annotated bibliography pointing
to more than 40 topics in a new "BIB" package.
This is a massive new topic, comprising about 100 kB
of text in about 2,300 lines. We wrote it to “put our stake in the
ground” regarding the mechanization of operational semantics. It
includes an annotated bibliography that lists papers by many ACL2 users. If
you think a paper is missing, please add it or email me!
There were several tweaks to do$. If you use
DO loop$ (see do-loop$) or if you have lemmas that explicitly
mention do$ and you experience translation errors, you'll want to pay
attention to the revised documentation.
The fifth formal of do$ now represents the values returned rather
than a default value. This change supports a bug fix; see the item below
regarding “About a bug in DO$ in ACL2 Version 8.5”.
The sixth and seventh arguments of do$ have been combined into a
record that also contains a list of the names of all the stobjs in the
DO loop$. In the new record, the measure term is stored in
untranslated form. The record is only used in the hard error produced when
the evaluation of a DO$ term fails to terminate and is not relevant to
the logical value of the DO$ term.
Fixed a bug in handling of do-loop$ expressions that return
multiple values, when encountered during proofs. An example labeled with
“Version 8.5” is near the end of community-book
projects/apply/loop-tests.lisp.
A bug in do$, hence in do-loop$ expressions, was that
single-threadedness (for stobj-based computations) can be violated when
a loop terminates prematurely because the measure fails to decrease. The bug,
which has been fixed, is explained in detail in a comment in ACL2 source file
apply.lisp, entitled “About a bug in DO$ in ACL2
Version 8.5”.
Fixed a bug that could cause an implementation error during a proof, when
printing a term with a do$ call. (The bug was in untranslating
certain applications of nth, update-nth, or update-nth-array during a proof.)
