Note-3-0-1
ACL2 Version 3.0.1 (August, 2006) 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
to disallow table events that set the ACL2-defaults-table in a 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 exit and 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
example.
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 that 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 :initially and
:resizable 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 helpful discussion.
(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 defpkg, in-theory,
table, make-event, and value-triple, but has been fixed
for all but in-theory and 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 prog2$, time$, mbe, and
must-be-equal. Thanks to David Rager for bringing this problem to our
attention.
The file books/Makefile-generic has been improved so that when book
certification fails with `make', the failure message contains the book
filename.
Documentation has been written to explain how to avoid an expensive
immediate rewrite of the result of applying a :rewrite or
:meta 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
evaluation of 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/misc/sort-symbols.lisp). If you currently
call a function like 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
ld 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 caddr and cadddr instead of taking
its cadr and caddr). Thanks to Bob Boyer for bringing this
bug to our attention.
A new argument to the compile-flg argument of certify-book,
: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 t of 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.
Now, certify-book gives a "Guards" warning only for :logic 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
encapsulate and 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
of defining (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
comprehending defund, not just defun.
A new function, mod-expt, computes (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
addition.
New functions getenv$ and 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
before, :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
than 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 changes.
The proof-builder 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 the proof-builder's show-rewrites (and sr)
command, and the proof-builder's rewrite command has been
correspondingly modified to accept these :definition rules.
Fixed `make' targets copy-distribution, copy-workshops, and
copy-nonstd so that they should also work for non-developers.
Fixed a bug that was causing :pr to display syntaxp
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 let or mv-let expression).
