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, 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.
CHANGES TO EXISTING FEATURES
Significant changes have been made for list-processing primitives such as
assoc; see equality-variants. In summary: instead of
separate functions based on
equal, there is
essentially just one function, which is based on
eql variants are logically just the
equal variant. For
member are macros that generate
corresponding calls of
member-equal in the logic, although in raw Lisp
they will execute using tests
References to any of these in logical contexts such as theories are now
references to the function based on
equal; for example, the hint
:in-theory (disable member) is completely equivalent to the hint
:in-theory (disable member-equal). Distributed books have been
modified as necessary to accommodate this change. While the need for such
changes was relatively infrequent, changes were for example needed in
contexts where terms are manipulated directly; for example,
defevaluator needs to mention
member-equal rather than
member, just as it was already the case to mention, say,
binary-append rather than
append. Again, see equality-variants
for more information about equality variants.
A few improvements were made in support of the modified treatment of equality variants discussed above. The changes include the following.
o We now allow the use of macro aliases (see macro-aliases-table in
:trigger-fnsof rules (see rule-classes).
o We now remove so-called ``guard holders'' (including calls of
return-last, hence of
o We also remove guard holders in formulas of
intersection-eqcan now take any positive number of arguments, and
union-eqcan take zero arguments. (Thanks to Jared Davis for requesting this enhancement.) The same can be said for new macros
o A few changes were made to built-in theorems from source file
axioms.lisp, in particular disabling
consp-assoc-equal(formerly two enabled rules,
consp-assoc) but adding this theorem as a
:forward-chainingrule, and similarly for
true-list-listp-forward-to-true-listp-assoc-equal(and eliminating rule
true-list-listp-forward-to-true-listp-assoc-eq; and disabling rule
true-listp-cadr-assoc-eq-for-open-channels-p. Also, theorem
all-boundp-preserves-assochas been renamed to
all-boundp-preserves-assoc-equaland also strengthened.
o Some guards were slightly improved (logically weaker or the same).
get-output-stream-string$ to allow for a context and to do
genuine error printing instead of using
cw. See io.
Added the symbols
A small change was made to the processing of more than one
declaration for the same function. In particular, a guard of
Attachments are now allowed during evaluation of the first argument of
prog2$ even in contexts (such as proofs) during which the use of
attachments is normally prohibited. More generally, the second of the three
return-last has this property, except in the case of
mbe (or related macros like
mbe1), where the
may provide the value. Thanks to Sol Swords for useful discussions leading
us to implement this enhancement.
The restriction has been removed that prohibited the use of
encapsulate events with a non-empty signature. This
restriction was introduced in Version 3.4, but has not been necessary since
Version 4.0, when we first started disallowing guard verification for
functions introduced non-locally inside such
We weakened the checks involving common ancestors for evaluator and
meta (and clause-processor) functions (see evaluator-restrictions)
so that except in the
mbe case, the next-to-last argument of
return-last is not considered. Thanks to Sol Swords for bringing this
issue to our attention.
append no longer requires at least two arguments. Thanks to
Dave Greve for requesting this enhancement.
(Mostly for system hackers) Now,
break-on-error breaks at a more
appropriate (earlier) time for certain system functions that do not return
state, such as
translate11. Thanks to David Rager for requesting this
Show-accumulated-persistence may take a new argument,
simply causes an alphabetical list of runes to be printed out.
trace$ so that
:cond forms may
state even if the function being traced does not include
state as a formal.
The system function
acl2x-expansion-alist now takes a second argument,
state. This change allows for more flexibility in the sorts of
attachments that can be made to this function (see defattach). Thanks to
Jared Davis and Sol Swords for requesting this enhancement and providing a
An obscure proof-checker change, unlikely to affect users, replaces the
state global variables
are now untouchable (see set-fmt-hard-right-margin and
see push-untouchable). If you bind these
state globals with
state-global-let*, then you will need to do so with appropriate
setters to restore their values, for example as follows.
(state-global-let* ((fmt-hard-right-margin 500 set-fmt-hard-right-margin) (fmt-soft-right-margin 480 set-fmt-soft-right-margin)) ...)
The error message has been improved for the case of evaluating an undefined function that has an attachment (see defattach). Thanks to Jared Davis for sending the following example, which illustrates the additional part of the message.
ACL2 !>(defstub foo (x) t) [[... output omitted ...]] ACL2 !>(defattach foo identity) [[... output omitted ...]] ACL2 !>(defconst *x* (foo 3)) ACL2 Error in ( DEFCONST *X* ...): ACL2 cannot ev the call of undefined function FOO on argument list: (3) Note that because of logical considerations, attachments (including IDENTITY) must not be called in this context. [[... additional output omitted ...]]
The directory string supplied to
add-include-book-dir no longer must
terminate with the `
/' character, as had been required in some Lisp
implementations. Thanks to Sol Swords for bringing this issue to our
We no longer print induction schemes with gag-mode; use
if you want to see them. Thanks to Dave Greve for this suggestion.
It is now legal to supply a constant for a stobj array dimension. See defstobj. Thanks to Warren Hunt for requesting this enhancement.
We cleaned up a few issues with
o It is no longer illegal to submit a
defpkgform in raw-mode (see set-raw-mode). Thanks to Jun Sawada for reporting an example in which an
include-bookform submitted in raw-mode caused an error because of a `hidden'
defpkgform (see hidden-defpkg). There will no longer be an error in such cases.
o It had been the case that locally including a book could make it possible to use a package defined by that book. Consider for example the following book,
foo.lisp.(in-package "ACL2") (local (include-book "arithmetic/top" :dir :system))After certifying this book, it had been possible to admit the following events in a new session.(include-book "foo") (defconst acl2-asg::*foo* 3) (defconst *c* 'acl2-asg::xyz)In Version_4.3, neither of these
defconstevents is admitted.
o A hard Lisp error is now avoided that had been possible in rare cases when including books with hidden packages (see hidden-defpkg). An example may be found in a comment in the
note-4-3(in ACL2 source file
The undocumented (but sometimes useful) functions
are now guard-verified
logic mode functions. Thanks to
Sandip Ray for requesting this enhancement.
It had been the case that when including a book, functions defined in the book's certification world (that is, in its portcullis commands) were typically not given compiled code. That has been fixed.
pl2 have been improved, primarily
by printing information for more rule classes. See pl and see pl2. See
also the item below about the new proof-checker command,
mv? extend the funtionality of
mv (respectively) to the case of a single value.
Macro with-local-state is available for system programmers who wish bind
state locally, essentially using with-local-stobj. But this
should only be done with extreme care, and it requires an active trust tag;
Formatted printing functions now have analogues that print to strings and do
not take an output channel or
state as arguments.
The system function
ancestors-check is now available for verified
modification by users, i.e., attachment using
(defattach ancestors-check <your_function>). Thanks to Robert Krug for
providing the necessary proof support, which we modified only in small ways.
warning$-cw, provide formatted
observations and warnings (respectively) without
state. Thanks to Harsh Raju Chamarthi and David Rager for requests
leading to these utilities.
Observation-cw is now used in some of the
distributed books (thanks to Robert Krug for useful interaction for that).
The proof-checker command
type-alist (see proof-checker-commands)
now takes an optional third argument that causes the production of
forward-chaining reports (see forward-chaining-reports). Thanks to Dave
Greve for requesting such an enhancement.
The reports generated by forward-chaining, forward-chaining-reports,
have been changed to indicate when a conclusion reached by forward chaining
REDUNDANT with respect to the type information already known. Thanks
to Dave Greve for suggesting this enhancement.
with-prover-time-limit is now legal for events
(see embedded-event-form). For example, the following is now legal.
(encapsulate () (with-prover-time-limit 2 (defthm append-assoc (equal (append (append x y) z) (append x (append y z))))))
The new utility
with-prover-step-limit is analogous to the utility
with-prover-time-limit, but counts ``prover steps'' rather than
checking for time elapsed. See with-prover-step-limit. Also
see set-prover-step-limit to provide a default step-limit. Note that just
with-prover-time-limit may now be used to create events, as
discussed just above,
with-prover-step-limit may also be used to create
events. Thanks to Carl Eastlund for requesting support for step-limits.
progn$ is analogous to
prog2$, but allows an arbitrary
number of arguments. For example:
ACL2 !>:trans1 (progn$ (f1 x) (f2 x) (f3 x)) (PROG2$ (F1 X) (PROG2$ (F2 X) (F3 X))) ACL2 !>Thanks to David Rager for contributing this macro.
defattach may now be supplied the argument
:skip-checks :cycles. In this case, as with argument
a trust tag is reuired (see defttag), and no logical claims are made. The
effect is to avoid the usual check that the extended ancestor relation has no
cycles (see defattach). Thanks to Dave Greve for requesting this feature.
You can now limit the printing of subgoal names when using
:goals. See set-print-clause-ids. Thanks to
Karl Hoech for a suggestion leading to this enhancement.
A new proof-checker command,
short, provides information about
type-prescription rules that
match a given term. Thanks to Dave Greve for requesting this enhancement.
See also the item above about related improvements to commands
ACL2 now avoids some repeated attempts to rewrite hypotheses of rewrite rules. See set-rw-cache-state for a discussion of this behavior and how to avoid it. The default behavior has been observed to reduce by 11% the overall time required to complete a regression. Here are the directories that had the top three time decreases and top three time increases, shown in seconds.
-368 coi/gacc (1064 down to 696: decrease of 35%) -220 workshops/1999/ste (664 down to 444: decrease of 33%) -148 unicode (331 down to 183: decrease of 45%) .... +7 workshops/2002/cowles-flat/support (229 up to 236: increase of 3%) +8 workshops/1999/ivy/ivy-v2/ivy-sources (508 up to 516: increase of 2%) +12 workshops/2009/hardin/deque-stobj (78 up to 91: increase of 17%)
The so-called ``ancestors check,'' which is used to limit backchaining, has
been strengthened so that two calls of
equal are considered the same
even if their arguments appear in the opposite order. Thanks to Robert Krug
for providing an implementation and a useful discussion.
The check for irrelevant-formals in processing of
defuns has been
made more efficient. Thanks to Eric Smith for reporting this issue in 2001
(!) and thanks to Warren Hunt for recently sending an example. For that
example, we have seen the time for the irrelevant-formals check reduced
from about 10 seconds to about 0.04 seconds.
(GCL only) The macro
mv has been modified so that certain fixnum boxing
can be avoided.
(Allegro CL only) We have set to
nil four Allegro CL variables that
otherwise enable storing of certain source information (for details, see the
discussion of ``cross-referencing'' in ACL2 source file
As a result of this change we have about a 6% speedup on the regression
suite, but a 27% time reduction on an example that includes a lot of books.
Exhaustive matching for the case of free-variables has been extended to
type-prescription rules, in analogy to the default setting
:match-free :all already in place for rewrite, linear, and
forward-chaining rules. See free-variables-type-prescription. Thanks
to Dave Greve for requesting this enhancement.
A soundness bug was fixed in some raw-Lisp code implementing the function,
take. Thanks to Sol Swords for pointing out this bug with
(essentially) the following proof of
(defthmd take-1-nil-logic (equal (take 1 nil) '(nil)) :hints(("Goal" :in-theory (disable (take))))) (thm nil :hints (("Goal" :use take-1-nil-logic)))
mbe in ``safe-mode'' situations -- i.e., during evaluation
defpkg forms, and during
macroexpansion -- are now guard-checked. Thus, in these situations both
:exec forms will be evaluated, with an error if the
results are not equal. Formerly, only the
:logic form was evaluated,
which was a soundness bug that could be exploited to prove
nil. For a
such a proof and a bit of further explanation, see the example at the top of
the comments for
(deflabel note-4-3 ..) in ACL2 source file
It had been possible to prove
nil by proving the following
theorem using ACL2 built on CCL and then proving its negation using
ACL2 built on a different host Lisp.
(defthm host-lisp-is-ccl (equal (cdr (assoc 'host-lisp *initial-global-table*)) :ccl) :rule-classes nil)This hole has been plugged by moving the setting of
'host-lispout of the constant
trace$ for arguments that are stobj accessors or updaters.
It also gives an informative error in this case when the accessor or updater
is a macro (because the introducing
defstobj event specified
Avoided a potential error that could occur when no user home directory is
located. Our previous solution for Windows simply avoided looking for ACL2
customization files (see acl2-customization) and
acl2-init.lsp files in
a user's home directory. With this change, we handle such files the same for
Windows as for non-Windows systems: we always look for ACL2 customization
files (see acl2-customization) and
acl2-init.lsp files in a user's home
directory, but only if such a directory exists. Thanks to Hanbing Liu for
reporting this issue.
(GCL only) Fixed a bug that prevented the use of
get-output-stream-string$ when the host Lisp is GCL.
with-live-state to work properly for executable
counterparts (so-called ``*1*'' functions).
Fixed a bug in the error message caused by violating the guard of a macro call.
Fixed a bug in an error message that one could get when calling
defattach with argument
:skip-checks t to attach to a
program mode function symbol that was introduced with
defun. (This is indeed an error, but the message was confusing.)
Thanks to Robert Krug for bringing this bug to our attention.
Fixed a bug in the loop-checking done on behalf of
could miss a loop. For an example, see the comment about loop-checking in
the comments for
(deflabel note-4-3 ..) in ACL2 source file
Terms of the form
(hide <term>) without free variables could be
simplified, contrary to the purpose of
hide. This is no longer the
case, Thanks to Dave Greve for reporting this issue.
An infinite loop could occur when an error was encountered in a call of
wormhole-eval, for example with the following form, and this has been
(wormhole-eval 'demo '(lambda () (er hard 'my-top "Got an error!")) nil)
Fixed a bug in detection of package redefinition. While we have no example demonstrating this as a soundness bug, we cannot rule it out.
Fixed a bug in the message produced by an erroneous call of
Thanks to Jared Davis for reporting this bug and sending a helpful example.
For a failed
defthm event, we now avoid printing
runes that are used only in processing proposed rules to be stored, but
not in the proof itself. Thanks to Dave Greve for sending us an example that
led us to make this fix.
ACL2 did not reliably enforce the restriction against non-
include-book events inside
encapsulate events, as
illustrated by the following examples.
; not permitted (as expected) (encapsulate () (include-book "foo")) ; permitted (as expected) (encapsulate () (local (include-book "foo"))) ; formerly permitted (surprisingly); now, not permitted (local (encapsulate () (include-book "foo")))Moreover, the corresponding error message has been fixed. Thanks to Jared Davis and Sandip Ray for relevant discussions.
include-book is given a first argument that is not a string, a
more graceful error now occurs, where previously an ugly raw Lisp error had
occurred. Thanks to Eric Smith for bringing this bug to our attention.
Fixed a bug in an error message that was printed when an unexpected
expression has occurred where a
declare form is expected.
(Since all functions are compiled when the host Lisp is CCL or SBCL, the
following bug fix did not occur for those host Lisps.) After evaluation of
t), all defined functions are expected to run
with compiled code; but this was not the case for functions exported from an
encapsulate event. This has been fixed.
It had been the case that the
puff command was broken for
include-book form whose book had been certified in a world with an
add-include-book-dir event. This has been fixed.
Evaluation of stobj updaters (see defstobj) may no longer use
attachments (see defattach). This is a subtle point that will likely not
affect many users. Thanks to Jared Davis for bringing this issue to our
attention; a slight variant of his example appears in a comment in ACL2
It had been the case that even when a stobj creator function was
declared to be untouchable (see push-untouchable), a
form based on that same stobj was permitted. Now, such forms are not
admitted. Thanks to Jared Davis for a query leading to this fix.
Fixed a buggy message upon guard violations, which was suggesting the
(set-guard-checking :none) in some cases when guard-checking was
already set to
It had been possible to get a hard Lisp error when computing with
ec-call in books. The following is an example of such a book,
whose certification no longer causes an error.
(in-package "ACL2") (defun f (x) x) (defconst *c* (ec-call (f 3))) (defun g (x) (cons x x))
pl2, and also the proof-checker commands
show-rewrites (and hence their respective aliases
sr), now take rule-id arguments that can be
runes. These commands dealt with definition rules already, e.g.
:pl2 (append x y) binary-appendbut they did not allow explicit specification of
:pl2 (append x y) (:definition binary-append)
The following example illustrates a bug in the processing of (admittedly
obscure) hints of the form
:do-not-induct name, where
nil. In this example,
ACL2 had essentially ignored the hint and reverted to prove the original goal
by induction, rather than to skip the goal temporarily as is expected for
such hints. Thanks to David Rager for a helpful discussion.
(thm (and (equal (append (append x y) z) (append x y z)) (equal (append (append x2 y2) z2) (append x2 y2 z2))) :hints (("Subgoal 1" :do-not-induct some-name)))
Fixed a slight bug in the definitions of built-in
example, in a fresh ACL2 session the value of the following form is
but formerly included several
(let ((world (w state))) (set-difference-theories (function-theory :here) (function-theory 'ground-zero)))
CHANGES AT THE SYSTEM LEVEL AND TO DISTRIBUTED BOOKS
Many changes have been made to the distributed books, as recorded in svn logs under the `Source' and 'Updates' links at http://acl2-books.googlecode.com/. Here we list some of the more significant changes.
o A large library has been graciously contributed by the formal verification group at Centaur Technology. See
books/centaur/and, in particular, file
books/centaur/README, which explains how the library depends on the experimental HONS extension (see hons-and-memoization).
o Among the new books is an illustration of
books/misc/defattach-example.lisp, as well as a variant of defattach that avoids the need for guard verification,
o Distributed book
books/misc/trace1.lisphas been deleted. It had provided slightly more friendly trace output for new users, but distributed book
books/misc/trace-star.lispmay be better suited for that purpose.
ACL2 can once again be built on LispWorks (i.e., as the host Lisp), at least
with LispWorks 6.0. Thanks to David Rager for useful conversations.
Several changes have been made from previous LispWorks-based ACL2
o ACL2 now starts up in its read-eval-print loop.
o You can save an image with
o Multiprocessing is not enabled.
o The stack size is managed using a LispWorks variable that causes the stack to grow as needed.
o When ACL2 is built a script file is written, as is done for other host Lisps. Thus, (assuming that no
PREFIX is specified),
just a small text file that invokes a binary executable, which for Lispworks
The HTML documentation no longer has extra newlines in <pre> environments.
Statistics on ACL2 code size may be found in distributed file
doc/acl2-code-size.txt. This file and other information can be found in
a new documentation topic, about-acl2.
Fixed the build process to pay attention to environment variable
ACL2_SYSTEM_BOOKS (which may be supplied as a command-line argument to
make'). An ACL2 executable can thus now be built even when there is no
books/ subdirectory if a suitable replacement directory is supplied.
Some warnings from the host Lisp are now suppressed that could formerly appear. For example, the warnings shown below occurs in Version 4.2 using Allegro CL, but not in Version 4.3.
ACL2 !>(progn (set-ignore-ok t) (set-irrelevant-formals-ok t) (defun bar (x y) x)) [[.. output omitted ..]] BAR ACL2 !>:comp bar ; While compiling BAR: Warning: Variable Y is never used. ; While compiling (LABELS ACL2_*1*_ACL2::BAR ACL2_*1*_ACL2::BAR): Warning: Variable Y is never used. BAR ACL2 !>
The distributed Emacs file
emacs/emacs-acl2.el now indents calls of
warning$@par the same way that calls of
The parallel version (see parallelism) now supports parallel evaluation of the ``waterfall'' part of the ACL2 prover; see set-waterfall-parallelism. Thanks to David Rager for doing the primary design and implementation work.
A new macro,
spec-mv-let, supports speculative and parallel execution
in the parallel version, courtesy of David Rager.
Among the enhancements for the HONS version (see hons-and-memoization) are the following.
Memoized functions may now be traced (see trace$). Thanks to Sol Swords for requesting this enhancement.
logicmode functions that return
nil. Thanks to Sol Swords for this enhancement.
Memoizeis now explicitly illegal for constrained functions. (Already such memoization was ineffective.)
A new keyword argument,
:AOKP, controls whether or not to allow memoization to take advantage of attachments; see memoize and for relevant background, see defattach.
Memoizeis now illegal by default for
logicmode functions that have not had their guards verified. See memoize (keyword
:ideal-okp) and see acl2-defaults-table (key
:memoize-ideal-okp) for and explanation of this restriction and how to avoid it.
History commands such as
pbtnow display ``
M'' or ``
m'' to indicate memoized functions. See pc.