Major Section: RELEASE-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
Fixed subtle soundness bugs related to
meta rules by restricting
evaluators (see defevaluator), as discussed in a new documentation topic:
Fixed a soundness bug that was allowing redefinition from
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
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
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
open-output-channel! is identical as a function to
open-output-channel, except that the new function may be called even
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.
books/defexec/reflexive/reflexive.lisp to illustrate reflexive
ACL2 now generate scripts that invoke the saved image with
(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
ACL2 has a better implementation of
) (hence of
)). 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
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
(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
mod-expt in GCL. Thanks to Warren Hunt, with contributions
from Robert Krug, for providing this book,
Modified macro break-on-error to print of 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.
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
been replaced by
defpun-base. Thanks to Dave Greve for providing a first
version of this update to
books/arithmetic-3/bind-free/top.lisp, has been
arithmetic-3-bind-free-base, to avoid potential name conflicts.
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.
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
hons.lisp. Future versions of ACL2 may fully incorporate this
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
(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
(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.
term-evisc-tuple (see ld-evisc-tuple) is overridden by state
user-term-evisc-tuple in all cases. Formerly, this was only the
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
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;
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
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
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
(OpenMCL and Allegro CL only) Fixed ACL2's redefinitions of raw Lisp
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
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
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
:frame, from inside the proof-checker.
This has been fixed.
Fixed a bug that could cause functions that call system built-ins
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
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
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-checker-commands for the new proof-checker command
clause-processor (or for short,
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.
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,
A new release of the RTL library,
books/rtl/rel7/, replaces the previous
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
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
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).
xargs keywords may now be used in
events. In particular, this is the case for
(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,
(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
Added a new
:msg argument to
assert-event; see assert-event. The
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
#. 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).)
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-fns, can control the enforcement of untouchability.
See remove-untouchable. Thanks to Peter Dillinger for suggesting these
The ``TTAG NOTE'' string was being printed by
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
progn! event setting raw-mode to
t without setting raw-mode back
(progn! (set-raw-mode t) ...)