• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
      • About-ACL2
        • Recursion-and-induction
        • Operational-semantics
        • Soundness
        • Release-notes
          • Note-2-8
          • Note-2-7
          • Note-8-6
          • Note-8-2
          • Note-7-0
          • Note-8-5
          • Note-8-3
          • Note-8-1
          • Note-8-0
          • Note-7-1
          • Note-6-4
          • Note-2-9-3
          • Note-2-9-1
          • Note-8-4
          • Note-7-2
          • Note-6-5
          • Note-4-0
          • Note-2-9-2
          • Note-3-6
          • Note-3-3
          • Note-3-2-1
          • Note-3-0-1
          • Note-2-9-5
          • Note-2-5
          • Note-1-5
          • Note-6-1
          • Note-4-3
          • Note-4-2
          • Note-4-1
          • Note-3-5
          • Note-3-4
          • Note-3-2
          • Note-3-0-2
          • Note-2-9-4
          • Note-2-9
          • Note-1-8
          • Note-1-7
          • Note-1-6
          • Note-1-4
          • Note-1-3
          • Note-7-4
          • Note-7-3
          • Note-6-3
          • Note-6-2
          • Note-6-0
          • Note-5-0
          • Note-8-7
            • Note-8-7-books
          • Note-1-9
          • Note-2-2
          • Note-1-8-update
          • Note-3-5(r)
          • Note-2-3
          • Release-notes-books
          • Note-3-6-1
          • Note-1-2
          • Note-2-4
          • Note-2-6
          • Note-2-0
          • Note-3-0
          • Note-3-2(r)
          • Note-2-7(r)
          • Note-1-1
          • Note-3-4(r)
          • Note-3-1
          • Note-2-8(r)
          • Note-2-1
          • Note-2-9(r)
          • Note-2-6(r)
          • Note-3-1(r)
          • Note-3-0(r)
          • Note-3-0-1(r)
          • Note-2-5(r)
          • Note-4-3(r)
          • Note-4-2(r)
          • Note-4-1(r)
          • Note-4-0(r)
          • Note-3-6(r)
          • Note-3-3(r)
          • Note-3-2-1(r)
        • Version
        • Acknowledgments
        • Pre-built-binary-distributions
        • Common-lisp
        • Git-quick-start
        • Copyright
        • Building-ACL2
        • ACL2-help
        • Bibliography
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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

New Features

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).

Bug Fixes

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.

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.

EMACS Support

Experimental Versions

Subtopics

Note-8-7-books

Release notes for the ACL2 Community Books for ACL2 8.7