ACL2 Version 3.0.2 (December, 2006) Notes
NOTE! New users can ignore these release notes, because the
documentation has been updated to reflect all changes that are recorded
Fixed soundness bugs in the handling of primitive function pkg-witness, and improved its documentation. (The executable counterpart
returned an incorrect default value, and the axiom
symbol-package-name-pkg-witness-name needed pkg-name to be other
than "" in order to avoid the default value of "ACL2".) As fallout,
a new built-in :forward-chaining rule,
symbol-package-name-of-symbol-is-not-empty-string, now asserts that the
symbol-package-name of a symbol is never "". Thanks to Mike
Gordon for bringing these soundness bugs to our attention by attempting to
prove translations of ACL2 axioms in HOL4.
Fixed a soundness bug in linear arithmetic, due to incomplete tracking of
forced assumptions while deriving inequalities. Thanks to Robert Krug for
providing a fix and a proof of nil before the fix.
Fixed a soundness bug in the redundancy criterion for defun events,
which has been modified; see redundant-events. This bug is illustrated
below. Thanks to Peter Dillinger and Jared Davis for contributions to an
email thread that led us to discover this bug. The solution is that for a
definition to be redundant with an earlier definition, ACL2 no longer ignores
:measure xargs except when skipping proofs (e.g., during
include-book). However, a new ``measure'', (:? v1 ... vk), is
supported, for specifying a measured subset of the set of formals, i.e., a set
of formals that serves as the set of parameters for some valid measure.
(local (defun foo (x y)
(declare (xargs :measure (acl2-count y)))
(if (and (consp x) (consp y))
(foo (cons x x) (cdr y))
; So the following is redundant -- but it guesses a measure
; of (acl2-count x), which isn't right!
(defun foo (x y)
(if (and (consp x) (consp y))
(foo (cons x x) (cdr y))
; end of encapsulate
; Now we prove a non-theorem by exploiting the bug above,
; erroneously replacing formal y by a constant in the induction
; scheme hinted below. (This should not be allowed, as y should be
; labeled as a measured formal.)
:hints (("Goal" :induct (foo x '(3)))))
; It's easy to get a contradiction by instantiating the
; non-theorem just above.
:hints (("Goal" :use ((:instance bad (x '(7)))))))
Fixed a bug in :pl and the proof-builder's
show-rewrites (sr) command that was causing a Lisp break. For
:pl, also improved the display of unifying substitutions,
modified output to take binding hypotheses (equal var term) into account
properly, and arranged for inclusion of meta rules that modify the
given term. Thanks to Eric Smith for bringing these issues to our
Introduced new utilities for undoing commands, :ubu and
:ubu!, which are analogous to :ubt and :ubt! (respectively) except that they only undo back up to, but not
including, the indicated command.
Fixed a performance bug, pointed out by Eric Smith, that was negating
efforts made for the preceding release to avoid computation for disabled
Added time$ and value-triple to *acl2-exports*. Thanks
to Bob Boyer and Erik Reeber (respectively) for bringing these issues to our
Improved the automatic proclaiming of function types for GCL and OpenMCL,
specifically to use an output format consistent with the Common Lisp spec.
Thanks to Bob Boyer for bringing this issue to our attention.
Added books/misc/transfinite.lisp, which deals with transfinite
induction in ACL2. Thanks to Eric Smith for contributing this book.
Added books/misc/process-book-readme.lisp to the distribution. Thanks
to Sandip Ray for pointing out its omission.
Added contributions books/concurrent-programs/bakery/ and
books/concurrent-programs/german-protocol/. These contributions can be
used as tutorials, especially by new ACL2 users, for learning how to model
concurrent protocols in ACL2 and the steps involved in reasoning about their
correctness. Thanks to Sandip Ray for these contributions. See the
Readme.lsp files in these directories.
Theory invariants may now involve the variable ENS instead of the
variable THEORY. The practical effect of this change is that any
expression of the form (MEMBER-EQUAL rune THEORY) occurring in a theory-invariant expression should be replaced by (ACTIVE-RUNEP rune).
See theory-invariant. Thanks to Eric Smith and Dave Greve for pointing
out an inefficiency in the handling of theory invariants that led to this
change, which can speed up their handling by orders of magnitude on large
examples, and to Eric for testing this change and pointing out problems with
an early implementation of it.
Theory invariants (see theory-invariant) are no longer checked on
theories defined by deftheory events. After all, one can
define a theory with deftheory that is not intended to be used as the
current theory, but rather is intended to be combined with other theories (see theory-functions). Thanks to Eric Smith for bringing
this issue to our attention.
Theory-invariant errors had been reported with very little detail
when warnings were inhibited. This problem has been fixed; thanks to Eric
Smith for bringing it to our attention and providing an example. We have also
improved the handling of redundancy for theory-invariant events.
The macro defun-sk now has a new optional keyword, rewrite,
that can be used to change the form of the :rewrite rule
generated when the quantifier is forall. Thanks to Eric Smith and
Sandip Ray for useful discussions on this topic. We have also slightly
modified the hints for the defthm event underneath a
defun-sk in order to make the proof more reliably efficient.
A new event, reset-prehistory, allows setting of a barrier before
which undoing is illegal. An argument to this macro allows the barrier to be
made permanent; otherwise, it can be removed with :ubt-prehistory. Thanks to Peter Dillinger for useful conversations leading
to the addition of reset-prehistory.
A new query, (wormhole-p state), allows
users to determine whether or not they are in a wormhole. Thanks to
Peter Dillinger for providing this utility.
Value-triple no longer evaluates its form during include-book,
and in raw Lisp its calls trivially macroexpand to nil, without any
consideration of its argument. This change avoids errors and warnings when
stobj names occur in the argument.
We fixed what could be considered a soundness hole that could occur by
exploiting redefinition in a particular way. Thanks to Peter Dillinger for
raising a question that led to discovery of this hole.
A bug has been fixed in handling of illegal theory expressions.
Thanks to Eric Smith, who reported this problem and provided the example
(in-theory '((:definition natp) (:rewrite doesntexist))) to show how a
hard error could occur.
Improved error reporting by certify-book when the certification
world contains inadmissible forms.
Modified defchoose to add two new keyword arguments. There is now
a :doc keyword argument; previously, an optional documentation string
(see doc-string) was to be placed just before the body, without a
keyword. There is also a :strengthen argument that strengthens the axiom
added, which allows for the definition of ``fixing'' functions for equivalence
relations that choose canonical representatives of equivalence classes. See
defchoose. Thanks for Dave Greve for useful discussions that led us to
this :strengthen enhancement.
Added books/misc/bash.lisp, which provides utilities for simplifying a
goal into a list of subgoals (as documented at the top of that file). Thanks
to Dave Greve for requesting this utility and suggesting refinements to its
functionality, which have been incorporated.
(For Emacs users only) The command meta-x new-shell provided by file
emacs/emacs-acl2.el now puts you in shell-mode, which for example
supports directory tracking. Thanks to Jared Davis for suggesting this
Fixed some mishandling of stobjs by make-event
Introduced a new event, defttag, that introduces a ``trust tag''
(``ttag'') allowing for extensions of ACL2 and for the use of generally unsafe
ACL2 constructs. Thanks to Peter Dillinger, Sandip Ray, and Erik Reeber for
useful discussions on defttag and the following related items.
A new event, remove-untouchable, can be used to give users access
to system functions and data structures. We also fixed a bug in push-untouchable; and, it no longer is a no-op in :program mode.
Thanks to Peter Dillinger for proposing remove-untouchable and
suggesting that it and push-untouchable be functional in :program mode.
Raw-mode (see set-raw-mode) no longer disables certify-book.
However, set-raw-mode is now disallowed unless there is an active ttag
(see defttag). If you want to execute (set-raw-mode
t) and there is no active ttag, consider executing (set-raw-mode-on!) instead.
Redefinition of system functions is disallowed unless there is an active
ttag. However, redef! now introduces (defttag :redef!) in order
to allow redefinition of system functions.
A new event, progn!, is a legal embedded event form that can go in
books and both encapsulate and progn forms (see embedded-event-form), and is similar to progn except that it allows
arbitrary forms. Thus, a progn! form is potentially dangerous and can
only be evaluated if there is an active ttag.
See ttags-seen for information about how to find the ttags known in
the current ACL2 world, and for related caveats.
A new book created with Peter Dillinger, books/misc/hacker.lisp (added
after Version_3.3: now books/hacking/hacker.lisp), uses progn! to
define utilities with-raw-mode and with-redef-allowed, which
respectively allow raw Lisp evaluation and redefinition to take place within a
certifiable book (!).
Macro with-output is no longer allowed in function bodies because
it does not have (and has never had) any effect in raw Lisp. See with-output for a workaround.
Fixed a bug in redundancy of defstobj in raw Lisp, which caused an
error when certifying a book with a redundant defstobj event whose
stobj had already been modified. Here is an example:
(defstobj st fld)
(update-fld 3 st)
(certify-book "foo" 1) ; where foo.lisp contains (defstobj st fld)
New books illustrating make-event have been contributed in
directory books/make-event/: dotimes.lisp (David Rager),
stobj-test.lisp, and logical-tangent.lisp (Peter Dillinger).
Modified print-object$ (see io) so that it no longer prints an
extra space at the end.
Replaced the ``draconian restriction to avoid capture'' that had prevented
some :functional-instance hints from being legal. The
corresponding check now only requires that no variable free in the functional
substitution is captured by a let or mv-let (or lambda) binding. See lemma-instance.
Added new extended metafunction, mfc-rw+, which is equivalent to
mfc-rw except that it takes an alist argument, which may be useful for
efficiency. See extended-metafunctions. Thanks to Robert Krug for
suggesting this more efficient variant of mfc-rw.
Added support for the ignorable declare form.
We now cause an error on a call of open-input-channel (see io)
with an argument string whose first character is the | character. Thanks
to Bob Boyer for providing an example (several months ago) showing the danger
of such calls, namely that the following command would log you out and kill
all of your processes when running on top of GCL in Linux:
(open-input-channel "|kill -9 -1" :object state)
Restricted the use of make-event to contexts in which it can be
tracked properly, under legal events (see embedded-event-form).
Thanks to Peter Dillinger for bringing an example to our attention that led to
Fixed a bug that was avoiding guard-checking for the functions
compress1 and compress2. Thanks to David Rager for bringing
this bug to our attention.
Added an error message when a defun or mutual-recursion
event fails, to clarify whether failure is for the measure conjecture
or for the guard conjecture. Thanks to David Rager for requesting
clarification for such failures.
Fixed a bug in reporting of guard violations (hard Lisp error) when
certain macros (for example, cond) are used in the guard.
Thanks to Jared Davis for bringing this problem to our attention and providing
assistance with the solution, in particular by providing a helpful
Grant Passmore has contributed a resolution/paramodulation prover written
in ACL2, in directory books/deduction/passmore/. Thanks, Grant.
Improved the error message when illegal theories are encountered.
Improved the suppression of output for inhibit-output arguments of
routines in the book books/misc/expander.lisp. Thanks to Qiang Zhang for
pointing out the possibility for improvement here.
Added a new directory books/arithmetic-3/extra/ that extends
books/arithmetic-3 with additional rules, contributed by Alex Spiridonov
with guidance from Robert Krug. WARNING: This directory is under development.
It may undergo large changes in future releases, so please consider it
experimental and subject to change. Feedback is welcomed.
As part of the work mentioned just above, Robert Krug and Alex Spiridonov
contributed improvements to books/arithmetic-3/:
o A new rule |(* (/ x) (/ (expt x n)))| in
bind-free/collect.lisp, which is important for reducing collect-*
expressions though it slowed down one proof (see comment above this rule in
o Slight improvements of rules integerp-mod and rationalp-mod in
o To avoid conflict with books/rtl/rel6/arithmetic/, renamed rule
mod-minus to mod-neg in floor-mod/floor-mod.lisp, and renamed
(GCL on Windows only) Made a low-level change to avoid multiplying stacks
for GCL on Windows, since GCL 2.6.6 broke while doing this.
Fixed bugs in linear arithmetic (rarely evidenced, it seems) involving
using < to compare complex rational constants. Thanks to Robert Krug for
helping with the fixes.
Added a new event, assert-event, for checking that forms evaluate
to non-nil values. Thanks to Peter Dillinger for suggesting and
collaborating on this addition.