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
declare form, the function symbol (or symbols,
plural, in the case of
mutual-recursion) being defined may now be used
in the specified
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
Processing of the
:guard-hints in an
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
:at-end. If that argument is supplied and evaluates to
nil, then the previous behavior occurs.
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
lambda) expression is expanded away, as is every
call of a so-called ``guard holder'' (
the). These were formerly only expanded away in the
conclusion. Thanks to Konrad Slind for a helpful email leading to this
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
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
comp. This is all managed with new state global
print-circle-files; see print-control. Thanks to Dave Greve
for pointing out that GCL is limited by default to 1024 indices for
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
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
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
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.
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
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
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.
Fixed a soundness bug related to redundancy of
(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
event to be redundant with another, they must be evaluated with the same
default-ruler-extenders. Analogous to this issue of
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
(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"Thanks to Dave Greve for reporting this bug and making available a very helpful test case.
: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
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
(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
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
:multiplicity options that caused hard errors for some underlying Lisps.
Fixed a bug in the interaction of
caused error as
comp tried to re-trace functions that it temporarily
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')
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,
books/Makefile-generic and, as needed, distributed book
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
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
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.