• 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-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-4-1

ACL2 Version 4.1 (September, 2010) 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 since Version 4.1 into the following categories of changes: existing features, new features, heuristic improvements, bug fixes, distributed books, 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.

CHANGES TO EXISTING FEATURES

The guard associated with calls of the macro, search, has been weakened so that now, given strings are no longer restricted to contain only standard characters unless the :test argument is char-equal.

Modified the writing of ``hidden defpkg'' forms into certificate files (see hidden-defpkg), to support moving certificate files for distributed books, as is done by ACL2s (see ACL2-sedan) and Debian releases of ACL2. Thanks to Camm Maguire for reporting a problem with Debian releases of ACL2 that led to this change.

Expanded the constant *acl2-exports* by adding intersection-equal to the list. Thanks to Jared Davis for requesting this change.

The :comp utility now compiles functions that have code conditionalized for raw Lisp only (presumably because a trust tag was active when they were defined). Previously, this was not the case when :comp was applied to more than a single function symbol.

NEW FEATURES

A new macro, top-level, allows evaluation directly in the top level loop for forms that normally need to be evaluated inside function bodies, such as with-local-stobj. See top-level. Thanks to Jared Davis for requesting such a utility.

Added count, a Common Lisp function, to ACL2. In support of that addition, also added rewrite rule eqlablep-nth.

HEURISTIC IMPROVEMENTS

[None this time.]

BUG FIXES

We fixed a soundness bug that could occur when a function that returns multiple values is called in its own guard. Thanks to Sol Swords for reporting this bug and sending a small self-contained example, which is included in a comment in the function chk-acceptable-defuns1 in ACL2 source file defuns.lisp.

It was possible to cause an error when giving theory hints during redefinition of functions. This has been fixed. Thanks to Ian Johnson for sending an example that nicely illustrated this problem.

Fixed system function io? for the case that formal parameter commentp is t and vars is non-empty. Thanks to David Rager for bringing to our attention the fact that io? was broken for such a combination of parameters.

Not exactly a bug fix, but: defun-sk was breaking when a :guard is specified, so we have improved the documentation (see defun-sk) to explain how to provide verified guards for a function introduced by defun-sk. Thanks to Jared Davis for bringing this issue to our attention.

Made a fix to the handling of interrupts, which in rare cases might have left one in a state where all subsequent proof attempts were labeled as ``Aborting due to an interrupt''.

Fixed :pso and related utilities, so that when proof output is redirected to a file, all summary output goes to that file rather than to the terminal.

(GCL on Windows only) Removed an inappropriate check, resulting in an error about ``pathname-device,'' that could prevent Windows GCL builds of ACL2. Thanks to Camm Maguire for reporting this problem and a helpful discussion.

(Windows only) Modified the computation of canonical pathnames to avoid issues of case-insensitivity, in particular for the drive (e.g., "C:" vs. "c:"). Thanks to Harsh Raju Chamarthi for reporting this issue and helping with its debugging.

(Windows only) The value of (@ distributed-books-dir) no longer will be missing the Windows drive prefix, for example, "C:". Thanks to Harsh Raju Chamarthi for reporting this issue and helping with its debugging.

NEW AND UPDATED BOOKS AND RELATED INFRASTRUCTURE

See the log entries for a record of books changed or added since the preceding release, with log entries.

Modified books/Makefile-generic by adding a new BOOKS_SKIP_COMP variable, which is used in Makefiles in some subdirectories of books/, in order to avoid errors when compiling certified books for multiple Lisps.

EMACS SUPPORT

Distributed file emacs/emacs-acl2.el has been modified so that the forms control-t e and control-t control-e now pick up package markers (see sharp-bang-reader), in the following sense: if the top-level form is preceded by a line starting with #!, then that line is included in the inserted string. Thanks to Jared Davis for suggesting this enhancement and providing a preliminary implementation.

EXPERIMENTAL VERSIONS

For the HONS version there have been some changes to memoize:

Memoize accepts a new keyword, :recursive, that is a synonym for the existing keyword :inline. Thanks to Sol Swords for requesting this addition. Moreover, it is now enforced that these keywords have Boolean values.

Memoize may now be called on :program mode functions. Thanks to Sol Swords for requesting this enhancement.

A bug has been fixed. Now, if memoize is called with a :condition-fn (with value other than nil or t), then the guard of the memoized function and the :condition-fn must be the same. Previously, one could exploit the lack of such a check to get a hard Lisp error, for example as follows.

(defun f (x) (declare (xargs :guard t)) x)
(defun cf (x) (declare (xargs :guard (consp x))) (car x))
(memoize 'f :condition-fn 'cf)
(f 3)

Memoization is now illegal for built-in functions that use underlying raw Lisp in their implementations. To see why, consider the form (gc$), which is a macro call expanding to (gc$-fn nil). Previously, after evaluation of (memoize 'gc$-fn), a call of gc$ would no longer call the garbage collector, which had been invoked by raw Lisp code. Now, evaluation of (memoize 'gc$-fn) causes an error.