• 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

• Note-8-7
• Release-notes-books

Note-8-7-books

Release notes for the ACL2 Community Books for ACL2 8.7

The following is a brief summary of changes made to the community-books between the releases of ACL2 8.6 and 8.7.

See also note-8-7 for the changes made to ACL2 itself. For additional details, you may also see the raw commit log.

New Libraries

HOL-ACL2 Link Support

See projects/hol-acl2/README-acl2. That directory provides modifications of the HOL-ACL2 link from a HOL4 distribution, updating ACL2 aspects of that link to work with the latest versions of ACL2.

Changes to Existing Libraries

C Library

Tool-Oriented C Syntax

We have added a tool, c$::defpred, to concisely define predicates over the abstract syntax.

Schroeder-Bernstein Library

This library has moved from [books]/projects/schroder-bernstein to [books]/projects/schroeder-bernstein in order to reflect the prevailing German convention of printing an "o" with umlaut as "oe" when umlaut letters are unavailable.

Standard Typed Alists Library

A theorem has been added.

Standard Utilities Library

A macro binder for b* has been added. This binder closely resembles the fun binder, but expands to a macrolet instead of an flet.

Tools Library

The "defthm-macro" generated by make-flag has been fixed to handle theorems over trivial mutual-recursion cliques consisting of just one function.

Documentation

Licensing Changes

Build System Updates

Testing

Miscellaneous

Books based on run-script now certify even when gag-mode has been set in advance, say, by an ACL2-customization file.

Tests run by certifying kestrel/acl2data/gather/tests/run-tests.lisp would fail when environment variable ACL2_CUSTOMIZATION was set. That bug has been fixed.

The new directory demos/attach-stobj/ illustrates the use of attach-stobj. See file README.txt in that directory.

The new book demos/fp.lisp (with associated files fp.acl2 and fp-raw.lsp in the same directory) illustrates the power of partial-encapsulate, showing how it is used in the implementation of floating-point operations in ACL2.