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.
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
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
(accumulated-persistence :all); then see accumulated-persistence for a
discussion of display options using
to Dave Greve for suggesting this new capability and collaborating on its
design and implementation.
defattach utility now permits the use of
functions, though this requires the use of a trust tag (see defttag).
See defattach and for discussion of the new capability, see defproxy,
which explains how part of this change involves allowing
mode functions to be declared non-executable.
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
(defattach foo nil).
Made small changes to
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
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) (forall (a b) (foo a b c)) :witness-dcls ((declare (Xargs :guard t :verify-guards nil)))) (verify-guards forall-a-b-foo)
The implementations of
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 obtained with
The following utilities no longer print an observation about raw-mode
set-raw-mode-off. Thanks to Jared Davis for suggestion this change
in the case of
include-book (which proved awkward to restrict to that
The system function
translate-and-test now permits its
LAMBDA form to
refer to the variable
WORLD, which is bound to the current ACL2 logical
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
*acl2-exports*, which is still a list, has been
extended significantly, though only with the addition of symbols that one
might reasonably have expected all along to belong to this list. A new
books/misc/check-acl2-exports.lisp, checks (at
certification time) that no documented constant, macro, or function symbol in
"ACL2" package has been accidentally omitted from
*acl2-exports*. Thanks to Dave Greve for helpful discussions related to
Improved the built-in `
untranslate' functions to produce
expressions when appropriate (more to help with tools that call
untranslate and the like, than to help with proof output).
redo-flat now works for
certify-book failures, just
as it continues to work for failures of
The following only affects users who use trust tags to add to list values of
either of the
state global variables
logic-fns-with-raw-code. For functions that belong to either of the
above two lists,
trace$ will supply a default value of
:notinline, to avoid discarding raw-Lisp code for the function.
The guard of the macro
intern has been strengthened so that its
second argument may no longer be either the symbol
*main-lisp-package-name* or the string
"COMMON-LISP". That change
supports another change, namely that the following symbols in the
"COMMON-LISP" package are no longer allowed into ACL2: symbols in that
package that are not members of the list constant
*common-lisp-symbols-from-main-lisp-package* yet are imported into the
"COMMON-LISP" package from another package. See pkg-imports and
see symbol-package-name. To see why we made that change, consider for
example the following theorem, which ACL2 was able to prove when the host
Lisp is GCL.
(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
nil), using an ACL2 built on top of a different host Lisp, say CCL, that does not import the symbol
"COMMON-LISP"package. Then then one can prove
nilby giving this theorem as a
The axioms introduced by
defpkg have changed. See the discussion of
pkg-imports under ``NEW FEATURES'' below.
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.
redef- now turns off redefinition.
Improved proof output in the case of a
clause-processor hint that
proves the goal, so that the clause-processor function name is printed.
proof-checker command `
then' now stops at the first failure (if
It is no longer permitted to submit definitions in
:logic mode for merely
part of an existing
mutual-recursion event. Such an action left the
user in an odd state and seemed a potential soundness hole.
break$ is now in
logic mode. Thanks to Jared
Davis for requesting this enhancement.
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 been
program mode). Note that if one desires different behavior,
one can create one's own version of
verify-termination (but with a
Improved the guards for the following functions, often weakening them,
to reflect more precisely the requirements for calling
union-eq. Thanks to Jared Davis for pointing
out this issue for
(CCL only) Made a change that can reduce the size of a compiled file produced
certify-book when the host Lisp is CCL, by discarding source
information (for example, discarding
See the discussion above about new statistics that can be gathered by the
A new hint,
instructions, allows use of the proof-checker at
the level of hints to the prover. Thanks to Pete Manolios for
requesting this feature (in 2001!). See instructions.
(For system hackers) There are new versions of system functions
translate-cmp respectively, that do not take or return
the Essay on Context-message Pairs for relevant information. Thanks to David
Rager for collaborating on this enhancement.
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
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
(equal (symbol-package-name (intern-in-package-of-symbol str t)) (symbol-package-name (intern-in-package-of-symbol str nil)))Thanks to Sol Swords for a helpful report, which included the example above. See pkg-imports and see defpkg.
Added a new hint keyword,
backchain-limit-rw, to control the level
of backchaining for rewrite, meta, and linear rules. This
overrides, for the current goal and (as with
descendent goals, the default backchain-limit
(see set-backchain-limit). Thanks to Jared Davis for requesting this
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.
(file-write-date$ filename state) has been added, giving the
write date of the given file.
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
:STRING rather than to filenames.
See io. Thanks to Jared Davis for a helpful conversation that led us to add
We have slightly improved the handling of
rules that contain free variables. Formerly, such rules might fire only
once, when the first match for a free variable is discovered, and would
not fire again even if subsequent forward chaining made available another
match. This made it difficult to predict whether a rule with free
variables would fire or not, depending as it did on the order in which
newly derived conclusions were added. The new handling is a little
slower but more predictable. Thanks to Dave Greve for sending a helpful
example that led us to consider making such an improvement.
We have slightly improved the so-called ``type-set'' heuristics to work
a bit harder on terms of the form
(rec term), where
rec is a
so-called ``compound-recognizer'' function, that is, a function with a
compound-recognizer rule. Thanks to Jared
Davis for sending a helpful example (found, in essence, in the modified
type-set-rec, source file
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.
include-book a bit by memoizing checksums of symbols. (This
change pertains to ``normal'' ACL2 only, not the
(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
type-prescription rules (ACL2 source function
type-set-relieve-hyps). One change avoids a linear walk through the context
(the ``type-alist'' structure), while the other could avoid storing
forced assumptions (into the so-called ``tag-tree'').
Fixed a long-standing soundness bug caused by the interaction of
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
includes a proof of
nil that no longer succeeds. A similar fix was made
for generalization, though we have not exploited the previous code to prove
nil in that case.
Fixed a bug that allowed book certification to ignore
encapsulate events. Thus, a book could contain an event of the
(skip-proofs (encapsulate ...)), and a call of
that book could succeed even without supplying keyword
:skip-proofs-okp t. This bug was introduced in Version 3.5 (May,
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
Fixed a bug in
top-level, which was not reverting the logical
world when an error resulted from evaluation of the given form. Thanks
to Jared Davis for bringing this bug to our attention.
Fixed a long-standing bug (back through Version 2.7) that was discarding
changes to the connected book directory (see cbd) when exiting and then
re-entering the top-level ACL2 loop (with
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
clause-processor rules, that the guard on the metafunction or
fn, holds under suitable assumptions. Those
assumptions include not only that the first argument of
pseudo-termp, but also that all stobj inputs satisfy the
corresponding stobj recognizer predicates. We had erroneously considered
stobj outputs of
fn instead of stobj inputs. Thanks to Sol Swords for
bringing this bug to our attention with a simple example, and correctly
pointing us to the bug in our code.
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
ACL2_SYSTEM_BOOKS has been set to the name of a
directory with a parent that is a soft link. Thanks to Dave Greve for
supplying an example to led us to this fix, which involves avoiding Allegro
CL's implementation of the Common Lisp function,
Fixed a bug that was failing to substitute fully using bindings of free
forced hypotheses. A related change is that instead of
binding such a free variable to a new variable of the form
???-Y, the new
variable is now 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
"Raw-mode" warnings about
add-include-book-dir that could be generated by the use of raw-mode
include-book. Thanks to Dave Greve for bringing this issue to
Fixed the printing of results from forms within an
encapsulate, so that
they are abbreviated according to the
It is now possible to evaluate stobj-related forms after evaluating
nil, even in cases where such evaluation formerly caused a guard
violation due to a bug in ACL2. Here is an example of an error that no
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
guard-checking values of
nilare temporarily converted to
t. Thanks to Pete Manolios, Ian Johnson, and Harsh Raju Chamarthi for requesting this improvement.
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
(ACL2 source file
doc and related utilities now cause a clean error when
provided other than a symbol. Thanks to Jared Davis for pointing out the raw
Lisp error that had occurred in such cases.
It had been the case that in raw-mode (see set-raw-mode), it was possible to
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 project web page,
There is new
Makefile support for certifying just some of the distributed
books. See book-makefiles, in particular discussion of the variable
ACL2_BOOK_DIRS. Thanks to Sandip Ray for requesting this enhancement.
The documentation for
make-event now points to a new book,
books/make-event/defrule.lisp, that shows how
make-event can be used to
do macroexpansion before generating events. Thanks to Carl Eastlund for
useful interaction on the acl2-help mailing list that led us to add this
Incorporated a version of changes from Jared Davis to the
emacs utility (distributed file
emacs/emacs-acl2.el), so that one can
fill a format string from anywhere within the string.
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