Note-3-2
ACL2 Version 3.2 (April, 2007) Notes
NOTE! New users can ignore these release notes, because the documentation has been updated to reflect all changes that are recorded
here.
Before this release, a raw Lisp error could put the ACL2 user into the
debugger of the host Common Lisp. Now, such cases will generally put the user
back at the top-level loop after an informative message. For details, see
set-debugger-enable; also see break$.
Fixed a soundness bug that was allowing unknown packages to sneak into a
book and wreak havoc. Thanks to Peter Dillinger for sending an interesting
example that led us to an exploration resulting in finding this bug. (A
comment in the source code for note-3-2 shows such an example.) That
example led us to fix a couple of other bugs related to packages. See hidden-death-package if you are generally interested in such issues, and for
associated examples, see comments in note-3-2 in the ACL2 source
code.
Fixed subtle soundness bugs related to :meta rules by
restricting evaluators (see defevaluator), as discussed in a new
documentation topic: see evaluator-restrictions.
Fixed a soundness bug that was allowing redefinition from :logic to :program mode. This prohibition had been in ACL2 for
awhile but was accidentally removed in the preceding version.
Fixed a soundness bug related to trace$. Thanks to Peter Dillinger
for bringing it to our attention and for useful discussions, and providing a
proof of nil, the essence of which is illustrated as follows:
(value-triple (trace$ (bar :entry (defun foo () 17))))
Thus, trace$ could be used to cause destructive raw Lisp behavior.
Now, trace$ fails unless it is either given a list of symbols or else
there is an active trust tag (see defttag); otherwise, consider using
trace! instead.
Closed a loophole that could be viewed as compromising soundness. It was
possible to write files during book certification by exploiting make-event expansion, but that is no longer the case by default. A new
function open-output-channel! is identical as a function to
open-output-channel, except that the new function may be called even
during make-event expansion and clause-processor hints,
but requires that there is an active trust tag (see defttag). Thanks
to Peter Dillinger for producing a convincing example (forging a certificate during book certification; see open-output-channel!) and
to him, Sandip Ray, and Jared Davis for useful discussions on the topic.
Added book books/defexec/reflexive/reflexive.lisp to illustrate
reflexive functions.
ACL2 now generates scripts that invoke the saved image with exec.
(Previously this was only done for GCL and CLISP.) The benefit of this change
can be to avoid the lingering of ACL2 processes after enclosing processes have
exited. Thanks to Peter Dillinger for pointing out this issue.
ACL2 has a better implementation of (good-bye) (hence of
synonyms (quit) and (exit)). As a result,
you should now be able to exit ACL2 and Lisp from within the ACL2
read-eval-print loop with any of the above; formerly, this was not supported
for some Lisp implementations, and was slow in OpenMCL. Thanks to SBCL
developer Harald Hanche-Olsen for useful advice.
Fixed a bug in raw-mode (see set-raw-mode) that was causing hard
errors when evaluating calls of er-progn, or of macros expanding to
such calls.
Fixed a few Makefile dependencies, necessary only for parallel `make'.
A new book, misc/defpun-exec-domain-example.lisp, provides an example
showing how partial functions which return a unique value for arguments in a
specified domain can be efficiently executed with ACL2. Execution is achieved
using the mbe construct. Thanks to Sandip Ray for providing this
example.
Existing function mod-expt computes (mod (expt base exp) mod)
with great efficiency in GCL, but not in other Lisps. Now, the book
arithmetic-3/floor-mod/mod-expt-fast.lisp defines a function
mod-expt-fast that should provide significantly improved performance for
such expressions in other Lisps as well, though still probably not as fast as
when using mod-expt in GCL. Thanks to Warren Hunt, with contributions
from Robert Krug, for providing this book,
Modified macro break-on-error to print an error message before
entering a break, and to cause a hard error if the underlying Lisp cannot
handle it (formerly, a raw Lisp break would occur). Thanks to Bob Boyer for
bringing these issues to our attention.
The book books/misc/defpun.lisp, as well as other books related to the
defpun macro, has been modified to avoid namespace collisions by
prefixing function symbol names with "DEFPUN-"; for example base
has been replaced by defpun-base. Thanks to Dave Greve for providing a
first version of this update to defpun.lisp.
A theory, base, in books/arithmetic-3/bind-free/top.lisp, has
been renamed arithmetic-3-bind-free-base, to avoid potential name
conflicts.
Fixed books/arithmetic-3/bind-free/banner.lisp to print (as before) a
message about how to turn on non-linear arithmetic, by modifying the call of
value-triple to use :on-skip-proofs t. Thanks to Robert Krug for
bringing this issue to our attention.
Modified books/Makefile-subdirs and books/Makefile-psubdirs so
that they can be used with books/Makefile-generic. Thus, one can set
things up so that `make' can be used to certify books both in the current
directory and subdirectories, for example as follows.
ACL2 = ../../saved_acl2
arith-top: top all
all: top
DIRS = pass1 bind-free floor-mod
include ../Makefile-subdirs
include ../Makefile-generic
top.cert: top.lisp
top.cert: bind-free/top.cert
top.cert: floor-mod/floor-mod.cert
top.cert: floor-mod/mod-expt-fast.cert
An experimental extension of ACL2 is under development by Bob Boyer and
Warren Hunt to support function memoization, hash conses, and an applicative
version of hash tables. The default build of ACL2 does not include this
extension, other than simple logic definitions of functions in new source file
hons.lisp. Future versions of ACL2 may fully incorporate this
experimental extension.
The defevaluator event macro has been modified primarily by adding
a new constraint as follows, where evl is the evaluator. The idea is
that for the evaluation of a function call, one may replace each argument by
the quotation of its evaluation and then also replace the alist environment
with nil.
(DEFTHMD UNHIDE-evl-CONSTRAINT-0
(IMPLIES (AND (CONSP X)
(SYNTAXP (NOT (EQUAL A ''NIL)))
(NOT (EQUAL (CAR X) 'QUOTE)))
(EQUAL (evl X A)
(evl (CONS (CAR X)
(KWOTE-LST (UNHIDE-evl-LIST (CDR X) A)))
NIL))))
In order to support this change, there is another change: an evaluator maps
nil to nil (note (AND X (CDR (ASSOC-EQ X A))) in place of
(CDR (ASSOC-EQ X A)) below).
(DEFTHM UNHIDE-evl-CONSTRAINT-1
(IMPLIES (SYMBOLP X)
(EQUAL (UNHIDE-evl X A)
(AND X (CDR (ASSOC-EQ X A))))))
With the new defevaluator, Dave Greve has been able to do a proof
about beta reduction that seemed impossible before (see
books/misc/beta-reduce.lisp). Thanks to Dave for suggesting an initial
version of this change.
Explicit compilation is now avoided for OpenMCL, resulting in fewer files
to manage (no more files resulting from compilation) and, according to some
tests, slightly faster run times. See compilation. Thanks to Bob
Boyer and Warren Hunt for suggesting this possibility.
Now, the term-evisc-tuple (see ld-evisc-tuple) is overridden by
state global user-term-evisc-tuple in all cases. Formerly, this was only
the case when term-evisc-tuple was called with non-nil first
argument.
Symbols with the dot (.) character are generally no longer printed
with vertical bars. For example, before this change:
ACL2 !>'ab.c
|AB.C|
ACL2 !>
After this change:
ACL2 !>'ab.c
AB.C
ACL2 !>
Thanks to Jared Davis for suggesting this improvement.
Fixed bugs in guard verification for theorems. The following examples
illustrate these bugs. If either theorem's body is executed in raw Lisp there
is likely to be a hard Lisp error, even though verify-guards was
supposed to ensure against that behavior.
; Example: Verify-guards failed to check that all functions in the theorem
; had already been guard-verified.
(defun my-car (x) (car x))
(defthm my-car-compute-example (equal (my-car 3) (my-car 3)))
(verify-guards my-car-compute-example)
; Example: Verify guards of a theorem whose body uses state improperly.
(defthm bad-state-handler
(if (state-p state)
(equal (car state) (car state))
t)
:rule-classes nil)
(verify-guards bad-state-handler)
See gcl for an example, developed with Warren Hunt and Serita
Nelesen, that shows how to get fast fixnum (small integer) arithmetic
operations in GCL.
Fixnum declarations are now realized as (signed-byte 30) and
(unsigned-byte 29) instead of what was generally (signed-byte 29)
and (unsigned-byte 28). MCL users may thus find better performance if
they switch to OpenMCL. Note that some definitions have changed
correspondingly; for example, zpf now declares its argument to
be of type (unsigned-byte 29) instead of (unsigned-byte 28). A few
books may thus need to be adjusted; for example, changes were made to
books in books/data-structures/memories/.
ACL2's rewriter now avoids removing certain true hypotheses and false
conclusions. When a hypothesis rewrites to true or a conclusion rewrites to
false, ACL2 formerly removed that hypothesis or conclusion. Now, it only does
such removal when the hypothesis or conclusion is either a call of equal or an equivalence relation (see equivalence), or else is
sufficiently trivial (roughly, either redundant with another hypothesis or
conclusion or else trivially true without considering the rest of the goal).
A specific example may be found in source file simplify.lisp; search for
``; But we need to do even more work''. Thanks to Robert Krug for providing
the idea for this improvement and its initial implementation. As is common
with heuristic changes, you may find it necessary on occasion to rename some
subgoals in your hints. And in this case, you might also find it
necessary on rare occasions to add :do-not '(generalize) hints.
A new function, mfc-relieve-hyp, allows (for example) for more
powerful bind-free hypotheses, by providing an interface to the
rewriter's routine for relieving hypotheses. See extended-metafunctions. Thanks to Robert Krug for providing the idea for
this feature and its initial implementation.
Two improvements have been made to non-linear arithmetic (see non-linear-arithmetic). One allows for deducing strict inequality (<)
for the result of certain polynomial multiplications, where previously only
non-strict inequality (<=) was deduced. A second allows the use of the
product of two polynomials when at least one of them is known to be rational.
We had previously restricted the use of the product to the case where both
were known to be rational. Thanks to Robert Krug for these improvements.
(OpenMCL and Allegro CL only) Fixed ACL2's redefinitions of raw Lisp
trace and untrace in OpenMCL and Allegro CL so that when given no
arguments, they return the list of traced functions. For trace, this is
an ANSI spec requirement. Note that trace$ and untrace$
continue to return nil in the ACL2 loop.
Fixed a bug that was allowing the symbol &whole to appear in other
than the first argument position for a defmacro event, in violation of
the Common Lisp spec (and leading to potentially surprising behavior). Thanks
to Peter Dillinger for bringing this bug to our attention.
It had been illegal to use make-event under some calls of ld. This has been fixed. Thanks to Jared Davis for bringing this issue to
our attention with a simple example, in essence:
(ld '((defmacro my-defun (&rest args) `(make-event '(defun ,@args)))
(my-defun f (x) x)))
ACL2 no longer prohibits certain make-event forms when including
uncertified books. Thanks to Peter Dillinger for first bringing this
issue to our attention.
Hard errors arose when using break-rewrite stack display commands,
in particular :path and :frame, from inside the proof-builder. This has been fixed.
Fixed a bug that could cause functions that call system built-ins
f-put-global, f-get-global, or f-boundp-global to cause a raw
Lisp error even when proving theorems. Thanks to Peter Dillinger, for
reporting such a failure for the form (thm (w '(1 2 3))).
Renamed the formal parameters of function set-equal in distributed
book books/arithmetic-3/bind-free/normalize.lisp so that more distributed
books can be included together in the same session. In particular books
books/data-structures/set-theory and
books/arithmetic-3/extra/top-ext can now be included together. Thanks to
Carl Eastlund for bringing this problem to our attention and to Robert Krug
for suggesting the formals renaming as a fix.
Metafunctions must now be executable. See meta.
New utilities allow for user-defined simplifiers at the goal level, both
verified and unverified (``trusted''), where the latter can even be defined by
programs outside ACL2. See clause-processor, which points to a new
directory books/clause-processors/ that contains examples of these new
utilities, including for example a system (``SULFA'') contributed by Erik
Reeber that implements a decision procedure (thanks, Erik). Also see proof-builder-commands for the new proof-builder command
clause-processor (or for short, cl-proc).
The rewriter has been tweaked to run faster in some cases involving very
large terms. Thanks to Eric Smith and Jared Davis for providing a helpful
example that helped us locate the source of this inefficiency.
Added books/make-event/defspec.lisp. This book shows how one can
mimic certain limited forms of higher-order statements in ACL2 by use of
macros, make-event, and table events. Thanks to Sandip Ray
for his contribution.
A new release of the RTL library, books/rtl/rel7/, replaces the
previous version, books/rtl/rel6/. Thanks to Hanbing Liu and David
Russinoff for providing this new version.
We thank David Russinoff for providing a proof of the law of quadratic
reciprocity. See books/quadratic-reciprocity/Readme.lsp.
Eliminated a slow array warning (see slow-array-warning) that could
occur when exiting a wormhole after executing an in-theory
event in that wormhole. Thanks to Dave Greve for bringing this problem to our
attention.
A new accessor, (mfc-rdepth mfc), provides a new field, the remaining
rewrite stack depth, which has been added to metafunction context structures;
see extended-metafunctions. Thanks to Eric Smith for suggesting this
addition.
The algorithms were modified for collecting up rule names and other
information used in proofs, into so-called ``tag-trees''. Tag-trees are now
free of duplicate objects, and this change can dramatically speed up some
proofs that involve many different rules. Thanks to Eric Smith for doing some
profiling that brought this issue to our attention, and for reporting that
this change reduced proof time on an example by about 47% (from 3681.46
reported seconds down to 1954.69).
All legal xargs keywords may now be used in verify-termination
events. In particular, this is the case for :normalize.
(SBCL and CMUCL only) Fixed a problem with stobj array resizing functions
that was causing a hard error in ACL2 images built on SBCL or CMUCL.
A new table, evisc-table, allows you to introduce print
abbreviations, for example for large constants. Moreover, a new reader macro
— #, — makes it convenient to reference constants even inside
a quote. See evisc-table. Thanks to Bob Boyer and Warren Hunt for
useful discussions leading to this feature.
The macros in books/misc/expander.lisp now have a new keyword
argument, :simplify-hyps-p. The default behavior is as before, but now
case splitting from hypothesis simplification can be avoided. For details,
evaluate (include-book "misc/expander" :dir :system) and then :doc!
defthm? and :doc! symsym. Thanks to Daron Vroon for sending a question
that prompted this additional functionality.
ACL2 failed to apply :restrict hints to rules of class
:definition, except for the simplest sorts (see simple).
This has been fixed. Thanks to Jared Davis for pointing out this bug by
sending a small example.
Added a new :msg argument to assert-event; see assert-event. The implementation of value-triple has been modified to
support this change.
Fixed a bug in macro io? that now allows the commentp argument to
be t. This provides a way other than cw to print without modifying
state, for example as follows. (Warning: Certain errors may leave you in a
wormhole, in which case use :a! to abort.)
ACL2 !>(prog2$ (io? event t state
()
(fms "Howdy~%" nil *standard-co* state nil))
(+ 3 4))
Howdy
7
ACL2 !>:set-inhibit-output-lst (proof-tree event)
(PROOF-TREE EVENT)
ACL2 !>(prog2$ (io? event t state
()
(fms "Howdy~%" nil *standard-co* state nil))
(+ 3 4))
7
ACL2 !>
ACL2 now disallows calls of progn! inside function bodies, just as
it already disallowed such calls of progn, since in both cases the
Common Lisp meaning differs from the ACL2 meaning.
Redefinition of system functions now always requires an active trust tag
(see defttag). This restriction was intended before, but there was a
hole that allowed a second redefinition without an active trust tag. Thanks
to Peter Dillinger for pointing out this bug.
Verify-termination has been disabled for a few more built-in
functions that are in :program mode. (If you are curious about
which ones they are, evaluate (f-get-global 'built-in-program-mode-fns
state).) [Note added for Version_3.4: This state global has been changed to
'program-fns-with-raw-code.] Moreover, such functions now will execute only
their raw Lisp code, so for example they cannot be called during
macroexpansion. Thanks to Peter Dillinger and Sandip Ray for useful
discussions on details of the implementation of this restriction.
New untouchable state global variables, temp-touchable-vars and
temp-touchable-fns, can control the enforcement of untouchability. See
remove-untouchable. Thanks to Peter Dillinger for suggesting these
features.
The ``TTAG NOTE'' string was being printed by encapsulate events
whenever an active trust tag was already in effect (see defttag), even
if the encapsulate event contained no defttag event. This has been
fixed. Thanks to Peter Dillinger for a query leading to this fix.
Fixed a bug in progn! that could leave the user in raw-mode (see
set-raw-mode). This could occur when certifying a book with a
compile-flg value of t (see certify-book), when that book
contained a progn! event setting raw-mode to t without setting
raw-mode back to nil:
(progn! (set-raw-mode t) ...)
