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 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
The proof-builder command
We made the following minor changes to the behavior of
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
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
It had been the case that lp took a single argument,
The functionality of make-event has been significantly expanded.
First: if the expansion is of the form
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
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
: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'' (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
:useor :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
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
(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
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
Fixed a bug in wof, hence in psof (which uses
A small logical bug has been fixed in the logical definition of sys-call-status. Formerly it always returned
Fixed a bug that was causing an error upon evaluation of the form
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 ``
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
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
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 `
(SBCL only) Fixed
(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.
(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
(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.