NOTE-3-6

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 3.5 into the following categories of changes: existing features, new features, heuristic improvements, bug fixes, distributed books, Emacs support, and experimental hons-and-memoization version. Each change is described in just one category, though of course many changes could be placed in more than one category.

Note that (starting with ACL2 Version 3.5) LispWorks is no longer supported as a platform for ACL2, as the LispWorks compiler could not handle the ACL2 sources; see comments in the ACL2 sources about ``function size'' being ``too large''.

CHANGES TO EXISTING FEATURES

In the xargs declare form, the function symbol (or symbols, plural, in the case of mutual-recursion) being defined may now be used in the specified :measure and :guard terms. Note that, the definition(s) of the new symbol(s) are still not used in the termination proof. Thanks to Daron Vroon for discussions leading to this addition for the measure and to Dave Greve for requesting such an enhancement for the guard.

Processing of the :guard-hints in an xargs declare form is now delayed until the start of guard verification. As a result, the function symbol(s) being defined may now be used as one might expect in such hints, for example in an :in-theory form. Thanks to Jared Davis for suggesting that we make such an improvement and providing an example.

Made a low-level change to make-event in support of the ACL2s utility ``dynamic-make-event''. Thanks to Peter Dillinger for explaining the issue leading to this change.

Modified the failure message printed when a measure conjecture fails to be proved, to indicate whether or not the hint :ruler-extenders :all would create a different measure conjecture. Thanks to Peter Dillinger for suggesting such a modification.

A call of add-default-hints had added hints to the end of the current list of default hints. Now, it adds them to the beginning of that list, so that they are tried first. However, add-default-hints now takes a keyword argument, :at-end. If that argument is supplied and evaluates to other than nil, then the previous behavior occurs.

When save-exec is used to save ACL2 images, the build dates are now printed on separate lines at startup and in the executable script. Thanks To Bob Boyer for requesting some newlines.

Forward-chaining rules are now generated so that every let (also let* and lambda) expression is expanded away, as is every call of a so-called ``guard holder'' (must-be-equal, prog2$, ec-call, the). These were formerly only expanded away in the conclusion. Thanks to Konrad Slind for a helpful email leading to this change.

Current-theory now causes a hard error when applied to a name not found in the current ACL2 logical world, rather than simply returning nil.

When the underlying Common Lisp is GCL, ACL2 no longer uses the #n= reader macro when writing out certain files, including certificate files. In all other Lisps, it now uses the #n= ``print-circle'' feature not only for certificate files and ``expansion.lsp'' files written for example in support of make-event, but also for files written in support of :comp. This is all managed with new state global variable print-circle-files; see print-control. Thanks to Dave Greve for pointing out that GCL is limited by default to 1024 indices for #n=.

NEW FEATURES

A documentation topic explains in some detail how hints work with the ACL2 proof ``waterfall'': see hints-and-the-waterfall. This topic may be useful to those who write computed hints (see computed-hints) or other advanced hints.

Added a new hint keyword, :no-thanks, that avoids printing the usual ``Thanks'' message for hints. Thanks to Peter Dillinger for requesting this feature.

Added a new hint keyword, :backtrack, that checks the goals produced by processing a goal, and can cause the goal to be re-processed using a new hint. See hints. Thanks to Pete Manolios for a conversation that led to the idea of this hint.

Added a new class of hints, override-hints, that is similar to default-hints, except that override-hints are always applied, even if the user has supplied a hint explicitly for the goal. See override-hints. Thanks to Pete Manolios and Harsh Raju Chamarthi for useful discussions on this topic, including its application to testing.

When a goal ready to be pushed for proof by induction is given the new hint ``:do-not-induct :otf'', it is indeed pushed for proof by induction, rather than causing immediate failure as in the case of the hint ``:do-not-induct t''. Instead, the proof fails when the goal is later picked to be proved by induction. Thanks to Peter Dillinger for discussions leading to this feature.

