NOTE-6-3

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 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.

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.