ACL2 Version 4.2 (January, 2011) 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.2 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.
CHANGES TO EXISTING FEATURES
The accumulated-persistence utility can now do finer-grained
tracking, providing data for individual hypotheses and the conclusion of a
rule. See accumulated-persistence. To try this out, evaluate the form
The defattach utility now permits the use of
Redefinition (see ld-redefinition-action) is no longer permitted for
functions that have attachments (see defattach). In such cases, the
attachment must be removed first, e.g. with
Made small changes to mv-nth and defun-sk in order to permit guard verification of functions introduced with more than one quantified variable in a defun-sk form. The change to mv-nth is to weaken the guard by eliminating the requirement that the second argument satisfy true-listp, and replacing the call of endp in the definition body by a corresponding call of atom. The new definition of mv-nth is thus logically equivalent to the old definition, but with a weaker guard. Thanks to Sol Swords for sending the following example, for which the final verify-guards form had failed but now succeeds.
(defstub foo (a b c) nil) (defun-sk forall-a-b-foo (c) (declare (xargs :guard t :verify-guards nil)) (forall (a b) (foo a b c))) (verify-guards forall-a-b-foo)
The implementations of prog2$, time$, with-prover-time-limit, with-guard-checking, mbe (and must-be-equal), and ec-call have changed. See the discussion below
of the new utility, return-last. A consequence is that trace$
is explicitly disallowed for these and related symbols, which formerly could
cause hard Lisp errors, because they are now macros. Tracing of return-last
is also disallowed. Another consequence is that time$ now prints a more
abbreviated message by default, but a version of the old behavior can be
The following utilities no longer print an observation about raw-mode
The system function
Modified abort handling to avoid talking about an interrupt when the error was caused by a Lisp error rather than an interrupt.
The value of the constant
Improved the built-in `
The following only affects users who use trust tags to add to list values
of either of the state global variables
The guard of the macro intern has been strengthened so that
its second argument may no longer be either the symbol
(let ((x "ALLOCATE") (y 'car)) (implies (and (stringp x) (symbolp y) (equal (symbol-package-name y) "COMMON-LISP")) (equal (symbol-package-name (intern-in-package-of-symbol x y)) "SYSTEM")))
Now suppose that one includes a book with this theorem (with
The error message for free variables (e.g., in definition bodies and guards) now supplies additional information when there are governing IF conditions. Thanks to Jared Davis for requesting this enhancement and collaborating in its design.
Improved proof output in the case of a
The proof-builder command `
It is no longer permitted to submit definitions in
The macro verify-termination now provides clearer output in the
case that it is redundant. More important perhaps, as a courtesy it now
causes an error when applied to a constrained function, since presumably such
an application was unintended (as the constrained function could never have
Improved the guards for the following functions, often weakening
them, to reflect more precisely the requirements for calling eq:
See the discussion above about new statistics that can be gathered by the accumulated-persistence utility.
(For system hackers) There are new versions of system functions
A new utility, return-last, is now the unique ACL2 function that can pass back a multiple value result from one of its arguments. Thus, now the following are macros whose calls ultimately expand to calls of return-last: prog2$, time$, with-prover-time-limit, with-guard-checking, mbe (and must-be-equal), and ec-call. With an active trust tag, an advanced user can now write code that has side effects in raw Lisp; see return-last. Thanks to Jared Davis for requesting this feature.
A new function, pkg-imports, specifies the list of symbols imported into a given package. The axioms for defpkg have been strengthened, taking advantage of this function. Now one can prove theorems using ACL2 that we believe could not previously be proved using ACL2, for example the following.
(equal (symbol-package-name (intern-in-package-of-symbol str t)) (symbol-package-name (intern-in-package-of-symbol str nil)))
Added function no-duplicatesp-eq.
Added a new hint keyword,
Support is now provided for creating and certifying books that do not depend on trust tags, in the case that the only use of trust tags is during make-event expansion. See set-write-ACL2x. Thanks to Sol Swords for reporting a couple of bugs in a preliminary implementation.
See forward-chaining-reports for how to get new reports on the forward chaining activity occurring in your proof attempts. Thanks to Dave Greve for inspiring the addition of this utility.
It is now possible to use ACL2's printing utilities to return strings, by
opening output channels to the keyword
We have slightly improved the handling of
We have slightly improved the so-called ``type-set'' heuristics to
work a bit harder on terms of the form
We made three heuristic improvements in the way contexts (so-called ``type-alists'') are computed from goals (``clauses''). Although these changes did not noticeably affect timing results for the ACL2 regression suite, they can be very helpful for goals with many hypotheses. Thanks to Dave Greve for sending a useful example (one where we found a goal with 233 hypotheses!).
The algorithm for substituting alists into terms was modified. This change is unlikely to affect many users, but in one example it resulted in a speed-up of about 21%. Thanks to Dave Greve for supplying that example.
Sped up include-book a bit by memoizing checksums of symbols. (This change pertains to ``normal'' ACL2 only, not the hons version (see hons-and-memoization, where such memoization already occurred.) We found about a 23% speed-up on an example from Dave Greve.
Made a small change to the algorithm used to prove hypotheses of
Fixed a long-standing soundness bug caused by the interaction of forced hypotheses with destructor elimination. The fix was to avoid
using forcing when building the context (so-called ``type-alist'') when the
goal is considered for destructor elimination; those who are interested can
see a discussion in source function
Fixed a bug that allowed book certification to ignore
Fixed a bug that could occur when including a book that attempts to
redefine a function as a macro, or vice-versa. (For details of the issue, see
the comment in the definition of variable
(Windows only) Fixed handling of the Windows drive so that an executable image saved on one machine can be used on another, even with a different drive. Thanks to Harsh Raju Chamarthi for reporting this issue and doing a lot of testing and collaboration to help us get this right.
Made a change to avoid possible low-level errors, such as bus errors, when quitting ACL2 by calling good-bye or its synonyms. This was occurring in CCL, and we are grateful to Gary Byers for helping us find the source of those errors (which basically was that ACL2 was attempting to quit while already in the process of quitting).
Fixed a bug in with-guard-checking, which was being ignored in function bodies.
In some host Lisps, it has been possible to be in a situation where it is impossible to interrupt checkpoint printing during the summary. We had thought this solved when the host Lisp was CCL, but Sol Swords sent us an example (for which we are grateful) illustrating that this behavior could occur. This has been fixed.
Fixed a bug in a proof obligation generated for
Fixed the following bugs in defattach. We hadn't always been applying the full functional substitution when generating guard proof obligations. We had been able to hit an assertion when reattaching to more than one function. Attachment was permitted in the case of an untouchable function (see remove-untouchable). Finally, the guard proof obligation could fail in the case that the two functions have different formal parameter lists, as in the following example.
(encapsulate ((foo (x) x :guard (symbolp x))) (local (defun foo (x) x))) (defun bar (x2) (declare (xargs :guard (symbolp x2))) x2) (defattach foo bar)
Fixed a raw Lisp error that could be caused by including a book using
make-event to define a function symbol in a locally-introduced
package. An example appears in a comment in ACL2 source function
Made a change that can prevent an error near the end of book certification
when the underlying Host Lisp is Allegro Common Lisp, in the case that
Fixed a bug that was failing to substitute fully using bindings of free
variables in forced hypotheses. A related change is that instead of
binding such a free variable to a new variable of the form
Fixed a bug that could inhibit the printing of certain theory warnings (and probably, in the other direction, cause inappropriate such printing).
We eliminated excessive
It is now possible to evaluate stobj-related forms after evaluating
ACL2 !>(defstobj st fld) Summary Form: ( DEFSTOBJ ST ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ST ACL2 !>(set-guard-checking :none) Turning off guard checking entirely. To allow execution in raw Lisp for functions with guards other than T, while continuing to mask guard violations, :SET-GUARD-CHECKING NIL. See :DOC set-guard-checking. ACL2 >(fld st) ACL2 Error in TOP-LEVEL: The guard for the function call (FLD ST), which is (STP ST), is violated by the arguments in the call (FLD ST). [... etc. ...]
You can understand how things now work by imagining that when a function
introduced by defstobj is called, guard-checking values of
Fixed a bug in which the wrong attachment could be made when the same
function has an attachment in a book and another in the certification world of
that book (possibly even built into ACL2), if the load of a compiled file is
aborted because a sub-book's compiled file is missing. The bug has been
present since the time that defattach was added (Version_4.0). An
example may be found in a comment in the deflabel for
It had been the case that in raw-mode (see set-raw-mode), it was possible to confuse include-book when including a book in a directory different from the current directory. This has been fixed. Thanks to Hanbing Liu for bringing this problem to our attention with a small example.
NEW AND UPDATED BOOKS AND RELATED INFRASTRUCTURE
Many changes have been made to the distributed books, thanks to an active
ACL2 community. You can contribute books and obtain updates between ACL2
releases by visiting the ACL2 Books web page. [Note: This release note is
obsolete, as it referenced the now-invalid URL,
There is new
The documentation for make-event now points to a new book,
Incorporated a version of changes from Jared Davis to the
We refrain from listing changes here to experimental versions, other than
an enhancement to the hons version that can reduce sizes of certificate files, by applying hons-copy to introduce structure
sharing (ACL2 source function