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.
Fixed a soundness bug, introduced in the previous release, due to a failure
table events that set the
local context. Here is a proof of
nil that exploits the bug.
(encapsulate () (local (program)) (defun foo () (declare (xargs :measure 17)) (+ 1 (foo)))) (thm nil :hints (("Goal" :in-theory (disable foo (foo)) :use foo)))
Fixed a bug in the alternatives to
good-bye, which are the
quit commands. Thanks to Jared Davis and Peter Dillinger for
pointing this out right away.
The definition of
len has been highly optimized in raw Lisp. Thanks to
Bob Boyer and Warren Hunt for suggesting such an improvement and providing
a lot of help in coming up with the current implementation.
The clause subsumption algorithms have been improved, both to improve
efficiency during warnings for
rewrite rules and to punt when the
subsumption computation for induction appears to be blowing up. Thanks to
Robert Krug for bringing this issue to our attention and supplying a useful
A bug has been fixed that prevented
time$ from working properly in
OpenMCL and multi-threaded SBCL (actually, in any ACL2 image where feature
:acl2-mv-as-values is present). Thanks to Sol Swords for bringing this
problem to our attention.
A type-spec of the form
(satisfies pred) carries the requirement
pred be a unary function symbol in the current ACL2 world;
otherwise, it is illegal. Thanks to Dave Greve for pointing out that Common
Lisp has this requirement.
Installed a fix provided by Gary Byers (for ACL2 source function
install-new-raw-prompt), for OpenMCL, that fixes an issue exposed in some
versions of OpenMCL when compiler optimization is off.
Fixed a bug in contributed book
misc/untranslate-patterns.lisp that was
causing calls of
add-untranslate-pattern to be rejected in books.
Thanks to Ray Richards for pointing out this bug and to Jared Davis for
assisting in the fix.
Fixed a bug in
defstobj when keywords
are both supplied. In this case, the definition of the resizing function
mistakenly failed to quote the
:initially value, even though this value
is not to be evaluated. One could even get an error in this case, as in the
following example supplied by Erik Reeber, whom we thank for bringing this
bug to our attention:
(defstobj $test (test-x :type (array t (5)) :initially (0) :resizable t))
A new feature,
with-prover-time-limit, allows the setting of time
limits during proofs. This is not a general-purpose time-limit utility,
nor is it guaranteed to implement a strict bound; it only attempts to limit
time approximately during proofs. Thanks to Pete Manolios and Daron Vroon,
who made the most recent request for such a feature, and to Robert Krug for a
(GCL only) Fixed a bug in the procedure for building a profiling image. Thanks to Sol Swords for bringing this bug to our attention and to Eric Smith for bringing a subsequent problem to our attention.
Handling of theories can now use significantly less time and space. A regression suite run took about 25% longer before this change than it did after making this change (and also the ones in the next two paragraphs). Thanks to Vernon Austel for bringing this issue to our attention and for supplying code, quite some time ago, that provided detailed, useful implementation suggestions. Also thanks to the folks at Rockwell Collins, Inc. for pushing the limits of the existing implementation, thus encouraging this improvement.
Fixed a performance bug in obtaining executable counterpart symbols.
We now avoid certain computations made on behalf of warnings, when such warnings are disabled.
We have relaxed the checks made when including an uncertified book, to match the checks made when including a certified book. Thanks to Eric Smith for suggesting this change.
Fixed a bug in
pso (see set-saved-output) that caused an error
when printing the time summary.
Made fixes to avoid potential hard Lisp errors caused by the use of
program mode functions. The fix was to use a ``safe mode,''
already in use to prevent such errors during macroexpansion;
see guards-and-evaluation. However, such errors were possible during
evaluation of macro guards, for example as follows:
(defun foo (x) (declare (xargs :mode :program)) (car x)) (defmacro mac (x) (declare (xargs :guard (foo 3))) x) (defun g (x) (mac x))A similar issue existed for calls of
value-triple, but has been fixed for all but
make-event, where technical issues have caused us to defer this change.
Fixed a bug in
wet that caused problems in OpenMCL, and perhaps other
Lisp implementations, when the argument to
wet calls, or depends on,
certain built-ins including
must-be-equal. Thanks to David Rager for bringing this problem to our
books/Makefile-generic has been improved so that when book
certification fails with
make, the failure message contains the book
Documentation has been written to explain how to avoid an expensive immediate
rewrite of the result of applying a
rule. See meta. Thanks to Robert Krug for supplying this trick, and to Eric
Smith and Dave Greve for useful discussions.
(OpenMCL only) OpenMCL-based ACL2 image names formerly had extension
".dppccl", which was correct only for some platforms (including 32-bit
Darwin PPC). That has been fixed, thanks to a suggestion from Gary Byers.
It is now legal to attach both a
:use and a
:cases hint at the same
goal. Thanks to Eric Smith for (most recently) requesting this feature.
It is now permissible to include the same symbol more than once in the
imports list of a
defpkg form (i.e., its second argument). Also, the
defpkg forms with long import lists now uses a reasonably
efficient sorting routine to check for two different symbols with the same
name (see also
books/sort-symbols.lisp). If you currently call a
remove-duplicates-eql for your imports list, as had been
suggested by a
defpkg error message, then you may experience some
speed-up by removing that call. Thanks to Eric Smith for helping to discover
this issue through profiling.
Made miscellaneous efficiency improvements not listed above (for example,
following a suggestion of Eric Smith to avoid checking for so-called ``bad
Lisp objects'' during
include-book, which saved almost 3% in time on
one large example).
Modified the notion of ``untouchable'' to separate the notion of untouchable
functions and macros from the notion of untouchable state global variables.
See push-untouchable. Thanks to Bob Boyer for sending an example,
(put-global 'ld-evisc-tuple t state), that suggested to us the need for
more restrictive handling of untouchables. In particular, many
specials (see ld) are now untouchable. You may be able to work around this
restriction by calling
ld; see for example the change to
books/misc/expander.lisp. But please contact the ACL2 implementors if
this sort of workaround does not appear to be sufficient for your purposes.
Fixed a bug in function
set-standard-oi (see standard-oi).
Fixed a bug in the use of
ld-evisc-tuple. The bad behavior was an
improper use of the print-level and print-length components of the tuple
(specifically, taking its
cadddr instead of taking its
caddr). Thanks to Bob Boyer for bringing this bug to
A new argument to the
compile-flg argument of
:all, causes creation of a file to be compiled in place of the given
book, where that file contains not only a copy of the book (with
make-event forms expanded) but also contains definitions of the
so-called ``executable counterparts'' of the functions defined in the book.
Then, functions defined in the book will be run compiled when including the
book, even for functions whose guards have not been verified, or are in
:program mode and running in so-called ``safe mode''
(for example, during expansion of macros). The default behavior, value
compile-flg, is unchanged. Moreover, a new
:comp! argument of
include-book now compiles the executable counterparts when creating the
book's compiled file, and unlike
:comp, always deletes the old compiled
file first so that one always gets a fresh compile.
certify-book gives a "Guards" warning only for
mode functions that are defined in the given book but have not had their
guards verified. Previously, it also warned about such functions that were
defined in the certification world or in sub-books.
A new command,
redo-flat, facilitates the debugging of failed
progn forms by evaluating preliminary forms in
order to leave one at the point of failure. See redo-flat. Thanks to
Ray Richards and others for asking for such a utility, and to Sandip Ray
for useful discussions.
We have changed the automatic declaration of of function types (still done in
GCL and OpenMCL only, for now). Our motivation was to avoid the assumption
that Common Lisp functions return one value when ACL2 says that they do;
thanks to Bob Boyer for bringing this issue to our attention with the example
(foo x y) to be
(floor x y). ACL2 was saying that
foo returns a single value, but because
floor returns two values in
raw Lisp, so does
foo. Other changes to automatic declaration include
defund, not just
A new function,
(mod (expt base exp) m), and
does so efficiently in some implementations (currently only in GCL 2.7.0,
which is not yet released). Thanks to Warren Hunt for suggesting such an
setenv$ have been made available for
reading and writing environment variables. Thanks to Jun Sawada for
requesting these utilities.
The query utility
pl has been improved in several ways. As
meta rules are only printed if the argument is a symbol;
but the information printed for them is now more appropriate. The following
are changes for the case that the argument is not a symbol, but rather, a
term. (1) Rules are displayed that have equivalence relations other
equal. (2) All matching
definition rules are
displayed, where previously
:definition rules were only shown if they
were ``simple'' rules (sometimes known as ``abbreviations''); see simple.
(3) The ``Equiv'' field is printed for terms, not just symbols. (4) The
substitution is shown that, when applied to the left-hand side of the rule,
will yield the specified term. Thanks to Eric Smith for suggesting these
The proof-checker command
;show-rewrites has been improved to match
the changes described above for
pl. In particular,
definition rules that are not ``simple'' are now displayed by
sr) command, and the
rewrite command has been correspondingly modified to
copy-nonstd so that they should also work for non-developers.
Fixed a bug that was causing
pr to display
hypotheses oddly in some cases, in particular
(syntaxp (let ...)).
(The problem was in the ``untranslate'' display of the internal form of
syntaxp calls.) Thanks to Robert Krug for bringing this problem to our
attention. We also removed the restriction on
bind-free that its
argument could not be a variable, a constant, or (more interestingly) a
lambda application (i.e., a