Note-3-2-1
ACL2 Version 3.2.1 (June, 2007) 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
evaluation of 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 (Dynamically 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 with-prover-time-limit.
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 proof-builder's sr (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))
Modified 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 (and :all is supported only for legacy
purposes). A new value for compile-flg, :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 "T", "NIL", or ":RAW"
will determine the value of the optional compile-flg argument to be
t, nil, or :raw, respectively, when this argument is not
explicitly supplied.
Modified 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.
The function nonnegative-integer-quotient is now computed in raw
Lisp by calling 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
equivalence of nonnegative-integer-quotient and floor, and
serves as a repository for other miscellaneous proofs, including those
justifying ACL2 modifications such as this one.
Enhanced 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 accumulated-persistence statistics.
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: :by,
:cases, and :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 note-3-2-1, 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 body.
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 by
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
import function.
Modified 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
add-include-book-dir.
Added a new value for the :do-not-induct hint (see hints),
:otf-flg-override, which causes ACL2 to ignore the :otf-flg
when considering whether to abort the proof because of a :do-not-induct
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 a
change.
(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
treatment of state-global-let* by progn! in favor of a new keyword
argument, 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
these changes.
Incorporated backward-compatible enhancements to
books/misc/expander.lisp from Daron Vroon (documented near the top of
that file).
The specification of :backchain-limit-lst had required that only a
single (:rewrite, :linear, or :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 rule class (:rewrite :backchain-limit-lst 1) is now legal for the
corollary formula (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
attention.
