ACL2 Version 3.6 (August, 2009) 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
Processing of the
Made a low-level change to make-event in support of the ACL2s
Modified the failure message printed when a measure conjecture fails to be
proved, to indicate whether or not the hint
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,
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
When the underlying Common Lisp is GCL, ACL2 no longer uses the
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,
Added a new hint keyword,
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
Related to computed hints only: Each history entry in the list stored in
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
A source function (
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
We simplified induction schemes by eliminating each hypothesis of the form
Fixed a soundness bug related to redundancy of encapsulate events
(see redundant-events) and ruler-extenders. A proof of
Fixed soundness bugs related to the handling of subversive-recursions for constraints. Proofs of
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"
Thanks to Dave Greve for reporting this bug and making available a very helpful test case.
(CCL only) We removed a call, for CCL 1.3 (and beyond) only, of foreign
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
(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
Fixed bugs in the utility supporting moving directories of certified books,
sometimes used in Debian builds (as described in source function
Eliminated warnings that could arise when tracing a function with trace$. Now, when trace$ is applied to a function without option
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 pathname is supplied. Thanks to Jared Davis for bringing this bug to our attention.
Fixed a bug in the use of trace$ with the
Fixed a bug in the interaction of trace$ and
NEW AND UPDATED BOOKS AND RELATED INFRASTRUCTURE
See ReleaseVersionNumbers 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 starting with revision r286 up through revision r329.
It is no longer required to specify a value for environment (or `make')
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.
If the following form is evaluated before the load of
(if (boundp '*acl2-sources-dir*) (makunbound '*acl2-sources-dir*))
Fixed info-dir-entry line in generated info file (by patching
EXPERIMENTAL HONS VERSION
Bob Boyer and others have contributed numerous changes for the experimental
A heuristic (source function
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.