Changes in Version 3.0 since Version 2.9.4
Fixed a bug in cw-gstack that was causing a hard error when
attempting to report on a forced assumption. Thanks to Jared Davis for
pointing this out and sending an example that helped us to determine a
Added set-backchain-limit to the set of legal events that
can be placed in encapsulate forms and books. Thanks to John
Cowles for bringing this issue to our attention.
Fixed a bug that broke wet. Thanks to David Rager for bringing this
bug to our attention.
Guard verification now evaluates ground subexpressions (those with no free
variables) when computing the guard conjecture for the body of a function.
Thanks to Jared Davis for useful conversations leading to this change. See
verify-guards, in particular its ``Note on computation of guard
conjectures and evaluation'' near the end of that topic, for more details.
Added a warning when a theory-invariant is redefined. Thanks to
Jared Davis for suggesting a warning in this case and providing an informative
example. Also, theory-invariants are now maintained more completely,
as they are checked at the end of every event except for events executed on
behalf of an include-book or the second pass of an encapsulate.
Fixed the handling of runic designators to match their specification (see
theories), so that disabling the name of a defthm event disables all rules generated for that event.
(For those who do numerous builds using feature :acl2-mv-as-values,
currently only OpenMCL and multi-threaded SBCL by default:) You can speed up
builds by adding the following parameter to `make', under conditions described
in GNUmakefile: USE_ACL2_PROCLAIMS=:REUSE.
Arranged that traced functions (see trace$) are automatically
untraced when events are undone (for example see ubt), at least for
most underlying Common Lisp implementations.
The macro defun-sk now creates non-executable functions, which
allows stobjs to be used where they had previously been prohibited.
More generally, the user now has control over declare forms to be used
by the underlying defun'd function; see defun-sk. Thanks to
Sandip Ray for pointing out the need for such a modification.
:Definition rules are now treated, at least by default, as
truly first-class definitions. In particular, :expand hints use
the latest :definition rule by default. You may specify
:install-body nil to get the previous behavior of :definition rules;
See definition, and you may choose a previously-installed
:definition rule to provide the current body; see set-body. Also
see rule-classes for details of the :install-body field, and see
hints to see a new :with directive for controlling expansion. The
:with directive for :expand hints can even direct the use of a
:rewrite rule for expansion! Thanks to various people, including
Sandip Ray and Rob Sumners, for discussions on the issue of the applicability
of :definition rules for :expand hints.
Constraints for functional instantiation now use the original
definition rather than a simplified (``normalized'') version of it.
Fixed a bug that caused the prompt to stay the same when guard-checking is
off (see set-guard-checking) and raw-mode is changed (see set-raw-mode).
Lemma names in directory books/ordinals have been changed by replacing
/\ with & and replacing \/ with V. We made this change
because backslash is an escape character and hence disappears unless it is
Fixed proof-tree output so that failed non-proof events do not cause
the proof-tree to be re-printed. Thus for example, if you have already
advanced the checkpoint marker, it will not be reset by subsequent failed
non-proof events. Thanks to Pete Manolios and Peter Dillinger for bringing
this bug to our attention.
Fixed a bug that was preventing the printing of stobj fields as
constants instead of numbers in certain cases. (Note that this bug only
affected printing, not soundness.) Thanks to Eric Smith for bringing this
problem to our attention and providing the following example (which now works
(defstobj st fld1 fld2)
(in-theory (disable update-nth))
(defund run (st)
(declare (xargs :stobjs (st))) ;adding this didn't seem to help..
;works great; *fld1* prints as *fld1*
(thm (equal (update-nth *fld1* 'abc st)
(car (cons x y))))
;*fld1* gets printed as 0, presumably because the call to run intervenes.
(thm (equal (update-nth *fld1* 'abc (run st))
(car (cons x y))))
The macro progn now allows the use of macros defined within its
bodies even when at the event level, as illustrated by the following
(progn (defmacro my-defun (&rest args)
(my-defun g (x) x))
Thanks to Anna Slobodova for bringing this issue to our attention. A
related change is that all arguments of progn must now be embedded
event forms (see embedded-event-form), so use er-progn instead
if this is not the case.
The change to progn mentioned above also fixes a bug in handling
local events inside a progn that is inside an encapsulate or in a book. For example, the following form formerly caused an
(defun foo (x) x)
(progn (local (defun bar (x) x))
(defun abc (x) x)))
We fixed two bugs in :puff and :puff*. The
first, brought to our attention by Eric Smith (who we thank), caused a cryptic
error message when puffing a command with no subsidiary stored events; try,
for example, (encapsulate () (value-triple 3)). The second was due to a
failure to restore the ACL2-defaults-table. Suppose for example that
we have certified the book foo.lisp, which contains (program) followed by some definitions and/or theorems. Now suppose we
start ACL2 and execute the following.
(equal x x)
If we now execute :puff 1, ACL2 will roll back the world
to before the include-book; then ``puff'' the include-book, which will
leave us in :program mode; and finally skip re-execution of the
defthm because such events are skipped in :program
mode. The fix is to re-install the ACL2-defaults-table immediately
after the include-book to its pre-include-book value.
A new event, make-event, provides something like macros that take
state. For example, one can use it to put tests into certified books, do
proof search, and generate new function names. Many examples appear in
directory books/make-event/. See make-event. Thanks to Bob Boyer
and Jared Davis for useful feedback and to Warren Hunt, David Rager, and
Sandip Ray for helpful discussions leading to some of the examples in
In support of make-event, which is described in the preceding
paragraph, certify-book has a new keyword argument, :save-expansion,
that controls whether the result of expanding make-event forms is
written out to a file. See certify-book; and for a discussion of book
expansion files, see make-event.
We fixed a soundness bug that did not correctly detect local
events. For example, the following event was admitted.
(local (progn (program))) ; or, (local (with-output :off summary (program)))
(defun foo (x)
(declare (xargs :measure (acl2-count x)))
(1+ (foo x)))))
:hints (("Goal" :use foo))
A new value for guard checking, :none, is now allowed. If you
execute :set-guard-checking :none, then no guard checking
will take place (but raw Lisp code will not be executed in this case). As a
result, you should never see a guard violation, even for calls of
:program mode functions. We thank Pete Manolios, who has long
wanted this feature, and also Peter Dillinger, for asking for it. New
documentation explains the interaction between the defun-mode and the
value supplied to :set-guard-checking. See guard-evaluation-table, see guard-evaluation-examples-script, and see
In the course of adding the guard-checking value :none
described in the paragraph above, we eliminated an optimization that
eliminated guard checking for some recursive calls of :logic mode
mutually-recursive functions that have not had their guards verified. But we
doubt that this change will be noticed by any users!)
The ACL2 hyper-card has been enhanced, thanks to David Rager, with a
listing of ``Useful EMACS Commands'' to match comments in
Users contributed books following the Readme.lsp methodology:
data-structures/memories and unicode (Jared Davis), proofstyles
(Sandip Ray and J Moore).
Made some improvements to books/Makefile-generic (a file discussed
elsewhere; see books-certification-classic). In particular, improved
handling of .acl2 files for dependencies target.
(Only OpenMCL and, with feature :acl2-mv-as-values, GCL) Fixed a bug
that was causing proclaiming to fail when definitions are submitted
The default stack size has been increased for several lisps.
(Very technical) A restriction has been weakened on the use of local stobjs under a call of an ACL2 evaluator (trans-eval or
simple-translate-and-eval). Now, the error can only take place for
stobj names that occur in the term being evaluated. Thanks to Erik
Reeber for bringing this issue to our attention.
The notion of ``ancestor'' has been changed slightly. This notion is used
by extended metafunctions and break-rewrite (see extended-metafunctions and see brr@), and also with backchain limits
(see backchain-limit and see set-backchain-limit). Basically,
each time a hypothesis is encountered during application of a rewrite
rule, that hypothesis is pushed (after instantiating and negating) onto the
current list of ancestors before it is rewritten. However, hypotheses of the
form (equal var term), where var is free (see free-variables), had not been included in the ancestors (similarly for
(equiv var (double-rewrite term)) where equiv is a known equivalence relation). Now such ``binding hypotheses'' are included in a
special way in ancestors data structures. In particular, (null
(mfc-ancestors mfc)) will now be true if and only if the term being
rewritten is part of the current goal as opposed to a hypothesis from a rule
encountered during backchaining, even if that hypothesis is a binding
hypothesis. Thanks to Dave Greve for bringing this issue to our
Termination and induction analysis now continue through both arguments of
prog2$, not just the second. (Normally, the gathering up of if tests stops at function calls; but it continued through the second
argument of prog2$, and now it will continue through both arguments.)
Thanks to Sol Swords for discussion leading to this change.
The ACL2 distribution is now kept on the http server rather than the ftp
server (but the home page has not been moved). Thanks to Robert Krug for
letting us know that some ACL2 users have found it inconvenient to fetch ACL2
The file books/README.html has been renamed to books/Readme.html,
since some browsers don't show the former in the directory listing.