ACL2 Version 5.0 (August, 2012) 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 4.3 into the following categories of changes: existing features, new features, heuristic improvements, bug fixes, changes at the system level and to 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.
NOTE: ACL2 is now distributed under Version 2 of the GNU General Public License. [Added later: The license has changed since Version_5.0. See LICENSE.] Formerly, any later version had been acceptable. Moreover, books are no longer distributed from a University of Texas website, but rather, from Google Code at the ACL2 Books Downloads page.
CHANGES TO EXISTING FEATURES
A fatal error now occurs if environment variable
We now avoid certain duplicate conjuncts in the constraint stored
for encapsulate events. For example, the constraint stored for
the following event formerly included
(encapsulate ((foop (x) t)) (local (defun foop (x) (declare (ignore x)) t)) (defthm foop-constraints (and (booleanp (foop x)) (equal (foop (cons x y)) (foop y))) :rule-classes ((:type-prescription :corollary (booleanp (foop x))) (:rewrite :corollary (equal (foop (cons x y)) (foop y))))))
The test for redundancy (see redundant-events) of encapsulate events has been improved in cases involving redefinition (see ld-redefinition-action). Thanks to Jared Davis for providing the following example, which illustrates the problem.
(redef!) (encapsulate () (defun g (x) (+ 3 x))) (g 0) ; 3, as expected (encapsulate () (defun g (x) (+ 4 x))) (g 0) ; 4, as expected ; Unfortunately, the following was flagged as redundant because it agreed ; with the first encapsulate above. That has been fixed; now, it is ; recognized as not being redundant. (encapsulate () (defun g (x) (+ 3 x)))
The test for redundancy of defun and defconst events has been improved in the case that redefinition is active. In that case, redundancy now additionally requires that the ``translated'' body is unchanged, i.e., even after expanding macro calls and replacing constants (defined by defconst) with their values. Thanks to Sol Swords for requesting this enhancement, and to Jared Davis for pointing out a bug in a preliminary change. See redundant-events, in particular the ``Note About Unfortunate Redundancies''. Note that this additional requirement was already in force for redundancy of defmacro events.
The macro defmacro-last and the table return-last-table have been modified so that when they give special treatment
to a macro
We removed a barrier to admitting function definitions, as we explain using the following example.
(defun foo (m state) (declare (xargs :stobjs state)) (if (consp m) (let ((state (f-put-global 'last-m m state))) (foo (cdr m) state)) state))
Previously, ACL2 complained that it could not determine the outputs of the let form, as is necessary in order to ensure that state is returned by it. ACL2 now works harder to solve this problem as well as the analogous problem for mv-let and, more generally for mutual-recursion. (The main idea is to reverse the order of processing the if branches if necessary.) We thank Sol Swords for contributing a version of the above example and requesting this improvement.
It is no longer the case that break-on-error causes a Lisp break when encountering an error during translation of user input into internal (translated) form (see term). The reason is that an improvement to the translation process, specifically the one described in the preceding paragraph, allows certain backtracking from ``errors'', which are intended to be silent rather than causing breaks into raw Lisp. Thanks to Jared Davis for sending an example leading to this change.
(CCL and SBCL only) When the host Lisp is CCL or SBCL, then since all
functions are compiled, a certify-book command will no longer load the
newly-compiled file (and similarly for include-book with argument
Set-write-acl2x now returns an error triple and can take more values, some of which automatically allow including uncertified books when certify-book is called with argument :acl2x t.
The environment variable
The macros defthmd and defund no longer return an error
triple with value
For those who use set-write-ACL2x: now, when certify-book
is called without a
We have eliminated some hypotheses in built-in rewrite rules
Added the symbols f-get-global, f-put-global, and state-global-let* to
Added to the guards of push-untouchable and remove-untouchable the requirement that the second argument must be a Boolean. Thanks to Jared Davis for sending an example that led to this change.
The built-in function
All trust tags are now in the keyword package. The defttag
event may still take a symbol in an arbitrary package, but the trust tag
created will be in the keyword package (with the same symbol-name as
the symbol provided). Similarly, non-
There have been several changes to gag-mode. It is now is initially
An error now occurs if ld is called while loading a compiled book. See calling-ld-in-bad-contexts. Thanks to David Rager for reporting a low-level assertion failure that led us to make this change.
The proof-builder interactive loop is more robust: most errors will leave you in that loop, rather than kicking you out of the proof-builder and thus back to the main ACL2 read-eval-print loop. Thanks to David Hardin for suggesting this improvement in the case of errors arising from extra right parentheses.
The summary at the end of a proof now prints the following note when appropriate:
[NOTE: A goal of NIL was generated. See :DOC nil-goal.]
Improved dmr to show the function being called in the case of
explicit evaluation: ``
It is now permitted to bind any number of stobjs to themselves in
the bindings of a let expression. But if any stobj is bound to other
than itself in let bindings, then there still must be only one binding
The macro top-level now returns without error; See top-level. Formerly, this macro always returned an error triple
It is no longer the case that when you specify xargs keyword
(defun foo (x) (declare (xargs :guard t :non-executable t :mode :logic)) (prog2$ (throw-nonexec-error 'bar (list x)) (cons 3 x))) (defn h (x) (foo x))
After certifying this book and then including it in a new session, the
behavior occurred that is displayed below; notice the mention of
ACL2 !>(h 3) ACL2 Error in TOP-LEVEL: ACL2 cannot ev the call of undefined function BAR on argument list: (3) To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 !>
A tautology checker used in the ACL2 sources (function
The behavior of backquote (
(let ((x 3) (y 2) (z 7)) `(,x ,y ,@z))
Formerly, evaluation of this form had caused a guard violation in the ACL2
loop unless guard-checking was off (i.e., set-guard-checking was
A call of the theory macro had previously returned
The function booleanp is now defined using eq instead of equal, which may increase its efficiency. Thanks to Jared Davis for this change.
A new ``tau system'' provides a kind of ``type checker.'' See tau-system. Thanks to Dave Greve for supplying a motivating example (on which this system can provide significant speedup), and to Sol Swords for sending a very helpful bug report on a preliminary implementation.
Users may now arrange for additional summary information to be printed at
the end of events. [Note added at Version_6.1: Formerly we pointed
A new, advanced proof-builder command,
A new reader macro,
New proof-builder commands
It is now legal to call non-executable functions without the usual signature restrictions imposed on executable code. For example, the third event below was not admissible, but now it is.
(defstobj foo fld) (defun-nx id (x) x) (defun f (foo) (declare (xargs :stobjs foo :verify-guards nil)) (cons 3 (id foo)))
Thanks to Jared Davis for requesting this enhancement, in particular for
calling non-executable functions in the
(defstobj foo (fld)) (defun-nx my-identity (x) x) (defun my-fld (foo) (declare (xargs :stobjs foo)) (mbe :logic (my-identity foo) :exec (let ((val (fld foo))) (update-fld val foo))))
A new macro, non-exec, allows the use of non-executable code, for example inside ordinary function definitions. Thanks to Sol Swords for requesting this enhancement.
A new ``provisional certification'' process is supported that can allow books to be certified before their included sub-books have been certified, thus allowing for potentially much greater `make'-level parallelism. See provisional-certification. Thanks to Jared Davis for requesting this feature and for helpful discussions, based in part on rudimentary provisional certification schemes that he developed first at Rockwell Collins and later for his `Milawa' project. Also, thanks to Jared and to Sol Swords for testing this feature and for providing a fix for a bug in a preliminary implementation, and thanks to Sol for providing performance feedback and a crucial suggestion that led to an improved implementation.
Event summaries now show the names of events that were mentioned in hints of type
ACL2 now stores a data structure representing the relation ``Event A is used in the proof of Event B.'' See dead-events, which explains this data structure and mentions one application: to identify dead code and unused theorems. Thanks to Shilpi Goel for requesting such a feature and for helpful feedback.
A new documentation topic provides a guide to programming with state; see programming-with-state. Thanks to Sarah Weissman for suggesting that such a guide might be useful, and to David Rager for helpful feedback on a preliminary version. There also has been some corresponding reorganization of the documentation as well as creation of additional documentation (e.g., see state-global-let*). Now, most built-in functions and macros commonly used in programs (as opposed to events like defun, for example) are subtopics of a new topic — see ACL2-built-ins — which is a subtopic of programming, a topic that in turn has considerably fewer direct subtopics than before.
It is now possible to bind extra variables in a
A stobj may now be passed as an argument where another stobj is
expected if the two are ``congruent''. See defstobj, in particular,
its discussion of the new
A new top-level utility has been provided that shows the assembly language
for a defined function symbol; see disassemble$. Thanks to Jared Davis
for requesting such a utility and to Shilpi Goel for pointing out an
inconvenience with the initial implementation. Note that it uses the
A new documentation topic lists lesser-known and advanced ACL2 features, intended for those with prior ACL2 experience who wish to extend their knowledge of ACL2 capabilities. See advanced-features. Thanks to Warren Hunt and Anna Slobodova for requesting such information.
A new macro, deftheory-static, provides a variant of deftheory such that the resulting theory is the same at include-book
time as it was at certify-book time. Thanks to Robert Krug for
helpful discussions on this new feature and for updating his
A new event, defabsstobj, provides a new way to introduce single-threaded objects (see stobj and see defstobj). These so-called ``abstract stobjs'' permit user-provided logical definitions for primitive operations on stobjs, for example using an alist-based representation instead of a list-based representation for array fields. Moreover, the proof obligations guarantee that the recognizer is preserved; hence the implementation avoids executing the recognizer, which may be an arbitrarily complex invariant that otherwise would be an expensive part of guard checks. Thanks to Warren Hunt for a request leading us to design and implement this new feature, and thanks to Rob Sumners for a request leading us to implement a related utility, defabsstobj-missing-events. See defabsstobj. Also thanks to Sol Swords for sending an example exhibiting a bug in the initial implementation, which has been fixed.
A new command,
The new macro defnd defines a function with
The macros add-macro-fn and remove-macro-fn replace macros
add-binop and remove-binop, respectively, though the latter
continue to work. The new macros allow you to decide whether or not to
display calls of binary macros as flat calls for right-associated arguments,
It is now possible to request that the host Lisp compiler inline calls of specified functions, or to direct that the host Lisp compiler not inline such calls. See defun-inline and see defun-notinline. We thank Jared Davis for several extensive, relevant conversations, and for finding a bug in a preliminary implementation. We also thank others who have engaged in discussions with us about inlining for ACL2; besides Jared Davis, we recall such conversations with Rob Sumners, Dave Greve, and Shilpi Goel.
Reading of ACL2 arrays (see aref1, see aref2) has been made more efficient (as tested with CCL as the host Lisp) in the case of consecutive repeated reads of the same named array. Thanks to Jared Davis and Sol Swords for contributing this improvement.
Slightly modified the induction schemes stored, so that calls of so-called ``guard-holders'' (such as mbe and prog2$ — indeed, any call of return-last — and the) are expanded away. In particular, calls of equality variants such as member are treated as their corresponding function calls, e.g., member-equal; see equality-variants. Guard-holders are also now expanded away before storing constraints for encapsulate events, which can sometimes result in simpler constraints.
Improved the performance of dmr (technical note: by modifying raw
Lisp code for function
We now avoid certain rewriting loops. A long comment about this change,
including an example of a loop that no longer occurs, may be found in source
Slightly strengthened type-set reasoning at the level of literals
(i.e., top-level hypotheses and conclusions). See the comment in ACL2 source
Strengthened the ability of type-set reasoning to make deductions
about terms being integers or non-integer rationals. The following example
illustrates the enhancement: before the change, no simplification was
performed, but after the change, the conclusion simplifies to
(defstub foo (x) t) (thm ; should reduce conclusion to (foo t) (implies (and (rationalp x) (rationalp y) (integerp (+ x (* 1/3 y)))) (foo (integerp (+ y (* 3 x))))))
Fixed a class of soundness bugs involving each of the following functions:
getenv$, get-wormhole-status, cpu-core-count, wormhole-p, random$,
(defthm not-true (stringp (cadr (getenv$ "PWD" (build-state)))) :rule-classes nil) (defthm contradiction nil :hints (("Goal" :in-theory (disable (getenv$)) :use not-true)) :rule-classes nil)
Fixed a soundness bug involving
Fixed a soundness bug based on the use of skip-proofs together with
the little-used argument
Fixed a soundness bug that allowed users to define new proof-builder
primitive commands. Before this fix, a book proving
(Technical change, primarily related to make-event:) Plugged a
security hole that allowed books' certificates to be out-of-date
with respect to make-event expansions, but not recognized as such.
The change is to include the so-called expansion-alist in the certificate's
checksum. An example appears in a comment in the ACL2 sources, in
Fixed a bug in guard verification due to expanding calls of primitives when translating user-level terms to internal form, so called ``translated terms'' (see term). While we have not observed a soundness hole due to this bug, we have not ruled it out. Before the bug fix, the following event was admissible, as guard verification succeeded (but clearly should not have).
(defun f () (declare (xargs :guard t)) (car (identity 3)))
For those who want details about this bug, we analyze how ACL2 generates
guard proof obligations for this example. During that process, it
evaluates ground subexpressions. Thus,
While calls of many event macros had been prohibited inside executable code, others should have been but were not. For example, the following was formerly allowed.
(defun foo (state) (declare (xargs :mode :program :stobjs state)) (add-custom-keyword-hint :my-hint (identity nil))) (foo state) ; Caused hard raw Lisp error!
Thus, several event macros (including for example add-custom-keyword-hint) may no longer be called inside executable code.
Fixed an assertion that could occur, for example, after reverting to prove
the original goal by induction and generating a goal of
It was possible for defstobj to generate raw Lisp code with
excessively restrictive type declarations. This has been fixed. Thanks to
Warren Hunt for reporting this bug and sending an example that illustrates it.
See stobj-example-2 for examples of such raw Lisp code; now, one finds
Fixed a bug in that was ignoring the use of
Fixed a bug in the output from defattach, which was failing to list previous events in the message about ``bypassing constraints that have been proved when processing the event(s)''.
(GCL only) Fixed a bug in set-debugger-enable (which was only a bug in GCL, not an issue for other host Lisps).
Fixed ACL2 trace output to indent properly for levels above 99 (up to 9999). Thanks to Warren Hunt for bringing this bug to our attention.
Fixed a bug in the reporting of times in event summaries — probably one that has been very long-standing! The times reported had often been too small in the case of compound events, notably include-book. Thanks to everyone who reported this problem (we have a record of emails from Eric Smith and Jared Davis on this issue).
Fixed a bug in
(defund foo (x) (cons x x)) (thm (equal (car (foo x)) x) :hints (("Goal" :expand (:lambdas (foo x)))))
Certain ``program-only'' function calls will now cause hard Lisp errors.
(The rather obscure reason for this fix is to support logical modeling of the
ACL2 evaluator. A relevant technical discussion may be found in source
There was an unnecessary restriction that flet-bound functions must
return all stobjs among their inputs. For example, the following
definition was rejected because
(defun foo (state) (declare (xargs :stobjs state)) (flet ((h (state) (f-boundp-global 'x state))) (h state)))
We fixed a bug, introduced in the preceding release (Version 4.3), in the check for irrelevant formals (see irrelevant-formals). That check had been too lenient in its handling of lambda (let) expressions, for example allowing the following definition to be admitted in spite of its first formal parameter obviously being irrelevant.
(defun foo (x clk) (if (zp clk) :diverge (let ((clk (1- clk))) (foo x clk))))
Fixed a bug in the
Fixed a bug that occurred when certify-book was called after using set-fmt-soft-right-margin or set-fmt-hard-right-margin to set a small right margin.
Fixed set-inhibit-warnings so that it takes effect for a subsequent include-book event. Thanks to Jared Davis and David Rager for queries that led to this fix.
Hard Lisp errors are now avoided for certain
Fixed a bug in the ACL2 evaluator (source function
Fixed a hard Lisp error that could occur for ill-formed
It is now an error to include a stobj name in the
Some bogus warnings about non-recursive function symbols have been
eliminated for rules of class
(Allegro CL host Lisp only) Fixed an obsolete setting of compiler variable
Fixed a proof-builder bug that could result in duplicate goal names
in the case of forced hypotheses. An example showing this bug, before the
fix, appears in a comment in the ACL2 sources, in
We fixed a bug in a prover routine involved in type-set computations involving linear arithmetic. This bug has been around since at least as far back as Version_3.3 (released November, 2007). We are not aware of any resulting unsoundness, though it did have the potential to weaken the prover. For example, the following is proved now, but was not proved before the bug was fixed.
(thm (implies (and (rationalp x) (rationalp y) (integerp (+ (* 1/3 y) x))) (integerp (+ y (* 3 x)))) :hints (("Goal" :in-theory (disable commutativity-of-+))))
Although all bets are off when using redefinition (see ld-redefinition-action), we wish to minimize negative effects of its use, especially raw Lisp errors. The examples below had caused raw Lisp errors, but no longer.
(defstobj st fld :inline t) (redef!) (defstobj st new0 fld) (u) (fld st) ; previously an error, which is now fixed ; Fresh ACL2 session: (redef!) (defun foo (x) x) (defmacro foo (x) `(quote ,x)) (u) ; Fresh ACL2 session: (redef!) (defmacro foo (x) (cons 'list x)) (defun foo (x) x)
Fixed a bug that could cause hard Lisp errors in an encapsulate
event. Thanks to Sol Swords for sending an example that exhibited this bug.
Here is a simpler such example; the bug was in how it was checked whether the
guard for a guard-verified function (here,
(encapsulate ((f (x) t)) (local (defun f (x) (declare (xargs :guard t)) x)) (defun g (x) (declare (xargs :guard (if (integerp x) (f x) t))) x))
Fixed a bug in
#+skip #!acl2(quote 3)
This bug has been fixed.
Fixed a bug in the break-rewrite utility, which was evidenced by error messages that could occur when dealing with free variables. An example of such an error message is the following; we thank Robert Krug for sending us an example that produced this error and enabled us to produce a fix.
HARD ACL2 ERROR in TILDE-@-FAILURE-REASON-PHRASE1: Unrecognized failure reason, ((MEM-ARRAY . X86) (ADDR QUOTE 9)).
We fixed an obscure bug that we believe could interfere with defproxy because of an incorrect
CHANGES AT THE SYSTEM LEVEL AND TO DISTRIBUTED BOOKS
Improvements have been made related to the reading of characters. In
particular, checks are now done for ASCII encoding and for the expected char-code values for
The character encoding for reading from files has been fixed at ISO-8859-1. See character-encoding. Thanks to Jared Davis for bringing this portability issue to our attention (as this change arose in order to deal with a change in the default character encoding for the host Lisp, CCL), and pointing us in the right direction for dealing with it. In many cases, the character encoding for reading from the terminal is also ISO-8859-1; but this is not guaranteed. In particular, when the host Lisp is SBCL this may not be the case.
Although the HTML documentation is distributed with ACL2, it had not been
possible for users to build that documentation without omitting graphics, for
example on the ACL2 home page. That has been fixed, as files
Compiler warnings are suppressed more completely than they had been before. For example, the following had produced a compiler warning when the host Lisp is CCL, but no longer does so.
(defun f () (car 3)) (trace$ f)
Removed support for ``tainted'' certificates. One reason is that there are rarely incremental releases. A stronger reason is that for the compatibility of a new release is with the previous non-incremental release, it's not particularly relevant whether or not the new release is incremental.
The `make' variable
(SBCL only) ACL2 images built on SBCL now have an option,
The default value for variable
For the version supporting the reals, ACL2(r) (see real), the
(defun f () (declare (xargs :guard t)) (floor1 8/3)) (f) ; had caused raw Lisp error, before the fix
Among the enhancements for the parallel version, ACL2(p) (see parallelism), are the following. We thank David Rager for his work in developing ACL2(p) and these improvements in particular.
set-parallel-evaluationhas been renamed set-parallel-execution.
Calls of the macro set-waterfall-printing are no longer events, so may not be placed at the top level of books. However, it is easy to create events that have these effects; see set-waterfall-printing. Note that now,
:ubt and similar commands do not change the settings for either waterfall-parallelism or waterfall-printing.
The implementation of deflock has been improved. Now, the macro it defines can provide a lock when invoked inside a guard-verified or
:program mode function. Previously, this was only the case if the function definition was loaded from raw Lisp, typically via a compiled file.
The underlying implementation for waterfall parallelism (see set-waterfall-parallelism) has been improved. As a result, even the largest proofs in the regression suite can be run efficiently in
:resource-basedwaterfall parallelism mode. Among these improvements is one that can prevent machines from rebooting because operating system limits have been exceeded; thanks to Robert Krug for bringing this issue to our attention.
There is also a new flag for configuring the way waterfall parallelism behaves once underlying system resource limits are reached. This flag is most relevant to
:fullwaterfall parallelism. see set-total-parallelism-work-limit for more information.
The dmr utility has the same behavior in ACL2(p) as it has in ACL2 unless waterfall-parallelism has been set to a non-
nilvalue (see set-waterfall-parallelism), in which case statistics about parallel execution are printed instead of the usual information.
The user can now build the regression suite using waterfall parallelism. See the distributed file
acl2-customization-files/READMEfor details, and see unsupported-waterfall-parallelism-features for a disclaimer related to building the regression suite using waterfall parallelism.
When building ACL2 with both the hons and parallelism extensions (what is called ``ACL2(p)'' or, equivalently, ``ACL2(hp)''), the functions that are automatically memoized by the hons extension are now automatically unmemoized and memoized when the user toggles waterfall parallelism on and off, respectively.
Calling set-waterfall-parallelism with a flag of
tnow results in the same settings as if it were called with a flag of :resource-based, which is now the recommended mode for waterfall parallelism. Thanks to Shilpi Goel for requesting this feature.
The prover now aborts in a timely way in response to interrupts issued during a proof with waterfall parallelism enabled. (This had often not been the case.) Thanks to Shilpi Goel for requesting this improvement.
Among the enhancements for the HONS extension (see hons-and-memoization) are the following.
The compact-print code has been replaced by new serialization routines contributed by Jared Davis. This may improve performance when including books that contain make-events that expand to very large constants. You can also now save objects to disk without going into raw lisp; see serialize for details.
Printing of certain messages has been sped up (by using Lisp function
force-outputin place of finish-output). Thanks to Jared Davis for contributing this improvement.
Stobj array writes are perhaps twice as fast.
It is now permitted to memoize functions that take user-defined stobjs as inputs, provided that no stobjs are returned. Even if stobjs are returned, memoization is permitted provided the condition is
nil, as when profiling (see profile). Thanks to Sol Swords for an observation that led to this improvement and for useful conversations, including follow-up leading us to improve our initial implementation.
Fixes have been made for memoizing with a non-
nilvalue of :ideal-okp. Errors had occurred when memoizing with a :conditionother than tfor a :logic mode function that had not been guard-verified, even with a non- nilvalue of :ideal-okp; and after successfully memoizing such a function (without such :condition), it had not been possible to unmemoize it. Thanks to Sol Swords for reporting issues with the :ideal-okpargument of memoize.
If a book defined a function that was subsequently memoized in that book, the function would no longer behaves as memoized upon completion of book certification (unless that certify-book command was undone and replaced by evaluation of a corresponding include-book command). This has been fixed. Thanks to David Rager for pointing out the problem by sending an example.
We now support ACL2(h) built not only on 64-bit CCL but also on all supported host Ansi Common Lisps (i.e., all supported host Lisps except GCL). Thanks to Jared Davis for doing much of the work to make this improvement. Note that performance will likely be best for 64-bit CCL; for some Lisps, performance may be much worse, probably depending in part on the underlying implementation of hash tables.