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.
(OpenMCL and multi-threaded SBCL only) Fixed a soundness bug in the
mbe forms in the presence of Lisp feature
:acl2-mv-as-values. Thanks to Sol Swords for reporting this problem and
sending a simple proof of
nil (which can be found in a comment in the
ACL2 sources, in
(deflabel note-3-2-1 ...)).
Added a new utility,
dmr (Dynamicaly Monitor Rewrites), for watching
the activity of the rewriter and some other proof processes. See dmr. We
thank Robert Krug for useful contributions.
Fixed a bug in evaluation of calls of
Fixed the writing of executable scripts when building ACL2, so that the
build-time value of environment variable
ACL2_SYSTEM_BOOKS is no longer
written there. Thanks to Dave Greve for discussing this change.
Fixed bugs in
pl (which are similarly present in the
show-rewrites) command. The first bug was
evident from the following forms sent by Robert Krug, which caused an error.
(include-book "arithmetic-3/floor-mod/floor-mod" :dir :system) :pl (mod (+ 1 x) n)The second bug was due to a failure to take note of which rules are disabled, and could be seen by executing the following (very slow!).
(defstub modulus () t) (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system) :pl (mod (+ x y) (modulus))
certify-book so that by default, all executable-counterpart
functions (sometimes called ``*1* functions'') are compiled. This is the
behavior that was already supported with a
compile-flg argument of
:all; the change is that argument
t now has this behavior as well
:all is supported only for legacy purposes). A new value for
:raw, gives the behavior formerly produced by value
t, namely where executable-counterpart functions are not compiled. The
above changes are irrelevant if compilation is suppressed; see compilation.
Finally, if environment variable
ACL2_COMPILE_FLG is set, then after
converting to upper-case this environment variable's value of
":RAW" will determine the value of the optional
compile-flg argument to be
when this argument is not explicitly supplied.
include-book so that
:comp argument now acts like
:comp!, i.e., compiling a file that includes the file together with all
executable counterpart (so-called ``*1*'') functions. A new argument,
:comp-raw, has the behavior that
:comp had formerly, i.e., compiling
the actual book only.
nonnegative-integer-quotient is now computed in raw Lisp
floor on its arguments. This change was suggested by Peter
Dillinger, in order to avoid stack overflows such as reported by Daron
Vroon. A new book,
books/misc/misc2/misc.lisp, contains a proof of
floor, and serves
as a repository for other miscellaeous proofs, including those justifying
ACL2 modifications such as this one.
accumulated-persistence to break down results by useful vs.
useless rule applications. In particular, this provides information about
which rules were ever applied successfully, as requested by Bill Young.
Added coverage of
meta rules to the
Fixed a bug that was causing a
clause-processor hint to fire on a
subgoal of the goal to which it was attached, when the original application
didn't change the clause. Thanks to Dave Greve for pointing out this bug and
providing a useful example.
Fixed a bug in handling of computed hints related to the
stable-under-simplificationp parameter (see computed-hints). There were
actually two bugs. A minor but confusing bug was that the same goal was
printed twice upon application of such a hint. The major bug was that
:use hints (as well as other ``top'' hints:
:clause-processor) were not being applied properly. Thanks to Jared
Davis for sending an example some time ago that showed the duplicate
printing, and to Dave Greve for sending an example showing mis-application of
clause-processor hints. Note that you may find that existing
computed hints using the
stable-under-simplificationp parameter no longer
have the same behavior; see a comment about computed hints in
ACL2 source file
ld.lisp, for an example of how you might want to fix
such computed hints.
David Russinoff has contributed an updated version of
books/quadratic-reciprocity/ including minor modifications of the
treatment of prime numbers and a proof that there exist infinitely many
primes. Thanks to David for contributing this work, and to Jose Luis
Ruiz-Reina for posing the challenge.
Reduced the sizes of some certificate (
.cert) files by relaxing the
test that allows original
defpkg events to be placed there, rather
than evaluating the import list term into an explicit list of symbols.
Improved execution efficiency slightly for function
rcdp in file
books/misc/records.lisp, by using
mbe to introduce a tail-recursive
The executable script generated by
save-exec (and by the normal build
process) now includes a time stamp as a comment. Thanks to Jared Davis for
suggesting this change in order to support his use of
omake. In the
process, we also arranged that the startup banner for an executable created
save-exec shows all of the build (save) times, not just the one for
the original image.
Sped up most redundant
defpkg events by avoiding evaluation and sorting
of the imports list in the case of identical event forms. And, for
defpkg events that are not redundant, sped up their processing in Allegro
CL (and perhaps other Lisps, but apparently not GCL) by using our own
add-include-book-dir so that it refuses to associate a keyword
with a different directory string than one it is already bound to.
See delete-include-book-dir for how to remove the existing binding first.
Thanks to Robert Krug for pointing out that without this change, one can find
it difficult to debug a failure due to rebinding a keyword with
Added a new value for the
:do-not-induct hint (see hints),
:otf-flg-override, which causes ACL2 to ignore the
when considering whether to abort the proof because of a
hint. Thanks to Daron Vroon for suggesting such an addition.
Modified the printing of messages for entering and exiting raw mode
(see set-raw-mode), so that in particular they are inhibited during
include-book or whenever
observations are inhibited
(see set-inhibit-output-lst). Thanks to Peter Dillinger for suggesting such
(For system hackers only.) The handling of events of the form
(progn! (state-global-let* ...)) had a bug that was causing bindings to
be evaluated twice. Moreover, the use of system function
state-global-let* is suspect in raw Lisp. We have eliminated special
progn! in favor of a new keyword
state-global-bindings, that provides the intended
functionality. See progn!. Moreover, special handling that allowed
make-event forms under
state-global-let* has been removed; the
desired effect can be obtained using (progn! :state-global-bindings ...).
Thanks to Peter Dillinger for pointing out the above bug and collaborating on
Incorporated backward-compatible enhancements to
from Daron Vroon (documented near the top of that file).
The specification of
:backchain-limit-lst had required that only a single
meta) rule be
generated. We have weakened this restriction to allow more than one rule
provided that each rule has the same list of hypotheses. For example, the
(:rewrite :backchain-limit-lst 1) is now legal for the
(implies (f x) (and (g x) (h x))), where this was not
formerly the case. Thanks to Dave Greve for bringing this issue to our