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.
Below we roughly organize the changes since Version 3.6.1 into the following categories of changes: existing features, new features, heuristic improvements, bug fixes, distributed books, Emacs support, and experimental hons-and-memoization version. Each change is described in just one category, though of course many changes could be placed in more than one category. Also see note-3-6-1 for other changes since Version 3.6.
CHANGES TO EXISTING FEATURES
The ACL2 tutorial has, we think, been considerably improved. See acl2-tutorial.
mbe macro and
must-be-equal function were
disallowed in any definition within an encapsulate having a non-empty
signature. Now, these are allowed provided the definition has been declared
to be non-executable (see defun-nx). As a result,
events may now include
must-be-equal among the function symbols
known by the evaluator; this had not previously been allowed. Thanks to Sol
Swords for discussions leading to this relaxation for
Princ$ now prints strings more efficiently. Thanks to Jared Davis for
suggesting the improvements to
The use of
:non-executable t no longer requires
the absence of
state or declared
stobjs among the formal
parameters of a function definition. As before, the use of
:non-executable t turns off single-threadedness checking for the body,
and also as before, attempts to execute the function will fail. Thanks to
Sol Swords for requesting this relaxation (for automatic generation of
so-called ``flag functions'' for definitions using
The documentation has been improved for explaining to advanced users the
details of the ACL2 hint mechanism; see hints-and-the-waterfall, and see the
nonlinearp-default-hint in distributed book
books/hints/basic-tests.lisp. Thanks to Robert Krug for useful
discussions, in particular suggesting the above example as one to be
explained with the documentation.
time$ macro has been enhanced to allow user control of the timing
message that is printed, and of when it is printed. See time$. Thanks to
Jared Davis for providing the essential design, helpful documentation
(largely incorporated), and an initial implementation for raw Lisp.
:ttags argument to
include-book had been required when
including a certified book that uses trust tags. This is no longer the case:
:ttags defaults to
:all except that warnings will be
printed. Thanks to Jared Davis for requesting such a relaxation, and to him
and Sandip Ray for useful discussions.
The definition of
mv-let has been modified so that the single-step
macroexpansion (see trans1) of its calls can be evaluated. Thanks to Pete
Manolios for bringing this evaluation issue to our attention and ensuing
discussions. On a related note, all calls of so-called ``guard-holders''
must-be-equal (from calls of see mbe),
mv-list -- are now removed before storing
hypotheses of rules of class
The handling of
~s has been modified so that if the
argument is a symbol that would normally be printed using vertical bars
|), then that symbol is printed as with
~f. Thanks to Jared Davis
for providing the following example showing that treatment of
~s was a
(cw "~s0.~%" '|fo\|o|).
Error messages have been improved for ill-formed terms (in ACL2's so-called ``translation'' routines). Thanks to Jared Davis for requesting such an enhancement.
defun-sk so that it executes in
Previously, evaluation of a
defun-sk event in
caused a somewhat inscrutable error, but now,
program mode is
treated the same as
logic mode for purposes of
The ``system hacker'' commands
) are now embedded event forms
(see embedded-event-form), hence may be used in books as well as in
The function symbol
worldp (in the
"ACL2" package) has been renamed
gc$-fn (resulting from macroexpansion of
gc$) is now
logic mode. Thanks to Jared Davis for requesting this change.
The user now has control over whether compilation is used, for example
whether or not
certify-book compiles by default, using function
set-compiler-enabled. See compilation.
For keyword argument
include-book, the value
:comp-raw is no longer legal. Its handling was broken; so it seems that
this value wasn't actually used by anyone.
Modified the conversion of relative to absolute pathnames in portcullis commands for book certification. Now, more pathnames remain as relative pathnames.
mv-list is the identity function logically, but converts
multiple values to lists. The first argument is the number of values, so an
example form is as follows, where
foo returns three values:
(mv-list 3 (foo x y)). Thanks to Sol Swords for requesting this
feature and for reporting a soundness bug in one of our preliminary
state global variable,
host-lisp, has as its value a keyword
whose value depends on the underlying Common Lisp implementation. Use
(@ host-lisp) to see its value.
It is now possible to write documentation for HTML without error when
there are links to nonexistent documentation topics. See the comments in
acl2::write-html-file at the end of file
doc/write-acl2-html.lisp. When there are such errors, they should be
easier to understand than previously. Thanks to Alan Dunn for providing the
It is now possible to inhibit specified parts of the Summary printed at the
conclusion of an event. See set-inhibited-summary-types. Also
see with-output, in particular the discussion of the new
keyword. Thanks to Sol Swords for requesting more control over the Summary.
:case-split-limitations, can override the
default case-split-limitations settings (see set-case-split-limitations) in
the simplifier. Thanks to Ian Johnson for requesting this addition and
providing an initial implementation.
The so-called ``too-many-ifs'' heuristic has been modified. Such a heuristic
has been employed in ACL2 (and previous Boyer-Moore provers) for many years,
in order to limit the introduction of calls of
IF by non-recursive
functions. Most users need not be concerned with this change, but two proofs
in the regression suite (out of thousands) needed trivial adjustment, so user
proofs could need tweaking. In one application, this modification sped up
proofs by 15%; but the change in runtime for the regression suite is
negligible, so such speedups may vary. Thanks to Sol Swords for providing a
test from ACL2 runs at Centaur Technology, which was useful in re-tuning this
Guard proof obligations could have size quadratic in the number of clauses in
case statement. This inefficiency has been removed with a change
that eliminates a hypothesis of the form
(not (eql term constant)) when
there is already a stronger hypothesis, equating the same term with a
different constant. Thanks to Sol Swords for bringing this problem to our
attention and suggesting an alternate approach to solving it, which we may
consider in the future if related efficiency problems persist.
We adjusted the heuristics for determining induction schemes in the presence
of ruler-extenders, when handling calls of a function symbol that is a
ruler-extender, in either of two cases: either the function takes only one
argument; or the function is
ec-call, and the first
argument contains no recursive call. These cases are treated more directly
as though the ruler-extender call is replaced by the unique (in the case of
ec-call, the second) argument.
true-listp-append, has been
(implies (true-listp b) (true-listp (append a b)))If you are interested in the motivation for adding this rule, see comments in
true-listp-appendin ACL2 source file
Fixed a soundness bug in destructor elimination, which was preventing some
cases from being generated. Thanks to Eric Smith for reporting this bug and
sending a helpful example. (Technical detail: the fixes were in ACL2 source
eliminate-destructors-clause1, and comments in the former contain Eric's
Fixed a bug that supported a proof of
nil by exploiting the fact that
portcullis commands were not included in check-sum computations in
a book's certificate. For such a proof of
nil, see the relevant
comment in the ACL2 source file
(deflabel note-3-7 ...).
Changed the implementation of
add-include-book-dir. The previous
implementation could allow relative pathnames to be stored in the
portcullis commands of certificates of books, which
perhaps could lead to unsoundness (though we did not try to exploit this to
nil). Thanks to Jared Davis for reporting a bug in our first new
implementation. An additional change to both
delete-include-book-dir is that these now work in raw-mode
Fixed a soundness bug related to
defun-nx, has been provided for declaring functions to be
non-executable; see defun-nx. While we expect this bug to occur only rarely
if at all in practice, the following example shows how it could be evoked.
;;;;;;;;;;;;;;;;;;;; ;;; Book sub.lisp ;;;;;;;;;;;;;;;;;;;; (in-package "ACL2") (defun f () (declare (xargs :guard t :non-executable t)) (mv-let (a b c) (mv 3 4) (declare (ignore a b)) c)) (defun g () (declare (xargs :guard t)) (prog2$ (mv-let (x y z) (mv 2 3 4) (declare (ignore x y z)) nil) (f))) (defthm g-nil (equal (g) nil) :hints (("Goal" :in-theory (disable (f)))) :rule-classes nil) ;;;;;;;;;;;;;;;;;;;; ;;; Book top.lisp ;;;;;;;;;;;;;;;;;;;; (in-package "ACL2") (include-book "sub") (defthm contradiction nil :hints (("Goal" :use g-nil)) :rule-classes nil)
The modification described above pertaining to
defun-nx also prevents
execution of non-executable functions that have been traced. The
following example illustrates the problem; now, the following
g is illegal, an the problem disappears if
defun-nx is used
(defun g (x) ; Use defun-nx to avoid an error after Version_3.6.1. (declare (xargs :guard t :non-executable t)) x) (g 3) ; causes error, as expected (trace$ g) (g 3) ; returned 3 before the bug fix; after fix, causes error as expected
A hard error was possible when attempting to include an uncertified book
containing events of the form
(make-event '(local ...)). This has
been fixed. Thanks to Sol Swords for bringing this issue to our attention.
Fixed a bug in the heuristic improvement described for Version_3.6 (see note-3-6) as ``We simplified induction schemes....'' The bug had prevented, in unusual cases such as the following (notice the impossible case), prevent a proof by induction.
(defun foo (a x) (and (consp x) (case a (0 (foo (car x) (cdr x))) (1 (foo (cdr x) (car x))) (0 (foo a (cons x x)))))) (in-theory (disable (:type-prescription foo))) (thm (atom (foo a x)))
cw-gstack did not work with an
:evisc-tuple argument. This
has been fixed by changing
cw-gstack so that it now evaluates its
arguments. Thanks to Sol Swords for bringing this bug to our attention.
Fixed a bug in
pso during the printing of failure messages for
Fixed a bug in the handling of
#. (see sharp-dot-reader). Thanks to Bob
Boyer for bringing this bug to our attention.
Replaced a hard Lisp error with a clean error, in certain cases that a
hints value is erroneously supplied as a non-
(thm (equal x x) :hints 3).
Fixed a bug in the interaction of function tracing with conversion of a
logic mode. The following
example illustrates what had been wrong.
(defun f (x) (declare (xargs :mode :program)) (car x)) (f 3) ; raw Lisp hard error (trace$ f) (f 3) ; raw Lisp hard error (still) (defun f (x) (car x)) ; upgrade f to :logic mode (f 3) ; clean guard violation; f is no longer traced (trace$) ; uh oh - f is shown as traced (untrace$ f) (f 3) ; OUCH: hard Lisp error because old :program mode definition of ; the executable counterpart (sometimes called *1*f) was restored!
Made a fix so that when building ACL2 with
there will no longer be any safety-0 compiled code generated. Thanks to Gary
Byers for bringing this bug to our attention.
Fixed a bug in the handling of override-hints that generate custom
keyword hints (see custom-keyword-hints) involving the variable
stable-under-simplificationp. Thanks to Ian Johnson for bringing this
bug to our attention with explanation that included a helpful example,
included as comment in the ACL2 source code for function
Fixed bug that could cause Lisp error when value
:comp! supplied for
include-book, in some Lisp
platforms including SBCL.
Fixed a bug in the interaction of
make-event with calls of
that take keyword arguments. Thanks to Jared Davis for reporting this bug
and sending the following example:
(time$ (make-event '(defun g (x) x)) :msg "Defun g")
saved_acl2 script in CLISP could contain unexpected characters where
simple newlines were expected. Dave Greve found this in a Cygwin environment
on Windows. Thanks to Dave for reporting this bug and experimenting with a
fix, and thanks to the CLISP folks for providing helpful information.
Fixed a bug that could make
oops cause an error.
NEW AND UPDATED BOOKS AND RELATED INFRASTRUCTURE
See http://code.google.com/p/acl2-books/wiki/BooksSince361 for a list of books not in Version 3.6.1. For changes to existing books rather than additions, see the log entries at http://code.google.com/p/acl2-books/source/list.
We note in particular the new
system/ directory, which begins to specify
ACL2 system code. Some system functions were changed slightly (but with the
expectation of not generally affecting ACL2 behavior) in support of the
development of this book.
New utilities have been provided for certifying most of the distributed books
make-level paralellism. See
books/make-targets, or to
books/workshops in the regression run, see
books/regression-targets. Thanks to Sol Swords for providing these nice
David Rager contributed modifications to the parallel version (see parallelism) to take advantage of atomic increments available at least since Version 1.0.21 of SBCL and Version 1.3 of CCL.
The HONS version, supported primarily by Bob Boyer and Warren Hunt
(see hons-and-memoization), has undergone numerous improvements. For
example, keyword argument
:FORGET is now supported when calling
memoize from within the ACL2 loop, and system function
is memoized with the
:condition that both terms are function
applications (clearing the memo-table after each prover invocation). Thanks
to Jared Davis and Sol Swords for investigating the memoization of
worse-than, and with suitable