Major Section: RELEASE-NOTES
pkg-witness, and improved its documentation. (The executable counterpart returned an incorrect default value, and the axiom
pkg-nameto be other than
""in order to avoid the default value of "ACL2".) As fallout, a new built-in
symbol-package-name-of-symbol-is-not-empty-string, now asserts that the
symbol-package-nameof 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.
Pkg-witness bug allowed proof of nil. This shows the delicacy of *1* functions.
nilbefore the fix.
Tracking of forcing is subtle.
defunevents, 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
xargsexcept 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)) 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)))))))
We've previously talked about this one at some length.
pland the proof-checker's
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 attention.
Made nice :pl improvements.
ubu!, which are analogous to
ubt!(respectively) except that they only undo back up to, but not including, the indicated command.
:Ubu and :ubu! can be quite handy.
*acl2-exports*. Thanks to Bob Boyer and Erik Reeber (respectively) for bringing these issues to our attention.
books/misc/transfinite.lisp, which deals with transfinite induction in ACL2. Thanks to Eric Smith for contributing this book.
Illustrates how to do induction proofs by functional instantiation.
books/misc/process-book-readme.lispto the distribution. Thanks to Sandip Ray for pointing out its omission.
Please contribute books! It's pretty simple now; look for link with "How to Contribute" on home page.
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.lspfiles in these directories.
Perhaps Sandip has a word to say about these?
ENSinstead 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-invariantexpression 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.
You'll need to change any theory-invariant expressions to use ENS instead of THEORY.
deftheoryevents. After all, one can define a theory with
deftheorythat 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-invarianterrors 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
defun-sknow has a new optional keyword,
rewrite, that can be used to change the form of the
rewriterule 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
defthmevent underneath a
defun-skin order to make the proof more reliably efficient.
Users have wanted defun-sk to create nicer rewrite rules. This still isn't the default, but at least now it's easy to get this behavior.
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
I could give a demo. This is nice if you have some preliminary stuff that you want to leave around.
), allows users to determine whether or not they are in a
wormhole. Thanks to Peter Dillinger for providing this utility.
Value-tripleno 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.
; The "what could be considered a soundness hole" could be exploited as
; (in-package "ACL2")
; ; Portcullis commands:
; (set-ld-redefinition-action '(:warn! . :overwrite) state)
; (defun foo () t)
; (local (defun foo () nil))
; (defthm foo-prop
; (equal (foo) nil)
; :rule-classes nil))
; |# ; |
; ; NOTE: After the above commands:
; ; ACL2 !>(redefined-names state)
; ; NIL
; ; ACL2 !>
; ; Now execute:
; ; (certify-book "bad" 1)
; (defthm contradiction
; :hints (("Goal" :use foo-prop))
; :rule-classes nil)
; After certifying the book we can do this:
; (include-book "bad")
; (thm nil :hints (("Goal" :use contradiction)))
(in-theory '((:definition natp) (:rewrite doesntexist)))to show how a hard error could occur.
certify-bookwhen the certification world contains inadmissible forms.
defchooseto add two new keyword arguments. There is now a
:dockeyword argument; previously, an optional documentation string (see doc-string) was to be placed just before the body, without a keyword. There is also a
:strengthenargument 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
The new axiom allows the obtaining of a canonical representative.
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.
Note also expander.lisp.
meta-x new-shellprovided by file
emacs/emacs-acl2.elnow puts you in shell-mode, which for example supports directory tracking. Thanks to Jared Davis for suggesting this change.
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
defttagand the following related items.
This is a pretty sweeping change, since it lets you put almost anything into a book, even raw Lisp! I might discuss some of the sub-points just below.
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
programmode. Thanks to Peter Dillinger for proposing
remove-untouchableand suggesting that it and
push-untouchablebe functional in
Raw-mode (see set-raw-mode) no longer disables
set-raw-modeis now disallowed unless there is an active ttag (see defttag). If you want to execute
t)and there is no active ttag, consider executing
Redefinition of system functions is disallowed unless there is an active ttag. However,
(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
prognforms (see embedded-event-form), and is similar to
prognexcept 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,
progn!to define utiliities
with-redef-allowed, which respectively allow raw Lisp evaluation and redefinition to take place within a certifiable book (!).
with-outputis 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.
defstobjin raw Lisp, which caused an error when certifying a book with a redundant
stobjhad 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)
make-eventhave been contributed in directory
print-object$(see io) so that it no longer prints an extra space at the end.
:functional-instancehints from being legal. The corresponding check now only requires that no variable free in the functional substitution is captured by a
lambda) binding. See lemma-instance.
Wow, this had been awaiting a fix for a long time.
mfc-rw+, which is equivalent to
mfc-rwexcept 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
This one is particularly useful for automatically-generated code when you don't want to use set-ignore-ok.
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)
make-eventto 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.
compress2. Thanks to David Rager for bringing this bug to our attention.
mutual-recursionevent 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.
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.
books/deduction/passmore/. Thanks, Grant.
I'm sure Grant would like feedback.
inhibit-outputarguments of routines in the book
books/misc/expander.lisp. Thanks to Qiang Zhang for pointing out the possibility for improvement here.
books/arithmetic-3with 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.
Alex and Robert would probably like feedback.
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
o To avoid conflict with
books/rtl/rel6/arithmetic/, renamed rule
floor-mod/floor-mod.lisp, and renamed
<to compare complex rational constants. Thanks to Robert Krug for helping with the fixes.
assert-event, for checking that forms evaluate to non-
nilvalues. Thanks to Peter Dillinger for suggesting and collaborating on this addition.
Could be useful.