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 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
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 (
has been added, along with corresponding utilities
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-checker 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 or
dmr; see dmr.
dmr monitoring is enabled, then
(dmr-start) will have no
effect other than to print a corresponding observation, and if monitoring is
(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
t (see set-debugger-enable), and the debugger remained
(dmr-stop) was invoked. Now, the debugger is only enabled
(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
set-debugger-enable has first been called after that automatic
enabling. Finally, if the value of state global variable
:bt, then the new value will be
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
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 printed.
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
See set-inhibit-warnings, and see set-inhibit-warnings! for a variant that
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,
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
e2, and so on are evaluated, in order, until the evaluation of
ek completes without error. In that case, the expansion is treated
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
for an example. Second, an expansion may be of the form
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.
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
in that it executes a command. Unlike
returns values that include output from the command (in addition to the exit
status), rather than simply printing the command. See sys-call+.
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
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
:by hints has been changed in the
following two rather subtle ways, thanks to suggestions from Sol Swords.
:byhints, 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'' (
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
:byhint that is a
:functional-instance, if a
:do-nothint (see hints) has specified that
preprocess-clauseis 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
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 file
(GCL only) Fixed an obscure soundness bug due to an error in the GCL
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
: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 LispWorks.
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 ``
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
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,
specifies a form to evaluate before quitting the read-eval-print loop at
startup. See save-exec. Also see the source function
and its comments, source file
acl2-init.lisp, for more information.
Thanks to Jared Davis for suggesting the use of
"$@", as well as
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 `
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
(SBCL only) Fixed
save-exec for host Lisp SBCL to provide the same export
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.
emacs/emacs-acl2.el to eliminate some warnings that were
appearing in a recent Emacs version, replacing
(goto-char (point-max)) and
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 hons-shrink-alist. 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 this problem.
(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.