Related to computed hints only: Each history entry in the list stored in variable HIST (see computed-hints) now has a :CLAUSE field, which provide's access to a goal's parent, parent's parent, and so on (within the same induction and forcing round only).

It is now possible to inhibit warnings produced by in-theory events and hints that occur when certain built-in definitions and executable-counterparts are disabled: just evaluate (assign verbose-theory-warning nil). Thanks to Jared Davis (and probably others in the past) for requesting such a mechanism.

HEURISTIC IMPROVEMENTS

A source function (linearize-lst) was replaced by tail-recursive code, which can avoid a stack overflow. Thanks to Dave Greve for sending a helpful example.

The heuristics for limiting forward-chaining have been slightly relaxed, to allow derivations based on the occurrence of all arguments of the forward-chaining rule's conclusion in the goal (after stripping leading calls of NOT). Thanks to Dave Greve for contributing this improvement and providing a motivating example.

We simplified induction schemes by eliminating each hypothesis of the form (not (equal term (quote const))) for which some other hypothesis in the same case equates term with some (presumably other) quoted constant. Thanks to Dave Greve for requesting an improvement of this sort.

BUG FIXES

Fixed a soundness bug related to redundancy of encapsulate events (see redundant-events) and ruler-extenders. A proof of nil in ACL2 Version 3.5 appears in a comment in (deflabel note-3-6 ...) in the ACL2 source code. The fix is to insist that in order for one encapsulate event to be redundant with another, they must be evaluated with the same default-ruler-extenders. Analogous to this issue of default-ruler-extenders for encapsulates is an issue of the default-verify-guards-eagerness, which has similarly been fixed.

Fixed soundness bugs related to the handling of subversive-recursions for constraints. Proofs of nil in ACL2 Version 3.5 appear in a comment in (deflabel note-3-6 ...) in the ACL2 source code.

Fixed a bug that could cause the following error during calls of certify-book in the presence of calls of skip-proofs in the book:

   ACL2 Warning [Skip-proofs] in

   HARD ACL2 ERROR in FMT0: Illegal Fmt Syntax.  The tilde-@ directive at
   position 0 of the string below is illegal because its variable evaluated
   to 0, which is neither a string nor a list.

   "~@0"

The :corollary of a rule (see rule-classes) failed to use the default-hints of the logical world. This has been fixed.

(CCL only) We removed a call, for CCL 1.3 (and beyond) only, of foreign function sync in the closing of output channels. Thanks to Daron Vroon for reporting issues with such a call on a non-Intel platform.

Fixed a bug in reporting failures when monitoring rewrite rules with free variables in the hypotheses, that could cause a hard Lisp error (from which ACL2 continues, however). Thanks to Eric Smith for sending a very helpful example with his bug report.

Fixed the handling of :induct hints, which had thrown away hint information from parent goals. For example, the thm form below failed to prove even though the second hint is in some sense superfluous; induction occurs automatically at "Goal'" even without the hint on that. The failure was due to discarding the hint information on "Goal".

(in-theory (disable append))
(thm (equal (cdr (cons a (append (append x y) z))) (append x y z))
     :hints
     (("Goal" :in-theory (enable append))
      ("Goal'" :induct t) ; failed unless this line is commented out
      ))

Fixed a bug in the args command that was failing to show the formals of primitives (built-in functions like consp that do not come with explicit definitions). Thanks to John Cowles for pointing out this bug. (At a lower level, the bug was that primitives failed to have 'stobjs-in or 'stobjs-out properties.)

Fixed bugs in the utility supporting moving directories of certified books, sometimes used in Debian builds (as described in source function make-certificate-file). Thanks to Alan Dunn for pointing out such a bug, in paths associated with defpkg events in portcullis commands in certificates (which are used for error reporting). There were also bugs, now fixed, that prevented renaming some book paths. Please note that this mechanism is not guaranteed to be sound; in particular, it can probably misbehave when macros are used to generate portcullis events. However, it seems likely that such issues will be very rare.

