ACL2 Version 3.5 (May, 2009) Notes
NOTE! New users can ignore these release notes, because the documentation has been updated to reflect all changes that are recorded here.
Below we roughly organize the changes since Version 3.4 into the following categories: changes to existing features, new features, heuristic improvements, bug fixes, new and updated books, Emacs support, and experimental hons version. Each change is described in just one category, though of course many changes could be placed in more than one category.
CHANGES TO EXISTING FEATURES
Many improvements have been made to ACL2's ``evisceration'' mechanism for hiding substructures of objects before they are printed, and to related documentation:
o A new documentation topic explains evisc-tuples. See evisc-tuple.
o A new mode, ``iprinting'', allows eviscerated output to be read back in. See set-iprint.
default-evisc-tuplehas been deprecated and will probably be eliminated in future releases; use abbrev-evisc-tupleinstead. Also eliminated is the brr-term-evisc-tuple (also the user-brr-term-evisc-tuple). The term-evisc-tuple controls printing formerly controlled by the brr-term-evisc-tuple or user-brr-term-evisc-tuple.
o ACL2 output is done in a more consistent manner, respecting the intention of those four global evisc-tuples. In particular, more proof output is sensitive to the term-evisc-tuple. Again, see set-evisc-tuple.
o (Details for heavy users of the evisc-tuple mechanism) (1) There are no longer state globals named
user-term-evisc-tupleor user-default-evisc-tuple. (2) Because of the above-mentioned :DEFAULT, if you have referenced state globals directly, you should use accessors instead, for example (abbrev-evisc-tuple state)instead of (@ abbrev-evisc-tuple). (3) For uniformity, set-trace-evisc-tuple now takes a second argument, state.
Improved break-on-error in several ways. First, it breaks earlier
in a more appropriate place. Thanks to Dave Greve for highlighting this
problem with the existing implementation. Also, break-on-error now
breaks on hard errors, not only soft errors (see er, options
Trace! may now be used in raw Lisp (though please note that all soundness claims are off any time you evaluate forms in raw Lisp!). Thanks to Bob Boyer for feedback that led to this enhancement.
ACL2 now searches for file
If trace output is going to a file (because open-trace-file has been executed), then a note will be printed to that effect at the time that a call of trace$ or trace! is applied to one or more trace specs.
The notion of redundancy (see redundant-events) has been made more restrictive for mutual-recursion events. Now, if either the old or new event is a mutual-recursion event, then redundancy requires that both are mutual-recursion events that define the same set of function symbols. Although we are not aware of any soundness bugs fixed by this modification, nevertheless we believe that it reduces the risk of soundness bugs in the future.
The definition of
Certain certificate files will now be much smaller, by printing in a
way that takes advantage of structure sharing. Certifying the following
example produces a
(defun nest (i) ;; Makes an exponentially-sized nest of conses i deep. (if (zp i) nil (let ((next (nest (1- i)))) (cons next next)))) (make-event `(defconst *big* ',(nest 20)))
Thanks to Sol Swords for providing the above example and to him as well as to Bob Boyer, Jared Davis, and Warren Hunt for encouraging development of this improvement. We have also applied this improvement to the printing of function definitions to files on behalf of certify-book and comp.
Names of symbols are now printed with vertical bars according to the Common
Lisp spec. Formerly, if the first character of a symbol name could be the
first character of the print representation of a number, then the symbol was
printed using vertical bars (
The ACL2 reader now supports `
Some small changes have been made related to gag-mode:
o ACL2 had printed ``
Q.E.D.'' with all output suppressed and gag-mode enabled. Now, `` Q.E.D.'' will be suppressed when PROVEand SUMMARYoutput are suppressed, even if gag-modeis enabled.
o The use of set-gag-mode had drastic effects on the inhibited output (see set-inhibit-output-lst), basically inhibiting nearly all output (even most warnings) when turning on gag-mode and enabling all output except
proof-treeoutput when turning off gag-mode. Now, set-gag-mode only inhibits or enables proof ( PROVE) output, according to whether gag-mode is being turned on or off (respectively). The related utility set-saved-outputhas also been modified, basically to eliminate :allas a first argument and to allow tand :allas second arguments, for inhibiting prover output or virtually all output, respectively (see set-saved-output).
A defstub event signature specifying output of the form
Improved the efficiency of string-append so that in raw Lisp, it
calls concatenate. Thanks to Jared Davis for suggesting this change,
including the use of mbe. A minor change was made to the definition
of concatenate to support this change, and the lemma
The checksum algorithm used for certificate files of books
has been changed. Thanks to Jared Davis for contributing the new code. This
change will likely not be noticed unless one is using the experimental hons version of ACL2, where it can greatly speed up book certification and
inclusion because of function memoization (of source function
Fewer calls are made to the checksum algorithm on behalf of certify-book and a few other operations. Thanks to Jared Davis for providing data that helped lead us to these changes.
Formatted printing directives
Users may now control whether or not a slow array access results in a warning printed to the screen (which is the default, as before), and if so, whether or not the warning is followed by a break. See slow-array-warning.
On linux-like systems (including Mac OS X and SunOS),
The messages printed for uncertified books have been enhanced. Thanks to Jared Davis for requesting such an improvement.
A function definition that would be redundant if in
The ACL2 reader no longer accepts characters other than those recognized by
standard-char-p except for
(in-package "ACL2") (defconst *my-null* (code-char 0)) (make-event `(defconst *new-null* ,*my-null*))
For this book, a call of certify-book formerly broke during the compilation phase, but if there was no compilation, then a call of include-book broke. Now, the error occurs upon evaluation of the make-event form.
ACL2 now collects up guards from declare forms more as a user might expect, without introducing an unexpected ordering of conjuncts. We thank Jared Davis for sending us the following illustrative example, explained below.
(defun f (x n) (declare (xargs :guard (and (stringp x) (natp n) (= (length x) n))) (type string x) (ignore x n)) t)
Formerly, a guard was generated for this example by unioning the conjuncts
The guard of this guard failed to be verified because
Modified close-output-channel to try to do a better job flushing buffers. Thanks to Bob Boyer for helpful correspondence.
The notion of ``subversive recursion'' has been modified so that some functions are no longer marked as subversive. See subversive-recursions, in particular the discussion elaborating on the notion of ``involved in the termination argument'' at the end of that documentation topic.
It is now possible to affect ACL2's termination analysis (and resulting
induction analysis). Thanks to Peter Dillinger for requesting this feature.
The default behavior is essentially unchanged. But for example, the following
definition is accepted by ACL2 because of the use of the new
The following lemma was added in support of the improvement to string-append described above:
(defthm append-to-nil (implies (true-listp x) (equal (append x nil) x)))
A mechanism has been provided for users to contribute documentation. See
managing-ACL2-packages for an example, which contains a link to an
external web page on effective use of ACL2 packages, kindly provided by Jared
Davis. ACL2 documentation strings may now link to external web pages
using the new symbol,
The user now has more control over how ACL2 prints forms; See print-control. Thanks to Bob Boyer for useful discussions leading to this enhancement.
Some Common Lisp implementations only allow the syntax
Ill-formed documentation strings need not cause an error. See
(For Lisp programmers) Macro
Sped up guard generation for some functions with large if-then-else structures in their bodies. Thanks to Sol Swords for sending an illustrative example.
Sped up guard generation in some cases by evaluating ground
(variable-free) subexpressions. Thanks to Bob Boyer for sending a motivating
Modified slightly a heuristic association of ``size'' with constants, which
can result in significant speed-ups in proofs involving constants that are
Added a restriction in the linear arithmetic procedure for deleting polynomial inequalities from the linear database. Formerly, an inequality could be deleted if it was implied by another inequality. Now, such deletion requires that certain heuristic ``parent tree'' information is at least as restrictive for the weaker inequality as for the stronger. Thanks to Dave Greve for bringing a relevant example to our attention and working with us to figure out some surprising behavior, and to Robert Krug for making a key observation leading to the fix.
(GCL especially) Improved compiled code slightly by communicating to raw
Lisp the output type when a function body is of the form
Applied a correction suggested by Robert Krug to the variant of term-order used in parts of ACL2's arithmetic reasoning.
Fixed bugs in the handling of flet expressions, one of which had
the capability of rendering ACL2 unsound. Thanks to Sol Swords for pointing
out two issues and sending examples. One example illustrated how ACL2 was in
essence throwing away outer flet bindings when processing an inner
(in-package "ACL2") (defun a (x) (list 'c x)) ; Example from Sol Swords, which failed to be admitted (claiming that ; function A is undefined) without the above definition of A. (defun foo1 (x y) (flet ((a (x) (list 'a x))) (flet ((b (y) (list 'b y))) (b (a (list x y)))))) (defthm not-true (equal (foo1 3 4) '(b (c (3 4)))) :hints (("Goal" :in-theory (disable (:executable-counterpart foo1)))) :rule-classes nil) (defthm contradiction nil :hints (("Goal" :use not-true)) :rule-classes nil)
Sol's second example, below, pointed to a second bug related to computing
output signatures in the presence of nested
Fixed a subtle soundness bug in the forming of constraints from deduced
type prescriptions. As a result, when ACL2 prints a warning message labeling
encapsulated functions as ``subversive'', ACL2 will no longer deduce
Fixed a long-standing soundness bug in compress1 and compress2, whose raw Lisp code gave the logically incorrect result in the
case of a single entry other than the header, where that entry mapped
an index to the default value. Also fixed soundness bugs in compress1, in the case of
(in-package "ACL2") (defthm true-formula-1 (equal (compress1 'a '((:HEADER :DIMENSIONS (4) :MAXIMUM-LENGTH 5 :DEFAULT 1 :NAME A :ORDER <) (1 . 1))) '((:HEADER :DIMENSIONS (4) :MAXIMUM-LENGTH 5 :DEFAULT 1 :NAME A :ORDER <))) :hints (("Goal" :in-theory (disable (compress1)))) :rule-classes nil) (defthm ouch-1 nil :hints (("Goal" :use true-formula-1)) :rule-classes nil) (defthm true-formula-2 (equal (compress1 'a '((:HEADER :DIMENSIONS (4) :MAXIMUM-LENGTH 5 :DEFAULT NIL :NAME A :ORDER >) (1 . 1) (2 . 2))) '((:HEADER :DIMENSIONS (4) :MAXIMUM-LENGTH 5 :DEFAULT NIL :NAME A :ORDER >) (2 . 2) (1 . 1))) :hints (("Goal" :in-theory (disable (compress1)))) :rule-classes nil) (defthm ouch-2 nil :hints (("Goal" :use true-formula-2)) :rule-classes nil) (defthm true-formula-3 (equal (compress1 'a '((:HEADER :DIMENSIONS (3) :MAXIMUM-LENGTH 4 :NAME A :ORDER >) (1 . B) (0 . A))) '((:HEADER :DIMENSIONS (3) :MAXIMUM-LENGTH 4 :NAME A :ORDER >) (1 . B) (0 . A))) :hints (("Goal" :in-theory (disable (compress1)))) :rule-classes nil) (defthm ouch-3 nil :hints (("Goal" :use true-formula-3)) :rule-classes nil)
Fixed a soundness bug involving measured subsets and verify-termination, by changing verify-termination so that it uses make-event. See verify-termination, in particular the discussion about make-event near the end of that documentation topic. Peter Dillinger first raised the idea to us of making such a change; when we found this soundness bug, we were certainly happy to do so!
Fixed a bug that could cause a hard Lisp error but not, apparently,
unsoundness. The bug was in the lack of attention to the order of guard and
type declarations when checking for redundancy. In the following example, the
second definition was redundant during the first pass of the encapsulate form. The second definition, however, was stored on the second
pass with a guard of
(encapsulate () (local (defun foo (x) (declare (xargs :guard (consp x))) (declare (xargs :guard (consp (car x)))) x)) (defun foo (x) (declare (xargs :guard (consp (car x)))) (declare (xargs :guard (consp x))) x)) ; Now we get a hard Lisp error from evaluation of the guard of foo: (foo 3)
Fixed a bug in the guard violation report for function intern-in-package-of-symbol. Thanks to Dave Greve for bringing this bug to our attention.
Made a change to allow certain hints, in particular certain
ACL2 now properly handles interrupts (via control-c) issued during printing of the checkpoint summary. Previously it was possible on some platforms to make ACL2 hang when interrupting both during a proof and during the ensuing printing of the checkpoint summary. Thanks to Jared Davis and Sol Swords for bringing this problem to our attention.
Fixed a bug that was preventing, inside some book
(GCL and CCL only) Fixed a bug in certain under-the-hood type inferencing.
Thanks to Sol Swords for sending an example using stobjs defined with
Fixed a bug in print-gv, which was mishandling calls of functions with more than one argument.
Fixed a bug in the handling of and and or terms by the
Fixed printing of goal names resulting from the application of
Fixed proof-tree printing so that interrupts will not cause problems with hiding ordinary output because of incomplete proof-tree output. Thanks to Peter Dillinger for pointing out this issue.
Fixed a bug that could cause simplifications to fail because of alleged ``specious simplification.'' This bug could appear when deriving an equality from the linear arithmetic database, and then attempting to add this equality to the current goal's hypotheses when it was already present. Thanks to Eric Smith for sending a helpful example (in July 2005!) that helped us debug this issue.
Fixed a bug in processing of
Fixed a bug that was causing an error, at least for an underlying Lisp of CCL (OpenMCL), when ec-call was applied to a term returning multiple values. Thanks to Sol Swords for sending an example that brought this bug to our attention.
Fixed handling of array orders to treat keyword value
Contrary to existing documentation (see make-event-details), the
value of ``ld special variable'' ld-skip-proofsp was always
We have disallowed the certification of a book when not at the top-level,
either directly in the top-level loop or at the top level of ld.
Before this restriction, the following would certify a book with a definition
(er-progn (defun h (x) x) (certify-book "my-book"))
But a subsequent include-book of
Printing with fmt directive
(SBCL, CMUCL, and CCL only) Fixed a bug in sys-call-status in the case that the underlying Common Lisp is SBCL, CMUCL, or CCL (OpenMCL). Thanks to Jun Sawada for bringing this bug to our attention and providing a fix.
Fixed a bug evidenced by error message ``Unexpected form in certification world'', which could result from attempting to certify a book after evaluating an encapsulate form with a local defmacro. Thanks to Jared Davis for pointing out this bug and sending the example:
(encapsulate () (local (defmacro foo (x) `(table foo 'bar ,x))) (local (foo 3)))
Formerly, evaluating a trace$ form inside a wormhole such as the break-rewrite loop could leave the user in a bad state after returning to the top level, in which that function could not be untraced. This has been fixed. Note however that when you proceed from a break in the break-rewrite loop, the tracing state will be the same as it was when you entered that break: all effects of calling trace$ and untrace$ are erased when you proceed from the break.
A bug has been fixed that could result in needlessly weak induction schemes
in the case that a recursive call is made in the first argument of prog2$. This has been fixed by including prog2$ as a default
ruler-extender in the new ruler-extenders feature (see above, and see ruler-extenders). For details on this bug see Example 11 in distributed book
(For CCL/OpenMCL on Windows) ACL2 should now build on CCL (OpenMCL) on Windows. Thanks to David Rager for bringing this issue to our attention and helping with a fix that worked for CCL 1.2, and to the CCL team for improving handling of Windows-style filenames in CCL 1.3.
NEW AND UPDATED BOOKS
See ReleaseVersionNumbers for a list of books in Version 3.5 of ACL2 but not Version 3.4.
Run the shell command
svn log -r 94:HEAD
to see all changes to
Here are just a few highlights.
Thanks largely to Jared Davis, many
(include-book "arithmetic-5/top" :dir :system) (include-book "rtl/rel8/lib/top" :dir :system)
Modified distributed file
(defvar acl2-skip-shell nil) (setq acl2-skip-shell t)
EXPERIMENTAL HONS VERSION
Bob Boyer and others have contributed numerous changes for the experimental
The ACL2 state can now be queried with