ACL2 Version 6.3 (October, 2013) Notes
NOTE! New users can ignore these release notes, because the documentation has been updated to reflect all changes that are recorded
Below we roughly organize the changes since Version 6.2 into the following
categories of changes: existing features, new features, heuristic
improvements, bug fixes, changes at the system level, Emacs support, and
experimental versions. Each change is described in just one category, though
of course many changes could be placed in more than one category.
CHANGES TO EXISTING FEATURES
The evaluation of a term from a bind-free hypothesis had been
expected to produce an alist binding free variables to terms. While that is
still legal, it is also legal for that evaluation to produce a list of such
alists: then each is considered, until one of them permits all remaining
hypotheses to be relieved. See bind-free. Thanks to Sol Swords for
requesting this enhancement.
ACL2 continues to provide a way to specify keyword command abbreviations
for the top-level loop; see ld-keyword-aliases. However, ld-keyword-aliases is now a table rather than a state global;
it is thus no longer a so-called ld special. The functionality of
set-ld-keyword-aliases has essentially been preserved, except that it is
now an event (see events), hence it may appear in a book; it is local to a book (or encapsulate event); and the state
argument is optional, and deprecated. A non-local version
(set-ld-keyword-aliases!) has been added, along with corresponding
utilities add-keyword-alias and add-keyword-alias! for adding a
single keyword alias. See ld-keyword-aliases. Thanks to Jared Davis
for correspondence that led us to make this change.
The proof-builder command (exit t) now exits without a query
(but still prints an event to show the :INSTRUCTIONS). Thanks to Warren
Hunt for feedback leading us to make this change.
We made the following minor changes to the behavior of dmr; see dmr. First, if dmr monitoring is enabled, then (dmr-start) will
have no effect other than to print a corresponding observation, and if
monitoring is disabled, then (dmr-stop) will have no effect other than to
print a corresponding observation. Second, it had been the case that when
(dmr-start) is invoked, the debugger was always automatically enabled
with value t (see set-debugger-enable), and the debugger remained
enabled when (dmr-stop) was invoked. Now, the debugger is only enabled
by (dmr-start) if it is not already enabled and does not have setting
:never. Moreover, if such automatic enabling takes place, then the old
setting for the debugger is restored by (dmr-stop) unless set-debugger-enable has first been called after that automatic enabling.
Finally, if the value of state global variable 'debugger-enable is
:bt, then the new value will be :break-bt, not t.
When a call of progn is executed in the ACL2 loop, its constituent
events and their results are printed, just as was already done for
calls of encapsulate. Thanks to Jared Davis for a conversation
causing us to consider this change.
(CCL only) When set-debugger-enable is invoked with an argument
that prints a backtrace and CCL is the host Lisp, the backtrace will be
limited to 10,000 stack frames. (We have seen more than 65,000 stack frames
before this change.) This limit is the value of raw Lisp variable
*ccl-print-call-history-count*, which may be assigned another positive
integer value to serve as the maximum number of stack frames to be
Improvements have been made pertaining to the disabling (inhibiting) of
individual types of warning. Now, inhibited warnings are implemented in a
straightforward way using a separate table for this purpose, the
inhibit-warnings-table, rather than using the ACL2-defaults-table. See set-inhibit-warnings, and see set-inhibit-warnings! for a variant that is not local to an encapsulate or a book in which it occurs. Thanks to Sol Swords for sending
examples showing how set-inhibit-warnings did not always behave as one
might reasonably expect when books are involved.
It had been the case that lp took a single argument, 'raw.
This argument was not documented and also caused an error, so it has been
The functionality of make-event has been significantly expanded.
First: if the expansion is of the form (:OR e1 e2 ...), then event forms
e1, e2, and so on are evaluated, in order, until the evaluation of
some ek completes without error. In that case, the expansion is treated
simply as ek. With this capability, alternative expansions can be
attempted and the successful one does not need to be evaluated again. See the
new version of community book books/make-event/proof-by-arith.lisp for an
example. Second, an expansion may be of the form (:DO-PROOFS e), in
which case the event e is evaluated with proofs not skipped; see
ld-skip-proofsp. Third, new keyword :EXPANSION? can be used to
avoid storing expansions in certificate files. See make-event.
When a defun event prints a failure message in the summary, that
message now indicates when the failure is due to a failed proof of guard
verification or a failed proof of the measure theorem. Thanks to Shilpi Goel
for requesting this enhancement.
ACL2 can now be instructed to time activities using real time (wall clock
time) instead of run time (typically, cpu time). See get-internal-time. Thanks to Jared Davis for asking to be able to obtain
real-time reports in event summaries.
A new utility, sys-call+, is similar to existing utility sys-call in that it executes a command. Unlike sys-call, however,
sys-call+ returns values that include output from the command (in
addition to the exit status), rather than simply printing the command. See
The new macro verify-guards+ extends the functionality of verify-guards by permitting macro-aliases (see macro-aliases-table).
See verify-guards+. Thanks to Jared Davis for requesting this feature
and suggesting the use of make-event in its implementation. We have
also modified verify-guards to print a friendlier error message when
its argument is a macro-alias.
See last-prover-steps for a new utility that returns the number of
prover steps most recently taken.
The processing of :use and :by hints has been changed in
the following two rather subtle ways, thanks to suggestions from Sol
o For :by hints, the simplest check was an equality check, rather than
a more general subsumption check. That equality check was made after removing
so-called ``guard holders'' (must-be-equal, prog2$, ec-call, the) from both the previous theorem and the purported
theorem. Now, guard-holder removal has been strengthened, so that the results
are also put into so-called quote-normal form, for example replacing (cons
'3 '4) by '(3 . 4).
o For a lemma-instance provided to a :use or :by hint that
is a :functional-instance, if a :do-not hint (see hints) has
specified that preprocess-clause is not to be used, then preprocessing
will not be used on the constraints.
We eliminated certain warnings about being ``weak'' for every :type-prescription rule whose conclusion designates that the function call can
be equal to one of its arguments, e.g., (or (integerp (foo y)) (equal (foo
y) y)). In many cases (such as the one above), such warnings about ``weak''
simply aren't correct.
Fixed a soundness bug that was permitting a stobj to be bound by a
let or mv-let form, without being among the outputs of that
form. Thanks to Jen Davis and Dave Greve for reporting this bug. Their
report included an example which forms the basis for a proof of nil,
included as a comment in the form (deflabel note-6-3 ...) in ACL2 source
(GCL only) Fixed an obscure soundness bug due to an error in the GCL
implementation of set-debugger-enable. For details, see the relevant
comment in the ACL2 source code under (deflabel note-6-3 ...).
Fixed a bug in the case of a field of a (concrete) stobj that is an
abstract stobj (see nested-stobjs). Thanks to David Rager for bringing
this bug to our attention.
Splitter output for type if-intro (see splitter) could formerly
occur even when at most one subgoal is generated. This has been fixed.
Fixed a bug in wof, hence in psof (which uses wof),
that was causing the printing of a bogus error message.
A small logical bug has been fixed in the logical definition of sys-call-status. Formerly it always returned (mv nil state) whenever
the oracle of the state is non-empty (see state).
Fixed a bug that was causing an error upon evaluation of the form
(set-prover-step-limit nil). Thanks to David Russinoff for reporting
The :measure (if supplied) is now ignored when checking redundancy
with respect to a non-recursive definition that is not defined within a mutual-recursion. (See redundant-events and see xargs.) It
had been possible to get a low-level ACL2 error in this situation. Thanks to
Jared Davis for reporting this bug with a helpful example.
Eliminated a potential error when using comp to compile an
uncompiled function defined under progn!, which we observed in
CHANGES AT THE SYSTEM LEVEL
The ACL2 sources are now publicly available between ACL2 releases, using
svn; see the new ``acl2-devel'' project hosted by Google code at
http://acl2-devel.googlecode.com. Although such a copy of ACL2 is likely
to work well with the latest svn (trunk) revision of the ACL2 community
books (see community-books), please take seriously the warning message
printed at startup: ``The authors of ACL2 consider svn distributions to be
experimental; they may be incomplete, fragile, and unable to pass our own
regression.'' That message also provides instructions for bug reports. If
you decide to use svn versions of either the community books or ACL2, then you
should use both, as they tend to be kept in sync. We fully expect ACL2
releases to continue from time to time, as usual. Thanks to Jared Davis for
his efforts in setting up the new acl2-devel project and svn repository, and
to him and David Rager for convincing us to distribute ACL2 sources via svn
Thanks to a suggestion from Jared Davis, over 30 built-in functions are now
declared to be inline in order to boost performance. (The list may be found
by searching ACL2 source file axioms.lisp for ``(declaim
Better support has been provided for command line arguments, especially
those supplied directly by the user when calling ACL2. For one, problems with
quoting have been solved using "$@" in place of $*. Also, the
function save-exec now allows specification of arguments, both for the
host Lisp as well as ``inert'' arguments that can be passed along to calls of
programs (as with sys-call). A keyword argument,
:return-from-lp, specifies a form to evaluate before quitting the
read-eval-print loop at startup. See save-exec. Also see the source
function user-args-string and its comments, source file
acl2-init.lisp, for more information. Thanks to Jared Davis for
suggesting the use of "$@", as well as modifications to save-exec and helpful conversations about that.
A rather extensive overhaul has taken place for the function proclaiming
mechanism. As before, this is only used when the host Lisp is GCL. However,
building an executable is now faster for some Lisps, including GCL, by
avoiding repeated recompilation and perhaps repeated initialization.
(CCL only) We increased stack sizes when the host Lisp is CCL. The default
for recent CCL versions is equivalent to specifying `-Z 2M' on the
command line, but saved ACL2 scripts (including experimental versions ACL2(h),
ACL2(p), ACL2(r), and combinations of them) to `-Z 64M', representing a
32-fold increase. Thanks to Jared Davis for pointing us to community books
file books/centaur/ccl-config.lsp and to Sol Swords for helpful
(SBCL only) Fixed save-exec for host Lisp SBCL to provide the same
export of variable SBCL_HOME that was provided in the original
(GCL only) We made changes, following suggestions from Camm Maguire (whom
we thank for these suggestions), to support ACL2 builds on recent versions of
GCL (2.6.8 and 2.6.10; we recommend against using GCL 2.6.9, since issues
there were fixed in 2.6.10). Specifically, we no longer set the hole size,
and we allocate contiguous pages sufficient to run an ACL2 regression without
failing due to memory limitations.
Modified file emacs/emacs-acl2.el to eliminate some warnings that were
appearing in a recent Emacs version, replacing (end-of-buffer) by
(goto-char (point-max)) and next-line by forward-line. Thanks
to Warren Hunt for bringing the warnings to our attention.
(Allegro CL only) ACL2(h) now avoids blow-ups in hash table sizes that
could be caused by fast-alist-fork. Thanks to Jared Davis for
helping to debug this problem, and to David Rager for contributing the
community book books/parsers/earley/earley-parser.lisp, which highlighted
(SBCL only) Fixed a bug that was causing a Lisp break after turning on
waterfall-parallelism. Thanks to David Rager for confirming that our
proposed fix is correct.