Major Section: RELEASE-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
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
the list. Thanks to Jared Davis for requesting this change.
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
was applied to more than a single function symbol.
A new macro,
top-level, allows evaluation directly in the top level
loop for forms that normally need to be evaluated inside function bodies,
with-local-stobj. See top-level. Thanks to Jared Davis for
requesting such a utility.
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
chk-acceptable-defuns1 in ACL2
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
vars is non-empty. Thanks to David Rager for bringing to
our attention the fact that
io? was broken for such a combination of
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
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''.
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
(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:"). 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 http://code.google.com/p/acl2-books/source/list for a record of books changed or added since the preceding release, with log entries.
books/Makefile-generic by adding a new
variable, which is used in
Makefiles in some subdirectories of
books/, in order to avoid errors when compiling certified books for
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.
HONS version there have been some changes to
Memoizeaccepts 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.
Memoizemay now be called on
programmode functions. Thanks to Sol Swords for requesting this enhancement.
A bug has been fixed. Now, if
memoizeis called with a
:condition-fn(with value other than
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.