NOTE-3-0-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.

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))

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/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-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 the proof-checker's show-rewrites (and sr) command, and the proof-checker'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).