Eliminated warnings that could arise when tracing a function with trace$. Now, when trace$ is applied to a function without option :native, that function's declarations and documentation are discarded.

Fixed a bug that could cause a failure when building an executable image using SBCL as the underlying Common Lisp. Thanks to Jun Sawada for reporting this failure. We made a similar fix for CMUCL.

Fixed a bug in save-exec in the case that an absolute pathnanme is supplied. Thanks to Jared Davis for bringing this bug to our attention.

Fixed a bug in the use of trace$ with the :native and :multiplicity options that caused hard errors for some underlying Lisps.

Fixed a bug in the interaction of trace$ and :comp, which caused error as comp tried to re-trace functions that it temporarily untraced.

NEW AND UPDATED BOOKS AND RELATED INFRASTRUCTURE

See http://code.google.com/p/acl2-books/wiki/BooksSince35 for a list of books in Version 3.6 of ACL2 but not Version 3.5. For changes to existing books rather than additions, see the log entries at http://code.google.com/p/acl2-books/source/list starting with revision r286 up through revision r329.

It is no longer required to specify a value for environment (or `make') variable ACL2_SYSTEM_BOOKS when running make in the distributed book directory, even when that directory is not under the directory containing the ACL2 executable. Thanks to Peter Dillinger for providing this improvement, by modifying books/Makefile-generic and, as needed, distributed book Makefiles.

Thanks to Peter Dillinger, some books in support of the ACL2 Sedan (ACL2s) are more easily available for ACL2 users who do not use ACL2s. See acl2-sedan.

EMACS SUPPORT

If the following form is evaluated before the load of emacs/emacs-acl2.el, then variables are now set to reflect the directory containing that file.

(if (boundp '*acl2-sources-dir*)
    (makunbound '*acl2-sources-dir*))

Fixed info-dir-entry line in generated info file (by patching doc/write-acl2-texinfo.lisp). Thanks to Alan Dunn for providing this patch.

EXPERIMENTAL HONS VERSION

Bob Boyer and others have contributed numerous changes for the experimental ``hons'' version of ACL2 (see hons-and-memoization). A number of these have been crafted to work specifically with CCL (Clozure Common Lisp, formerly OpenMCL), which is now required as the underlying Lisp for the ``hons'' version of ACL2.

A heuristic (source function too-many-ifs has been made more scalable (for the non-HONS version as well, in fact), but with no functional change. Thanks to Jared Davis for noticing performance issues and suggesting fixes.

Other changes including the following, quoting Bob Boyer:

The CCL CASE macro now does better than a dumb linear search in some CASEes. SH and CSH are functions to talk to the underlying Gnu-Linux from CCL. Good for repeated calling when you simply cannot afford the copying cost of a FORK because you are using, say, a dozen gigabytes.

Added CCL compiler-macros for IF and OR, to support some 'coverage' analysis, cf. IF-REPORT, extending the profiling.

Introduced the type 'mfixnum' so that things like counting honses and counting calls to memoized or profiled functions can run fast in CCL 64 bits and yet still run at all under 32 bits.

Moved all HONSes to CCL's newish static space, which permits the address of a cons to be used as a hash key, as in most Lisps. (CCL moves most conses and most everything when it does a compacting-gc.)

Quite a few changes in the memoize-fn reporting.

Added a timer facility, cf. call-with-timeout. Good for running under throttle some gross thoughts like 'Is it true that you can't fit 12 pigeons into 11 holes' on some propositional calculus systems/functions.

Added rwx-size, pid-owner-cmdlines, rss, and proc-stat to help see what is really going on virtually in Gnu-Linux.

Fixed at least one bug in compact-print-file and helped make its integration into ACL2's read-object$ a little more sound. Still worried some about *print-readably* vs. readtable-case. Does anyone else stay awake late at night worrying about readtable-case?

Revised how the *watch-dog-process* interrupts the main process for the thousandth time, cf. watch. Haven't changed it in weeks, which means that (a) it is getting tolerable or (b) I've run out of gas.