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 3.3 into changes to existing features, new features, bug fixes, new and updated books, and Emacs support. Each change is described just once, though of course many changes could be placed in more than one category.
CHANGES TO EXISTING FEATURES
Fixed a long-standing potential infinite loop in the rewriter. Thanks to Sol
Swords for sending a concise example illustrating the looping behavior.
(Those interested in details are welcome to look at the comment about loop
behavior in source function
Incorporated a slight strengthening of non-linear arithmetic contributed by
Robert Krug (thanks, Robert). With non-linear arithmetic enabled, the
problem was essentially that ACL2 made the following ``optimization'': given
(< a u) and
(< b v), for positive rational constants
v of which at least one is known to be
(< (* a b) (* u v)). Without this optimization, however,
ACL2 now infers the stronger inequality obtained by direct multiplication of
the two given inequalities. To see the effect of this change, submit the
(set-non-linearp t) followed by:
(thm (implies (and (rationalp x) (< 3 x) (rationalp y) (< 4 y)) (< 0 (+ 12 (* -4 x) (* -3 y) (* x y)))))
set-checkpoint-summary-limit has been modified in several
ways: it now takes a single argument (no longer takes
state as an
argument); a natural number
n abbreviates the pair
(n . n); the
argument is no longer evaluated, but it still optionally may be quoted; and a
t, suppresses all printing of the checkpoint summary. Thanks
to Jared Davis for suggesting most of these improvements.
There was formerly a restriction on
mbe that the
:exec argument may
not contain a call of
mbe. This restriction has been removed, thanks
to a request from Jared Davis and Sol Swords. Thanks also to Sandip Ray, who
pointed out that this restriction may have been in place in order that
defexec can guarantee termination using the
:exec code; its
documentation has therefore been updated to clarify this situation.
Rules of class
rewrite are now stored by performing certain
logical simplifications on the left side of the conclusion:
(prog2$ X Y)
is replaced by
(mbe :logic X :exec Y) is replaced by
precisely, the analogous change is made to the generated call of
(the TYPE X) is replaced by
X (again, the
change is actually made on the macroexpanded form). Thanks to Jared Davis
and Sol Swords for requesting this change. An analogous change has also been
made for rules of class
trace$ utility has been reimplemented to work independently of the
underlying Lisp trace. It thus works the same for every host Lisp, except as
provided by an interface to the underlying host Lisp trace (the
option). Note that the host Lisp trace continues to be modified for GCL,
Allegro CL, and CCL (OpenMCL); see trace. See trace$ for updated detailed
documentation on tracing options, many of which are new, for example an
:evisc-tuple option that can be set to
:no-print if you want the
function traced without the usual entry and exit printing. The previous
trace$ had some issues, including the following, which have all been
fixed. Thanks to Peter Dillinger for assistance in determining desired
functionality of the new
trace$ and for helping to test it.
Recursive calls were not always shown in the trace for two reasons. (1) Compiler inlining could prevent recursive calls from being shown in the trace, in particular in CCL (OpenMCL). Thanks to Jared Davis and Warren Hunt for pointing out this issue and requesting a fix, and to Bob Boyer and Gary Byers for relevant helpful discussions. (2) ACL2's algorithm for producing executable counterparts prevented tracing of recursive calls even after
(set-guard-checking :none). Thanks to Peter Dillinger for requesting a fix.
It was possible to exploit a bug in the interaction of multiple values and trace to prove a contradiction. An example is in a comment in
(deflabel note-3-4 ...)in the ACL2 source code.
Certain large structures could cause expensive computations for printing even when a
:condcondition was specified and evaluated to
Trace!now suppresses printing of the event summary, and returns the value that would be returned (if there is an active trust tag) by the corresponding call of
Some bugs have been fixed in the underlying native trace installed by ACL2 for GCL, Allegro CL, and CCL (OpenMCL), including the following. In GCL it had been impossible to use the variable
:condexpression. In Allegro CL and CCL, a
trace$bug mishandled tracing non-ACL2 functions when directives such as
:exitwere supplied. GCL trace now hides the world even when tracing non-ACL2 functions. Tracing in CCL no longer causes a Lisp error when untracing a traced function defined outside the ACL2 loop; for example
(trace$ len1)followed by
(untrace$ len1)no longer causes an error.
wet has been changed, for the better we think. see wet.
The generation of goals for forcing-rounds has been changed to avoid
dropping assumptions formerly deemed ``irrelevant''. (A simple example may
be found in a comment in source function
prove.lisp.) Thanks to Jared Davis for sending us an example that
led us to make this change.
Modified the implementation of
make-event so that in the certificate
of a book,
local events arising from
make-event forms are
elided. For example, if
(make-event <form>) expands to
(local <expanded-form>), then where the latter had been stored in the
certificate, now instead
(local (value-triple :ELIDED)) will be stored.
Thanks to Eric Smith for requesting this improvement. He has reported that a
preliminary version of this improvement shrunk a couple of his
files from perhaps 40MB each to about 140K each.
table event that sets the entire table,
(table tbl nil alist :clear), is redundant (see redundant-events) when
alist is equal to the current value of the table. Thanks to
Peter Dillinger for requesting this change.
The event constructor
progn! now returns the value that is returned by
evaluation of its final form if no error occurs, except that it still returns
nil if the that final evaluation leaves ACL2 in raw-mode.
psog have been improved so that they show the
key checkpoint summary at the end of a failed proof.
(For a discussion of key checkpoints, see set-gag-mode.) As a result, a
set-checkpoint-summary-limit now affects subsequent evaluation
psog. In particular, you no longer need to
reconstruct a proof (by calling
defthm) in order to see
key checkpoints that were omitted due to the limit; just call
set-checkpoint-summary-limit and then run
The proof-checker behaves a little differently under gag-mode.
Now, proof-checker commands that call the theorem prover to create new
proof-checker goals, such as
(see proof-checker-commands), will show key checkpoints when in
gag-mode. As before, proof-checker commands
psog) -- see pso, see psog, and see pso! -- can then
show the unedited proof log. However, unlike proof attempts done in the ACL2
loop, such proof attempts will not show a summary of key checkpoints at the
end, because from a prover perspective, all such goals were considered to be
temporarily ``proved'' by giving them ``byes'', to be dispatched by later
A little-known feature had been that a measure of
0 was treated as
though no measure was given. This has been changed so that now, a
nil is treated as though no measure was given.
*acl2-exports* to include every documented symbol whose name
"SET-". Thanks to Jared Davis for remarking that
set-debugger-enable was omitted from
*acl2-exports*, which led to
The trace mechanism has been improved so that the
:multiplicity options can be used together for Lisps that support
:exit keyword. These Lisps include GCL and Allegro CL, whose
native trace utilities have been modified for ACL2. For SBCL and CCL
(OpenMCL), which use the built-in Lisp mechanism for returning multiple
values in ACL2 (see mv), the use of
remains unnecessary and will be ignored. In support of this change, the
modification of native Allegro CL tracing for ACL2 was fixed to handle
:exit forms correctly that involve
redef! is just like
redef, but prints a
warning rather than doing a query. The old version of
:redef! was for
system hackers and has been renamed to
Introduced a new utility for evaluating a function call using the so-called executable counterpart -- that is, executing the call in the logic rather than in raw Lisp. See ec-call. Thanks to Sol Swords for requesting this utility and participating in its high-level design.
See print-gv for a new utility that assists with debugging guard violations. Thanks to Jared Davis for requesting more tool assistance for debugging guard violations.
Improved the guard violation error message to show the positions of the formals, following to a suggestion of Peter Dillinger.
guard-debug capability to assist in debugging failed attempts
at guard verification. See guard-debug. Thanks to Jared Davis for
requesting a tool to assist in such debugging and to him, Robert Krug, and
Sandip Ray for useful discussions.
New utilities provide the formula to be proved by
See verify-guards-formula and see guard-obligation, Thanks to Mark Reitblatt
for making a request leading to these utilities. These utilities can be
applied to a term, not just an event name; thanks to Peter Dillinger for
correspondence that led to this extension.
A new utility causes runes to be printed as lists in proof output from simplification, as is done already in proof summaries. See set-raw-proof-format. Thanks to Jared Davis for requesting this utility.
An experimental capability allows for parallel evaluation. See parallelism. Thanks to David Rager for providing an initial implementation of this capability.
xor in analogy to
iff. Thanks to Bob Boyer, Warren Hunt,
and Sol Swords for providing this definition.
Improved distributed file
doc/write-acl2-html.lisp so that it can now be
used to build HTML documentation files for documentation strings in user
books. See the comment in the definition of macro
acl2::write-html-file at the end of that file. Thanks to Dave Greve and
John Powell for requesting this improvement.
It is now possible to specify
hints for non-recursive function
definitions (which can be useful when definitions are automatically
generated). See set-bogus-defun-hints-ok. Thanks to Sol Swords for
requesting such a capability.
:dir is now supported for
rebuild just as it has
We relaxed the criteria for functional substitutions, so that a function
symbol can be bound to a macro symbol that corresponds to a function symbol
in the sense of
macro-aliases-table. So for example, a functional
substitution can now contain the doublet
(f +), where previously it
would have been required instead to contain
We now allow arbitrary packages in raw mode (see set-raw-mode) -- thanks to Jared Davis for requesting this enhancement -- and more than that, we allow arbitrary Common Lisp in raw mode. Note however that for arbitrary packages, you need to be in raw mode when the input is read, not just when the input form is evaluated.
Two new keywords are supported by the
with-output macro. A
:gag-mode keyword argument suppresses some prover output as is done by
set-gag-mode. Thanks to Jared Davis for asking for a convenient way to
set gag-mode inside a book, in particular perhaps for a single theorem;
this keyword provides that capability. A
:stack keyword allows
encapsulate to ``pop'' the effect of
with-output call. Thanks to Peter Dillinger for requesting
such a feature. See with-output.
good-bye and its aliases
quit now all
take an optional status argument, which provides the Unix exit status for the
underlying process. Thanks to Florian Haftmann for sending a query to the
ACL2 email list that led to this enhancement.
Keyword commands now work for macros whose argument lists have lambda list
keywords. For a macro with a
lambda list keyword in its argument list,
the corresponding keyword command reads only the minimum number of required
arguments. See keyword-commands.
It is now legal to
(let* ((x (+ a b)) ...) (declare (ignorable x)) ...). Thanks to
Jared Davis for requesting this enhancement.
Added a warning when more than one hint is supplied explicitly for the same
goal. It continues to be the case that only the first hint applicable to a
given goal will be applied, as specified in the user-supplied list of
:hints followed by the
default-hints-table. Thanks to Mark
Reitblatt for sending a question that led both to adding this clarification
to the documentation and to adding this warning.
You may now use
set-ld-skip-proofs in place of their versions
ending in ``
p''. Thanks to Jared Davis for suggesting consideration of
such a change. All ``
set-'' utilites now have a version without the
p'' (and most do not have a version with the final ``
Added a "Loop-Stopper" warning when a
rewrite rule is specified
loop-stopper field that contains illegal entries that
will be ignored. Thanks to Jared Davis for recommending such a warning.
Added a substantial documentation topic that provides a beginner's guide to
the use of quantification with
defun-sk in ACL2. Thanks to Sandip Ray
for contributing this guide, to which we have made only very small
modifications. See quantifier-tutorial.
Defun-sk now allows the keyword option
:strengthen t, which
will generate the extra constraint that that is generated for the
defchoose event; see defchoose. Thanks to Dave Greve for
suggesting this feature.
Fixed a soundness bug related to the use of
encapsulate events. An example proof of
nil (before the fix) is in
a comment in
(deflabel note-3-4 ...) in the ACL2 source code. We
therefore no longer allow calls of
that have non-empty signatures.
Fixed a bug related to the definition of a function supporting the
value-triple. Although this bug was very unlikely to affect any
user, it could be carefully exploited to make ACL2 unsound:
(defthm fact (equal (caadr (caddr (value-triple-fn '(foo 3) nil nil))) 'value) ; but it's state-global-let* in the logic :rule-classes nil) (defthm contradiction nil :hints (("Goal" :use fact :in-theory (disable (value-triple-fn)))) :rule-classes nil)
LOCAL definitions of functions or macros are no longer considered
redundant with built-ins when the built-ins have special raw Lisp code,
because ACL2 was unsound without this restriction! A comment about redundant
definitions in source function
chk-acceptable-defuns shows how one could
nil without this new restriction. Note that system utility
redef+ removes this restriction.
Although ACL2 already prohibited the use of certain built-in
program mode functions for
verify-termination and during
macroexpansion, we have computed a much more complete list of functions that
need such restrictions, the value of constant
Modified what is printed when a proof fails, to indicate more clearly which event failed.
Fixed a problem with
dmr in CCL (OpenMCL) that was causing a raw Lisp
break after an interrupt in some cases. Thanks to Gary Byers for a
suggestion leading to this fix.
Fixed bugs in proof-checker code for dealing with free variables in hypotheses.
Upon an abort, the printing of
pstack and gag-mode summary
information for other than GCL was avoided when inside a call of
This has been fixed.
(Windows only) Fixed bugs for ACL2 built on SBCL on Windows, including one
:dir :system from working,
and one that prevented certain compilation. Thanks to Peter Dillinger for
bringing these to our attention and supplying a fix for the second. Thanks
also to Andrew Gacek for bringing
include-book issues to our attention.
Also, fixed writing of file
saved_acl2 at build time so that for Windows,
Unix-style pathnames are used.
Fixed a hard Lisp error that could occur with keywords as
(table :a :a nil :put). Thanks to Dave Greve for bringing this
problem to our attention and providing this example.
Fixed handling of
:OR hints so that proof attempts under an
hint do not abort (reverting to induction on the original input conjecture)
prematurely. Thanks to Robert Krug for pointing out this problem and
pointing to a possible initial fix.
(SBCL and CLISP only) It is now possible to read symbols in the
"COMMON-LISP" package inside the ACL2 command loop (see lp). This
could cause a raw Lisp error in previous versions of ACL2 whose host Common
Lisp was SBCL or CLISP. Thanks to Peter Dillinger for bringing this issue to
Fixed a bug that was preventing certain hints, such as
hints, from being used after the application of an
:or hint. Thanks to
Robert Krug for bringing this bug to our attention.
(Hons version only) Fixed a bug in the interaction of
hons version only) with event processing, specifically in interaction
with failures inside a call of
encapsulate. Thanks to
Jared Davis for bringing this bug to our attention and sending an example. A
simplified example may be found in a comment in source function
table-cltl-cmd, source file
history-management.lisp; search for
cw-gstack so that its
:evisc-tuple is applied to the top
clause, instead of using
(4 5 nil nil) in all cases. If no
:evisc-tuple is supplied then
(term-evisc-tuple t state) is used for
the top clause, as it is already used for the rest of the stack.
Fixed a bug in the interaction of proof-trees with
:otf-flg-override. Thanks to Peter Dillinger for reporting this
bug and sending an example that evokes it.
Fixed bugs in
find-rules-of-rune for the case of rule
elim. Thanks to Robert Krug and Jared Davis for bringing
these related bugs to our attention.
Improved failure messages so that the key checkpoints are printed only once
when there is a proof failure. Formerly, a proof failure would cause the key
checkpoints to be printed for every
superior to the proof attempt.
Fixed a bug in generation of guards for calls of
Thanks to Mark Reitblatt for sending an example showing this bug.
The bug can be in play when you see the message: ``HARD ACL2 ERROR in
MAKE-LAMBDA-APPLICATION: Unexpected unbound vars ("")''. A
distillation of Mark's example that causes this hard error is as follows.
(defun foo (x) (declare (xargs :guard t)) (let ((y x)) (pkg-witness y)))
cond macro now accepts test/value pairs of the form
(T val) in
other than the last position, such as the first such pair in
(cond (t 1) (nil 2) (t 3)). Thanks to Jared Davis for sending this
example and pointing out that ACL2 was sometimes printing goals that have
such a form, and hence cannot be submitted back to ACL2. A few macros
cond in some books under
books/bdd were similarly modified. (A second change will probably not be
noticeable, because it doesn't affect the final result: singleton
clauses now generate a call of
or in a single step of macroexpansion,
if. For example,
(cond (a) (b x) (t y)) now expands to
(OR A (IF B X Y)) instead of
(IF A A (IF B X Y)). See the source
cond-macro for a comment about this change.)
Fixed a bug in the interaction of proof-checker command
including numeric (``diving'') commands, with the
Specifically, if you executed
(add-binop mac fn) with
fn having arity
other than 2, a proof-checker command such as 3 or
(dv 3) at a call
mac could have the wrong effect. We also fixed a bug in diving with
DV into certain
OR calls. Thanks for Mark Reitblatt for
bringing these problems to our attention with helpful examples.
Fixed a couple of bugs that were causing an error, ``HARD ACL2 ERROR in RENEW-NAME/OVERWRITE''. Thanks to Sol Swords for bringing the first of these bugs to our attention.
Fixed a bug that could cause
certify-book to fail in certain cases
where there are
Fixed a bug in
start-proof-tree that could cause Lisp to hang or
produce an error. Thanks to Carl Eastlund for sending an example to bring
this bug to our attention.
Fixed a bug in the proof output, which was failing to report cases where the current goal simplifies to itself or to a set including itself (see specious-simplification).
Fixed a bug in
with-prover-time-limit that was causing a raw Lisp error
for a bad first argument. Thanks to Peter Dillinger for pointing out this
The following was claimed in
note-3-3, but was not fixed until
the present release:
doc/HTML/ now again includes installation
In certain Common Lisp implementations -- CCL (OpenMCL) and LispWorks, at least -- an interrupt could leave you in a break such that quitting the break would not show the usual summary of key checkpoints. This has been fixed.
NEW AND UPDATED BOOKS
books/clause-processors/SULFA/ with a new version from Erik
Reeber; thanks, Erik.
Added new books directory
tools/ from Sol Swords. See
books/tools/Readme.lsp for a summary of what these books provide.
The distributed book
books/misc/file-io.lisp includes a new utility,
write-list!, which is like
write-list except that it calls
open-output-channel! instead of
open-output-channel. Thanks to
Sandip Ray for requesting this utility and assisting with its
record-update macro supplied by Sandip Ray to distributed book
Sandip Ray has contributed books that prove soundness and completeness of
different proof strategies used in sequential program verification.
books/proofstyles/ has three new directories
comprising that contribution:
counterexamples/. The existing
books/proofstyles/ directory has been
moved to its subdirectory
Jared Davis has contributed a profiling utility for ACL2 built on CCL
books/misc/oprof.lisp. Thanks, Jared.
putprop take advantage of
under-the-hood Lisp (hashed) property lists. The new book
books/misc/getprop.lisp contains an example showing how this works.
Added the following new book directories:
books/paco/, which includes a
small ACL2-like prover; and
books/models/jvm/m5, which contains the
definition of one of the more elaborate JVM models, M5, along with other
files including JVM program correctness proofs. See files
these directories, and file
README in the latter.
Added books about sorting in
that directory for documentation.
books/misc/computed-hint-rewrite.lisp to provide an interface
to the rewriter for use in computed hints. Thanks to Jared Davis for
requesting this feature.
Jared Davis has provided a pseudorandom number generator, in
Robert Krug has contributed a new library,
reasoning about arithmetic. He characterizes it as being more powerful than
books/arithmetic-3/, and without its predecessor's
rewriting loops, but significantly slower than its predecessor on some
Incorporated changes from Peter Dillinger to verify guards for functions in
books/ordinals/lexicographic-ordering.lisp (and one in
ordinal-definitions.lisp in that directory).
A new directory,
books/hacking/, contains a library for those who wish to
use trust tags to modify or extend core ACL2 behavior. Thanks to Peter
Dillinger for contributing this library. Obsolete version
books/misc/hacker.lisp has been deleted. Workshop contribution
books/workshops/2007/dillinger-et-al/code/ is still included with the
workshops/ tar file, but should be considered deprecated.
assert!-stobj to return
(value-triple :success) upon success instead
(value-triple nil), following a suggestion from Jared Davis.
emacs/emacs-acl2.el so that the fill column default (for the
right margin) is only set (still to 79) in lisp-mode.
Modified Emacs support in file
emacs/emacs-acl2.el so that names of
events are highlighted just as
defun has been highlighted when it is
called. Search in the above file for
instructions on how to eliminate this change.
The name of the temporary file used by some Emacs utilities defined in file
emacs/emacs-acl2.el has been changed to have extension
.lisp; thus it is now
temp-emacs-file.lsp. Also, `
commands to `clean' books will delete such files (specifically,
books/Makefile-generic has been changed to delete