NOTE-3-2-1

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 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 (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 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-checker'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)

(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 miscellaeous 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.