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
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
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
[None this time.]
We fixed a soundness bug that could occur when a function that returns
multiple values that 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
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
Not exactly a bug fix, but: defun-sk was breaking when a
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''.
(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.,
(Windows only) The value of
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.
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 nilor t), then the guard of the memoized function and the :condition-fnmust 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.