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
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-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.
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 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 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
eliminated.
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.
NEW FEATURES
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 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
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.
HEURISTIC IMPROVEMENTS
The processing of :use
and :by
hints has been changed in the
following two rather subtle ways, thanks to suggestions from Sol Swords.
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 thatpreprocess-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.
BUG FIXES
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 file
ld.lisp
.
(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
this error.
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 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
between releases.
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 (inline
''.)
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 discussions.
(SBCL only) Fixed save-exec
for host Lisp SBCL to provide the same export
of variable SBCL_HOME
that was provided in the original saved_acl2
script.
(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 SUPPORT
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.
EXPERIMENTAL/ALTERNATE VERSIONS
(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.