ACL2 Version 4.0 (July, 2010) 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.6.1 into the following categories of changes: existing features, new features, heuristic improvements, bug fixes, distributed books, Emacs support, and experimental versions. Each change is described in just one category, though of course many changes could be placed in more than one category. Also see note-3-6-1 for other changes since Version 3.6.
CHANGES TO EXISTING FEATURES
There have been extensive changes to the handling of compiled files for
books, which may generally be invisible to most users. The basic idea is that
when compiled files are loaded on behalf of include-book, they are now
loaded before events in the book are processed, not afterwards. This can
speed up calls of
It was possible to get a hard Lisp error when certifying a book with a
redundant defconst form whose term is not identical to the existing
defconst form for the same name. The following example illustrates
the problem, which has been fixed (as part of the change in handling of
compiled files for books, described above). Imagine that after the initial
ACL2 !>(defconst *a* nil) [[output omitted]] ACL2 !>(certify-book "foo" 1) [[initial output omitted] * Step 5: Compile the functions defined in "/v/joe/foo.lisp". Compiling /v/joe/foo.lisp. End of Pass 1. End of Pass 2. OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3 Finished compiling /vjoe/foo.lisp. Loading /v/joe/foo.lisp Error: Illegal attempt to redeclare the constant *A*.
The wormhole facility has been changed to repair a bug that allowed guard violations to go undetected. The major change has to do with the treatment of what used to be called the ``pseudo-flag'' argument which has been replaced by a quoted lambda expression. See note-4-0-wormhole-changes for help in converting calls of wormhole. Also see see wormhole and see wormhole-eval.
The ACL2 tutorial has been greatly expanded, for example to include a self-contained discussion of rewriting. See ACL2-tutorial.
Formerly, the mbe macro and must-be-equal function were disallowed in any definition within an encapsulate having a non-empty signature. Now, these are allowed provided the definition has been declared to be non-executable (see defun-nx). As a result, defevaluator events may now include must-be-equal among the function symbols known by the evaluator; this had not previously been allowed. Thanks to Sol Swords for discussions leading to this relaxation for defevaluator.
Princ$ now prints strings more efficiently. Thanks to Jared Davis
for suggesting the improvements to
The use of xargs declaration
The documentation has been improved for explaining to advanced users
the details of the ACL2 hint mechanism; see hints-and-the-waterfall,
and see the example about
The definition of mv-let has been modified so that the single-step macroexpansion (see trans1) of its calls can be evaluated. Thanks to Pete Manolios for bringing this evaluation issue to our attention and ensuing discussions.
All calls of so-called ``guard-holders'' — prog2$, must-be-equal (from calls of see mbe), ec-call, and mv-list — are now removed before storing hypotheses of rules of class
(defthm foo (prog2$ (cw "asdf") (and (equal (car (cons x y)) x) (equal (cdr (cons x y)) y))))
The handling of fmt directive
Error messages have been improved for ill-formed terms (in ACL2's so-called ``translation'' routines). Thanks to Jared Davis for requesting such an enhancement.
Modified defun-sk so that it executes in
The ``system hacker'' commands
The function symbol
The user now has control over whether compilation is used, for example
whether or not certify-book compiles by default, using function
Modified the conversion of relative to absolute pathnames in portcullis commands for book certification. Now, more pathnames remain as relative pathnames.
On occasion, ACL2 prints the message ``Flushing current installed world'' as it cleans up when certain actions (installing a world) are interrupted. This operation has been sped up considerably. If your session includes many events, you can probably speed up any such operation further by invoking reset-prehistory. Thanks to Jared Davis for sending a query that led us to make this improvement.
Calls of the form
The underlying function for good-bye (and hence for exit
and quit) is now in
We now require that every function symbol in the signature of an
encapsulate event have a
The following functions now have raw Lisp implementations that may run
faster than their ACL2 definitions: assoc-eq, assoc-equal,
We now avoid infinite loops caused when tracing functions that implement trace$. Thanks to Rob Sumners and Eric Smith for useful discussions.
The implementation of trace! has been modified slightly, to accommodate the fix for ``some holes in the handling of trust tags'' described later, below.
This item applies unless the host Lisp is GCL. An interrupt (control-c)
will now cause a proof to exit normally in most cases, by simulating a
timeout, as though with-prover-time-limit had been called with a
time-limit of 0. If the first interrupt doesn't terminate the proof, a second
one should do so (because a different, more ``severe'' mechanism is used after
the first attempt). As a result, redo-flat should work as one might
expect even if a proof is interrupted. Thanks to Dave Greve for requesting
this enhancement to redo-flat. Technical note: for reasons related to
this change, time-limits are no longer checked in evaluator functions
It is now legal for proof-builder macro-commands to appear in
The value of
ACL2 !>(ld-post-eval-print state) ; default :COMMAND-CONVENTIONS ACL2 !>(ld-error-triples state) ; default T ACL2 !>(set-ld-error-triples nil state) *** Then, before the change: ACL2 !>(mv t 3 state) 3 *** Instead, after the change: ACL2 !>(mv t 3 state) (T 3 <state>)
The default behavior of ld has been changed. Formerly when an
error occurred that halted a subsidiary call of
(ld '((ld '((defun f (x) x) (defun bad (x)) ; ERROR -- missing the body )) (defun g (x) x)))
We have modified the generation of
(encapsulate ((f (x) t)) (local (defun f (x) x)) (defun g (x) (cons x (f x))) (defun h (x) (g x)) (defthm h-is-f (equal (car (h x)) x)))
Previously, the constraint on
The use of trace$ (or trace!) option
Several errors have been eliminated that formerly occurred when the
constraints for a function symbol were unknown because it was constrained
using a dependent clause-processor (see define-trusted-clause-processor. Now, it is assumed that the
The notion of constraint for functions introduced by defun
has been modified slightly. No longer do we remove from the body of the
definition calls of so-called ``guard-holders'': prog2$, must-be-equal, ec-call, and mv-list, and uses of
A new event, defattach, allows evaluation of calls of constrained (encapsulated) functions. In particular, users can now, in principle, soundly modify ACL2 source code; please feel free to contact the ACL2 implementors if you are interested in doing so. See defattach.
Eric Smith has noticed that if you exit the break-rewrite loop using
New function mv-list is the identity function logically, but
converts multiple values to lists. The first argument is the number of
values, so an example form is as follows, where
A new state global variable,
It is now possible to write documentation for HTML without error
when there are links to nonexistent documentation topics. See the comments in
It is now possible to inhibit specified parts of the Summary printed at the
conclusion of an event. See set-inhibited-summary-types. Also see
with-output, in particular the discussion of the new
It is now possible to defer and avoid some ttag-related output; see set-deferred-ttag-notes. Thanks to Jared Davis for requesting less verbosity from ttag-related output.
A new command,
ACL2 now provides a utility for canonicalizing filenames, so that soft
links are resolved; see canonical-pathname. Moreover, ACL2 uses this
utility in its own sources, which can eliminate some issues. In particular,
include-book with argument
You can now suppress or enable guard-checking for an individual form; see with-guard-checking. Thanks to Sol Swords for requesting this feature.
The walkabout utility has been documented (thanks to Rob Sumners
for suggesting this documentation). This utility can make it easy to explore
Rules of class
The so-called ``too-many-ifs'' heuristic has been modified. Such a heuristic has been employed in ACL2 (and previous Boyer-Moore provers) for many years, in order to limit the introduction of calls of if by non-recursive functions. Most users need not be concerned with this change, but two proofs in the regression suite (out of thousands) needed trivial adjustment, so user proofs could need tweaking. In one application, this modification sped up proofs by 15%; but the change in runtime for the regression suite is negligible, so such speedups may vary. Thanks to Sol Swords for providing a test from ACL2 runs at Centaur Technology, which was useful in re-tuning this heuristic.
Guard proof obligations could have size quadratic in the number of clauses
in a case statement. This inefficiency has been removed with a change
that eliminates a hypothesis of the form
We adjusted the heuristics for determining induction schemes in the presence of ruler-extenders, when handling calls of a function symbol that is a ruler-extender, in either of two cases: either the function takes only one argument; or the function is prog2$ or ec-call, and the first argument contains no recursive call. These cases are treated more directly as though the ruler-extender call is replaced by the unique (in the case of prog2$ and ec-call, the second) argument.
(implies (true-listp b) (true-listp (append a b)))
If you are interested in the motivation for adding this rule, see comments
The use of
The fundamental utility that turns an
Certification can now run faster (specifically, the compilation phase) for books with very large structures generated by make-event, when there is significant sharing of substructure, because of a custom optimization of the Lisp reader. Thanks to Sol Swords for bringing this efficiency issue to our attention.
Jared Davis reported inefficiency in certain make-event evaluation
due to a potentially expensive ``bad lisp object'' check on the expansion
produced by the
The application of rules of class
Heuristics have been tweaked so that false goals may be simplified to
Improved the efficiency of the built-in function, take. Thanks to Bob Boyer for suggesting this improvement.
ACL2 can now use evaluation to relieve hypotheses when applying
Evaluation has been sped up during theorems for calls of mv-let, by avoiding repeated evaluation of the expression to which its variables are bound. Thanks to Sol Swords for requesting this improvement and sending an illustrative example.
Modified a heuristic to avoid the opening up non-recursive function calls on calls of hide involving if-expressions. For example, the thm form below is now admitted
(defun bar (x) (cons x x)) (thm (equal (bar (hide (if a b c))) (cons (hide (if a b c)) (hide (if a b c)))))
Fixed a soundness bug in destructor elimination, which was preventing some
cases from being generated. Thanks to Eric Smith for reporting this bug and
sending a helpful example. (Technical detail: the fixes were in ACL2 source
Fixed a bug that supported a proof of
Changed the implementation of add-include-book-dir. The previous
implementation could allow relative pathnames to be stored in the portcullis commands of certificates of books, which
perhaps could lead to unsoundness (though we did not try to exploit this to
Fixed a soundness bug related to xargs keyword
;;;;;;;;;;;;;;;;;;;; ;;; Book sub.lisp ;;;;;;;;;;;;;;;;;;;; (in-package "ACL2") (defun f () (declare (xargs :guard t :non-executable t)) (mv-let (a b c) (mv 3 4) (declare (ignore a b)) c)) (defun g () (declare (xargs :guard t)) (prog2$ (mv-let (x y z) (mv 2 3 4) (declare (ignore x y z)) nil) (f))) (defthm g-nil (equal (g) nil) :hints (("Goal" :in-theory (disable (f)))) :rule-classes nil) ;;;;;;;;;;;;;;;;;;;; ;;; Book top.lisp ;;;;;;;;;;;;;;;;;;;; (in-package "ACL2") (include-book "sub") (defthm contradiction nil :hints (("Goal" :use g-nil)) :rule-classes nil)
The modification described above pertaining to defun-nx also
prevents execution of non-executable functions that have been traced.
The following example illustrates the problem; now, the following defun of
(defun g (x) ; Use defun-nx to avoid an error after Version_3.6.1. (declare (xargs :guard t :non-executable t)) x) (g 3) ; causes error, as expected (trace$ g) (g 3) ; returned 3 before the bug fix; after fix, causes error as expected
A hard error was possible when attempting to include an uncertified book
containing events of the form
Fixed a bug in the heuristic improvement described for Version_3.6 (see note-3-6) as ``We simplified induction schemes....'' The bug had prevented, in unusual cases such as the following (notice the impossible case), a proof by induction.
(defun foo (a x) (and (consp x) (case a (0 (foo (car x) (cdr x))) (1 (foo (cdr x) (car x))) (0 (foo a (cons x x)))))) (in-theory (disable (:type-prescription foo))) (thm (atom (foo a x)))
Macro cw-gstack did not work with an
Fixed a bug in
Fixed a bug in the handling of
Replaced a hard Lisp error with a clean error, in certain cases that a
Fixed a bug in the interaction of function tracing with conversion of a
(defun f (x) (declare (xargs :mode :program)) (car x)) (f 3) ; raw Lisp hard error (trace$ f) (f 3) ; raw Lisp hard error (still) (defun f (x) (car x)) ; upgrade f to :logic mode (f 3) ; clean guard violation; f is no longer traced (trace$) ; uh oh - f is shown as traced (untrace$ f) (f 3) ; OUCH: hard Lisp error because old :program mode definition of ; the executable counterpart (sometimes called *1*f) was restored!
Made a fix so that when building ACL2 with `make' option
Fixed a bug in the handling of override-hints that generate custom
keyword hints (see custom-keyword-hints) involving the variable
Fixed a bug that could make
(GCL only) Fixed a bug that could occur when calling
Proof summaries have been improved, so that they account for runes used in rewriting that takes place when generating goals to be proved in a forcing round. Thanks to Jared Davis for sending us an example illustrating this issue.
Fixed a bug that (at least in CCL) could put extra backslashes (`
We closed some holes in the handling of trust tags (also known as ``ttags''; see defttag) by include-book. The following example illustrates this rather subtle situation. Consider the following book.
(in-package "ACL2") (make-event (er-progn (encapsulate () (defttag :foo) (value-triple "Imagine something bad here!")) (value '(value-triple :some-value))) :check-expansion t)
Formerly, the following commands succeeded.
(certify-book "test3" 0 t :ttags :all) :u (include-book "test3" :ttags nil)
But because of make-event keyword argument
Closed a small loophole that had the potential, in rare circumstances, to violate atomicity of under-the-hood updates for ACL2 arrays.
The following example was formerly allowed, but resulted in a
guard-verified function (here,
(encapsulate ((f (x) t)) (local (defun f (x) (declare (xargs :guard t)) (consp x))) ;; ERROR! (defun g (x) (declare (xargs :guard (f x))) (car x)))
The use of
Fixed a bug that could cause a raw Lisp error when the first argument of with-local-stobj is not a symbol.
It had been possible to use the reserved keyword :computed-hints-replacement as the name of a custom keyword hint (see custom-keyword-hints). This has been fixed. Thanks to Dave Greve, who pointed out a confusing hint error message (which has also been fixed) that led us to this issue.
Fixed a bug that could cause a hard Lisp error, instead of a graceful ACL2
error, if keyword
Eliminated an error that could occur when redefining a function as a macro and then compiling, as in the example below.
(defun foo (x) x) :redef! (defmacro foo (x) x) :comp t
Thanks to Eric Smith for sending the above example in his bug report.
Fixed a bug that could result in an assertion when a clause-processor causes an error.
NEW AND UPDATED BOOKS AND RELATED INFRASTRUCTURE
See the log entries for a record of books changed or added since the preceding release, with log entries.
We note in particular the new
New utilities have been provided for certifying most of the distributed
books with more `make'-level parallelism. For example, we have obtained close
to a 12x reduction in time by using `
The top-level makefile,
The HONS version, supported primarily by Bob Boyer and Warren Hunt (see
hons-and-memoization), has undergone numerous improvements. For
example, keyword argument
David Rager contributed modifications to the parallel version (see parallelism), which include taking advantage of atomic increments available at least since Version 1.0.21 of SBCL and Version 1.3 of CCL.