|
|
|---|
|
|
|
|---|
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.
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).
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!)
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-
An attachable stobj (see attach-stobj) was created by the
executable (
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