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 here.
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
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
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
(encapsulate () (local (defun foo (x y) (declare (xargs :measure (acl2-count y))) (if (and (consp x) (consp y)) (foo (cons x x) (cdr y)) 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)) 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.) (defthm bad (atom x) :rule-classes nil :hints (("Goal" :induct (foo x '(3))))) ; It's easy to get a contradiction by instantiating the ; non-theorem just above. (defthm contradiction nil :rule-classes nil :hints (("Goal" :use ((:instance bad (x '(7)))))))
Fixed a bug in
Introduced new utilities for undoing commands,
Fixed a performance bug, pointed out by Eric Smith, that was negating efforts made for the preceding release to avoid computation for disabled warnings.
Added time$ and
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.
Theory invariants may now involve the variable
Theory invariants (see theory-invariant) are no longer checked on
theories defined by deftheory events. After all, one can
define a theory with
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,
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
A new query,
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
Improved error reporting by certify-book when the certification world contains inadmissible forms.
Modified defchoose to add two new keyword arguments. There is now
(For Emacs users only) The command
Fixed some mishandling of stobjs by make-event expansion.
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
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-modeand 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
Replaced the ``draconian restriction to avoid capture'' that had prevented
Added new extended metafunction,
Added support for the
We now cause an error on a call of
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 this fix.
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 example.
Grant Passmore has contributed a resolution/paramodulation prover written
in ACL2, in directory
Improved the error message when illegal theories are encountered.
Improved the suppression of output for
Added a new directory
As part of the work mentioned just above, Robert Krug and Alex Spiridonov
contributed improvements to
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 bind-free/collect.lisp).
o Slight improvements of rules
integerp-modand rationalp-modin floor-mod/floor-mod.lisp.
o To avoid conflict with
books/rtl/rel6/arithmetic/, renamed rule mod-minusto mod-negin floor-mod/floor-mod.lisp, and renamed integerp-+-reduce-leading-constantto integerp-+-reduce-leading-rational-constantin bind-free/integerp.lisp.
(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
Added a new event, assert-event, for checking that forms evaluate