Note-7-0
ACL2 Version 7.0 (January, 2015) 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 to ACL2 since Version 6.5 into the
following categories of changes: existing features, new features, efficiency
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.
A particularly major change with this release is that by default, ACL2
executables are hons-enabled: see hons-and-memoization. We
expect this change to be backward compatible for current ACL2 users, other
than a change to the name of the executable, as described below.
- As before, there are two ways to build ACL2: either hons-enabled,
to produce ACL2(h) with executable name saved_acl2h; or not hons-enabled,
to produce ``classic ACL2'', which we now call ACL2(c), with executable name
saved_acl2. [Note: These defaults were changed after Version_7.0.]
- Unlike before, the default build of ACL2 is now ACL2(h), hence with name
saved_acl2h [after Version_7.0, once again saved_acl2]. It is still
possible to build ACL2(c) (hence with name saved_acl2) [after
Version_7.0, saved_acl2c], but this is not the default.
- The change to building ACL2(h) by default may require you to change
scripts and environment variables to point to saved_acl2h rather than
saved_acl2. [This change is only for Version_7.0, not later
versions.]
Note that after the next ACL2 release, we might only support hons-enabled ACL2 builds.
See also note-7-0-books for a summary of changes made to the ACL2
Community Books since ACL2 6.5, including the build system.
Changes to Existing Features
Three new theorems have been built into ACL2 to allow some additional
simple arithmetic reasoning. For example, the following failed before this
change, typically causing the user to include an arithmetic book; but that is
no longer necessary.
(thm (implies (natp x)
(equal (expt 2 (+ 1 -1 x))
(expt 2 x))))
Thanks to Jared Davis for suggesting these, and for providing seven small
modifications to the community books to keep proofs from failing after the
changes. (So, if you have a proof failure involving `plus' (+) that
formerly succeeded, consider disabling one or more of these rules.) Here are
the three new built-in theorems.
Theorem: commutativity-2-of-+
(defthm commutativity-2-of-+
(equal (+ x (+ y z)) (+ y (+ x z))))
Theorem: fold-consts-in-+
(defthm fold-consts-in-+
(implies (and (syntaxp (quotep x))
(syntaxp (quotep y)))
(equal (+ x (+ y z)) (+ (+ x y) z))))
Theorem: distributivity-of-minus-over-+
(defthm distributivity-of-minus-over-+
(equal (- (+ x y)) (+ (- x) (- y))))
Type-set reasoning has been improved for a few built-in functions,
including first-n-ac, substitute, nthcdr, and subseq, and thus for some functions whose computed type depends on one of
these: for example, take and therefore, also butlast and
subseq-list, are now known to return true-listp results.
Thanks to Jared Davis for a request that led us to these changes. In
particular, the definitions of first-n-ac and substitute-ac have
been modified to call revappend instead of reverse, and the
following :type-prescription rules have been added to source file
axioms.lisp (and can be seen using :pe).
- true-listp-first-n-ac-type-prescription
- stringp-substitute-type-prescription
- true-listp-substitute-type-prescription
- true-listp-nthcdr-type-prescription
- stringp-subseq-type-prescription
- true-listp-subseq-type-prescription
Technical note on the above change: in some cases, the built-in
:type-prescription rule has been changed, essentially for the
better, but new rules have also been added. Consider for example the
function, substitute. This function calls substitute-ac, which
in turn now calls revappend instead of reverse, which allows
ACL2 to deduce a :type-prescription rule saying that substitute
returns a string or a true-list. However, new :type-prescription rules
stringp-substitute-type-prescription and
true-listp-substitute-type-prescription allow the stronger conclusion
that substitute returns a string or true-list, respectively depending on
whether type-set reasoning can deduce that the given sequence is or is
not a string. The deduced :type-prescription rule can still be of some
use in cases that type-set reasoning cannot establish whether or not the input
sequence is a string.
We removed support for processing legacy documentation strings
(those starting with ":Doc-Section"), since the xdoc system has
been stable for some time. Thanks to Jared Davis for assisting in that effort
and to David Rager for his encouragement. The ACL2 system and community-books still have code to support such processing, but it is
essentially commented out: specifically, each such piece of code is prefixed
by #+acl2-legacy-doc. We expect to delete such code entirely before the
next release.
The with-output macro now takes a new keyword, :evisc, that
specifies evisc-tuples. Thanks to Warren Hunt for requesting a way to
submit defun forms in a way that avoids printing large guard
goals during guard verification. The following example illustrates a way to
arrange this.
(defmacro defun/ (&rest args)
(mv-let (evisc args)
(cond ((eq (car args) :evisc)
(mv (cadr args) (cddr args)))
(t (mv '(:gag-mode (evisc-tuple 3 4 nil nil)) args)))
`(with-output :evisc ,evisc
(defun ,@args))))
; example:
(defun/ h (x)
(declare (xargs :guard t))
(append (cons (make-list 10) x) x))
The utility :pl2 no longer automatically instantiates free
variables; similarly for calls of :pl on a term. Thanks to Eric
Smith for sending an example showing the problem with the previous
implementation.
When the ld-evisc-tuple is non-nil, the utilities :pe, :pc, and :pcb! now abbreviate their output
accordingly. See set-evisc-tuple. Thanks to David Rager for bringing
the need for this change to our attention.
The utility disabledp now accepts runic abbreviations such as
(:d append). (See theories for a discussion of runic
abbreviations.) Thanks to Shilpi Goel for requesting this enhancement.
Gc-verbose now takes an optional second argument, which is only relevant
when the host Lisp is CCL, where that argument specifies verbosity for
EGC.
Nests of car and cdr calls are now printed
(``untranslated'') differently. The old method availed itself of all 28 of
the car-cdr macros. The new method only introduces 6 of them: cadr,
caddr, cadddr, cddr, cdddr, cddddr. It never
introduces such macros as caar or cddaar, preferring cars and
cdrs when necessary. Lisp programmers tend to recognize cadr,
caddr, and cadddr as the accessors for the 1st, 2nd, and
3rd (0-based) elements of a list. See community book
books/system/untranslate-car-cdr.lisp for further discussion and a
correctness proof.
It is now possible to create more efficient :meta rules by
writing metafunctions that create ``implicit hypotheses.'' See
meta-implicit-hypothesis.
We improved a few built in rules: lower-case-p-char-downcase,
upper-case-p-char-upcase, lower-case-p-forward-to-alpha-char-p, and
upper-case-p-forward-to-alpha-char-p. We also improved the rule
alpha-char-p-forward-to-characterp by replacing it with two rules,
alpha-char-p-forward-to-standard-char-p and
standard-char-p-forward-to-characterp. The new rules are, as before, in
ACL2 source file axioms.lisp.
The reader macro sharp-comma (#,), which has been deprecated
since ACL2 Version 3.5 (May, 2009), has been eliminated. Use sharp-dot
(#.) instead; see sharp-dot-reader.
A defthm or defaxiom event is now redundant when there is
already a syntactically identical event in the logical world, even if
the rules suggested by the two events differ. See redundant-events. Thanks to Jared Davis and Sol Swords for sending the
following example, which illustrates the change. Previously, the final event
was not redundant, and hence failed. Now, it is redundant, even though the
:typed-term suggested by the new type-prescription rule is
(booleanp (foop x)) where the existing rule's :typed-term is
(foop x).
(defund foop (x) (consp x))
(defthm booleanp-of-foop
(booleanp (foop x))
:rule-classes :type-prescription)
(in-theory (disable booleanp-compound-recognizer))
(defthm booleanp-of-foop
(booleanp (foop x))
:rule-classes :type-prescription)
In the case that summary output is inhibited but error output is not (see
set-inhibited-summary-types), failed events did not print an
error message. Now they do.
When a call of encapsulate with empty signature introduces no
events, it now has no effect on the ACL2 logical world.
Formerly, such an encapsulate form would create an event even in this
case. For example, the form (encapsulate nil (local (defun f (x) x)))
formerly created an event in the world, as well as a command when
executed at the top-level; but now it is truly a no-op. See encapsulate. Note: An idiom sometimes used for testing is
(encapsulate () (local ...) (local ...) ...), that is, a trivial
encapsulate where each sub-event is local. With this change, that
idiom is now properly supported. (Formerly, the second such encapsulate was
considered redundant with the first; but that is no longer the case, since the
first will not be stored in the world.)
We replaced an error with a warning for cases where a classic congruence rule is unnecessary. Thanks to Jared Davis for sending us an
example suggesting the need for a change. (See ACL2 source function
chk-acceptable-congruence-rule for his example and more explanation.)
We removed support for three declare forms that had been permitted
in ACL2(h) only, but were not advertised: dynamic-extent, inline and
notinline, because they seem difficult or impossible to support
correctly. For alternatives to using inline and notinline
declarations, see defun-inline and defun-notinline.
The nu-rewriter contained special provisions for rewriting expressions
composed of nth, update-nth, and update-nth-array,
together with let expressions and other applications of non-recursive
functions or lambda expressions. An email query was sent to the acl2
mailing list on 10/24/2014, giving people an opportunity to object to the
removal of this feature. Nobody objected, so we have removed it in order to
simplify the ACL2 code base. Thanks to David Rager for suggesting this sort
of code clean-up. Note that some system functions, for example
all-equal, have been deleted in support of this change.
Guards have been added for some system functions that support the
implementation of the tau-system: lower-bound-<=,
upper-bound->=, lower-bound->, upper-bound-<, and
squeeze-k. Thanks to Dmitry Nadezhin for supplying these improvements
(which he also used in modifications to the community book,
books/tau/bounders/elementary-bounders.lisp).
New Features
The new command :btm has been added to the list of valid brr-commands, to show the bottom-most frame in the path. Thanks to David
Rager for requesting this feature.
A new xargs keyword, :measure-debug, decorates each
termination proof goal with extra-info calls that show the source of
the goal. Thanks to Jared Davis (first in 2008!), Sol Swords, and Anna
Slobodova for requesting this feature.
A new reader macro, #{"""..."""}, has been contributed by Jared
Davis to support the writing of strings without escape characters. See his
community book books/system/fancy-string-reader-test.lisp for
examples.
(For those who program in raw Lisp) A new Lisp variable,
*hard-error-is-error*, has a default of nil that preserves existing
behavior; but it can be set to a non-nil value in order to cause
so-called ACL2 ``hard errors'' to result in Lisp errors whose condition, when
printed with format directive ~a, is the same error message that
ACL2 would otherwise print. See hard-error. Thanks to Jared Davis for
requesting this feature.
A new value for include-book keyword argument :uncertified-okp
is :ignore-certs, which specifies that all certificate files are to be
ignored during inclusion of this book and all of its sub-books. See include-book. Thanks to Sol Swords for requesting this feature and for
helpful discussions on its details.
Efficiency Improvements
The heuristics have changed for guessing the :typed-term field for a
:type-prescription rule when that field is not explicitly
specified. Specifically, consider the case that the conclusion of the rule is
a function call (p u) for some term u, such that there is an enabled
compound-recognizer rule for p. Formerly, the :typed-term
was u in this case. Now, it must be the case that the most recent
enabled such compound-recognizer rule is `strong', in the following
sense: if ts1 is the type-set implied by assuming the conclusion
true and if ts2 is the type-set implied by assuming the conclusion
false, then ts1 and ts2 are complementary. Thanks to Jared Davis
for an email that prompted us to make this change.
We have made several efficiency improvements (arguably heuristic in
nature), which may apply in many settings but especially in handling of
several forms during the execution of include-book — most
notably with-output forms, as (with-output ... FORM) is now
essentially just FORM during include-book. For some details,
including statistics showing up to 1/3 of include-book time eliminated
by these changes (and even significant time saved outside include-book),
see the comment about ``efficiency improvements'' in Community Books file
system/doc/acl2-doc.lisp, form (defxdoc note-7-0 ...). Thanks
to Sol Swords for noticing inefficiencies that led us to these improvements,
and for helpful discussions.
The dmr utility has been made much more efficient, yielding a
performance penalty of perhaps 10% instead of perhaps more than a factor of
30 (3000%).
We made a low-level implementation tweak that resulted in a speed-up of
2.6% in wall-clock time for a CCL-based regression (using ``make'' with
-j 8 and target ``everything''). (Technical note: We eliminated the Lisp
special variable *attached-fn-called*, using another variable *aokp*
instead. Special variable bindings can apparently be expensive!)
Some space has been saved in ACL2 executables by avoiding the duplication
of certain constants. Specifically: for each event (defconst name (quote
val)) in the ACL2 source files, val is stored in the Lisp image in
several places, but not all of these had been identical: they were all equal, but not all eq. (We believe that these were already all
eq for user-defined defconst events.) For example, in Linux
builds of ACL2(h) on host Lisp CCL, we have seen a space saving of
approximately 18.9 MB, which is 12.6%. Thanks to Jared Davis for pointing out
duplicate strings that he noticed using his spacewalk tool.
Bug Fixes
We fixed two bugs in spec-mv-let. The first was pointed out to us
by Jared Davis using essentially the following example, where the result
should be nil given that spec-mv-let is intended to have the
semantics of mv?-let.
ACL2 !>(set-ignore-ok t)
T
ACL2 !>(let ((a t)
(xval nil))
(spec-mv-let (yval)
xval
(mv?-let (xval)
a
(if xval
yval
nil))))
T
ACL2 !>
The second spec-mv-let bug was to allow the two lists of bound
variables to intersect. In the following example, given that spec-mv-let
is semantically just mv?-let, the result should have been 46, not 34.
This has been fixed. Thanks to David Rager for encouraging these two fixes
and checking them over.
ACL2 !>(set-ignore-ok t)
T
ACL2 !>(spec-mv-let
(x)
17
(mv?-let (x)
23
(if t
(+ x x)
"bad")))
34
ACL2 !>
The guard for function alpha-char-p was strengthened to require that
its argument is a standard character. The previous guard required only that
the argument is a character, and was a soundness bug; for a proof of nil
before this fix, see the comment about ``alpha-char-p'' in Community Books
file system/doc/acl2-doc.lisp, form (defxdoc note-7-0 ...).
Errors were possible when evaluating functions pkg-imports and
pkg-witness while including a book with a compiled (or expansion)
file. Such errors have been eliminated.
Fixed a bug in oracle-apply-raw.
(GCL CLtL1 only) Fixed a bug that was preventing set-debugger-enable from taking full effect in non-ANSI GCL.
(GCL only) The utility gc-verbose was broken, but has been
fixed.
Fixed a bug in provisional-certification that incorrectly caused an
error during the convert step for verify-guards+ forms. More
generally, this error occurred when encountering a make-event form
with a non-nil value supplied for the :expansion? keyword. Thanks
to David Rager for reporting this bug.
A raw Lisp error could occur with guard-checking turned off, because
type declarations were mistakenly left in the executable counterparts
(so-called ``*1* functions'') when ACL2 processed function definitions. The
following example shows how a type violation could occur in some Lisps (we saw
this in SBCL but not in CCL, for example).
(defun f (x)
(declare (xargs :guard (natp x)))
(let ((y (1+ x)))
(declare (type (integer 0 *) y))
y))
(set-guard-checking nil)
; Possible raw Lisp error:
; "The value -2 is not of type UNSIGNED-BYTE."
(f -3)
Thanks to Jared Davis for sending us an example that brought this bug to
our attention.
Fixed a bug that was causing a low-level assertion, saying:
``Implementation error: see 'replace-free-rw-cache-entry.'' Thanks to Anna
Slobodova for bringing this bug to our attention via an example, and to Sol
Swords for simplifying that example.
The iprint feature, which allows abbreviated output to be read back
in, did not work as one might expect when using the break-rewrite
feature (see brr). Thanks to David Rager for reporting this problem.
More generally: the problem was that values associated with iprint
indices during a wormhole, for example after breaking on a rewrite rule, were forgotten when exiting the wormhole. (Technical note for
those interested: the fix restores the main iprinting structure after exiting
a wormhole, just before reading the next top-level form. That restoration
uses raw Lisp, with logic-only code based on read-ACL2-oracle.) The
example below failed before the fix but now works.
(set-evisc-tuple (evisc-tuple 3 3 nil nil)
:iprint t
:sites :all)
(defthm my-rule (equal (car (cons x x)) x))
(brr t)
(monitor '(:rewrite my-rule) t)
(thm (equal (car (cons a a)) a) :hints (("Goal" :do-not '(preprocess))))
; Now entering a :brr break:
(make-list 10) ; printed without evisceration
; Set evisceration with iprinting:
(set-evisc-tuple (evisc-tuple 3 3 nil nil)
:iprint t
:sites :all)
(make-list 10) ; printed with evisceration
(a!) ; quit break-rewrite
; The following formerly caused a hard Lisp error, because although #@3#
; was printed in the output from (make-list 10) just above, iprint index 3
; was lost when exiting the break-rewrite wormhole. Now, this works
; because iprinting information from the wormhole is retained.
'#@3#
There was a bug in how so-called ``hidden packages'' were handled by encapsulate forms (see hidden-death-package), which was preventing
package axioms from being visible in certain contexts. (Technical remark:
packages that were hidden after the second pass but not the first were treated
as not-hidden, even though their package axioms were not introduced.) That,
in turn, could cause an include-book form to fail when the book
contains a deftheory-static form. Here is an example failure. First,
in a fresh ACL2 session evaluate the form (defpkg "FOO" nil) and then
evaluate the form (certify-book "foo" 1), where file foo.lisp is
as follows.
(in-package "ACL2")
(defun foo::foo (x) x)
(deftheory-static foo-theory
(current-theory :here))
Now evaluate the following sequence of forms. In previous versions of
ACL2, the final (include-book) form failed.
(encapsulate () (local (include-book "foo")) (defun h (x) x))
(encapsulate () (local (include-book "foo")) (defun h2 (x) x))
(include-book "foo") ; failed before the fix
We have cleaned up handling of interrupts and aborts when inside the break-rewrite loop, or indeed any wormhole. Thanks to David Russinoff
for bringing to our attention a case in which ACL2 quit a proof with
``Aborting due to an interrupt'' when in fact no interrupts had taken place.
Here is an example where that no longer happens but did, previously. (For a
different example, see the comment in the ACL2 sources definition of macro
bind-acl2-time-limit.)
(defun foo (x) (cons x x))
(brr t)
(monitor '(:definition foo) t)
(thm (equal (foo y) z))
(defun h (x) (declare (xargs :mode :program)) (car x))
; Raw Lisp error:
(h 3)
; Previously, unexpected proof abort "due to interrupt":
(thm (equal (append (append x y) x y) (append x y x y)))
When aborting with :a! inside the break-rewrite loop
from within the proof-builder, a raw Lisp error could subsequently
occur saying, ``Attempt to execute *wormhole-cleanup-form* twice!''. This has
been fixed. Thanks to Sol Swords for reporting a bug in our original fix.
Here is an example that formerly caused that behavior.
(defthm silly (implies (null x) (equal (append x y) y)))
(defconst *c* (make-list 10))
:brr t
:monitor (:rewrite silly) t
(verify (equal (append x (append *c* y)) (append y (append *c* x))))
bash
:go
:a!
bash ; formerly caused error
The utility redo-flat no longer worked when interrupting a
proof (with Control-c), due to a bug in Version 7.0. This has been fixed.
Thanks to Dave Greve for reporting this problem.
Changes at the System Level
As mentioned near the top of this documentation topic, default
builds of ACL2 are now hons-enabled.
(GCL only) GCL Versions prior to 2.6.12 are no longer supported.
Modified code used in distributing Debian releases that allows books
certified in one directory to be distributed in another. This change,
together with the fact that such relocation is not truly supported, is
explained in comments in source function make-certificate-file-relocated.
Thanks to Camm Maguire for discussions leading to this change.
(GCL only) Modified how home directory is calculated. Thanks to Camm
Maguire for help in making this change.
(SBCL only) Fixed a check done at build time that was preventing builds in
SBCL 1.2.2 because of its new backquote implementation. Thanks to Harsh Raju
Chamarthi and Pete Manolios for bringing this issue to our attention.
Development snapshots of ACL2 (and of the community-books) are now
available between releases from an ACL2
github repository; they are no longer available via svn. Thanks to David
Rager and Jared Davis for taking the lead on this conversion. As a result,
the banner printed at startup for those snapshots has changed slightly. For a
quick start guide for using git with ACL2, see git-quick-start.
(CCL only) Control-d now quits ACL2 in raw Lisp just as it has done for a
long time in the loop and, for ACL2(h) (i.e., hons-enabled ACL2), even
in raw Lisp.
(Should essentially affect GCL only) Significant re-work has been done for
function proclaiming, which is still only done when the host Lisp is GCL. In
particular, the build process now has extra steps even for other Lisps though
for them, the extra steps are trivial (technical details may be found in the
comment labeled ``Essay on Proclaiming'' in source file acl2-fns.lisp). We
now use GCL's automatic proclaiming mechanism to calculate function types
during the build (boot-strap), as we have seen it perform better than our own.
Thanks to Camm Maguire for helpful discussions, in particular for explaining
that mechanism and for pointing out that the re-proclaiming that had been done
previously during the build could lead to buggy behavior.
For Makefile targets for testing such as regression, the default ACL2
image used is now the same one that would be built for the same Makefile
variables. In particular, the command make regression is equivalent to
make regression ACL2_HONS=h, which uses the executable saved_acl2h,
not saved_acl2 as was formerly the case. Thanks to Harsh Raju Chamarthi
for finding a bug in a first attempt to make this change.
EMACS Support
Hons-enabled and Experimental Versions
(For hons-enabled executables only) Fixed a soundness bug related to
function memoization. For a proof of nil exploiting this bug in Version
6.5, see the comment about ``pons-addr-of-argument'' in Community Books file
system/doc/acl2-doc.lisp, form (defxdoc note-7-0 ...). Thanks
to Jared Davis for improving our original fix: by noting its applicability to
hons-clear (not just hons-wash); by tweaking our fix so that
it works even if a control-c interrupts (hons-clear or)
hons-wash; and later by finding another bug in source function
pons-addr-of-argument and suggesting a fix, which we incorporated.
(For hons-enabled executables only) Fixed a soundness bug due to the
fact that function never-memoize-fn returned nil in the logic but
returned t in raw Lisp. For a proof of nil exploiting this bug in
Version 6.5, see the comment about ``never-memoize-fn'' in Community Books
file system/doc/acl2-doc.lisp, form (defxdoc note-7-0 ...).
Static honsing for hons-enabled ACL2, an efficiency enhancement
formerly only available for CCL, is now incorporated into builds on
sufficiently recent GCL versions.
ACL2 executables that were hons-enabled could fail to use
previously-compiled definitions for memoized functions when include-book is invoked. This has been fixed.
(For hons-enabled executables only built on other than CCL or SBCL)
Calls of memoize only compile the memoized definition when the
original function is compiled, rather than unconditionally as before.
Several changes been made to function memoization (see memoize).
Here is a list of changes visible at the user level; for implementation
details, see note-7-0-memoize.
- It is now legal to call memoize on functions with special raw-Lisp
code (such as len) provided the value of the :inline keyword
argument is nil.
- Bug fix: Fixed bug that was making memsum attribute the count of
making of hash tables to ``Heap bytes allocated'' instead of to ``Number of
calls to mht.''
- Memoize keyword :trace is no longer supported, as the trace$
utility provides much more flexibility.
- Bug fix: Fixed a bug in handling of the :commutative argument of
memoize that could cause a hard Lisp error. For a book that exhibits
this bug, see the comment about ``:commutative'' in Community Books file
system/doc/acl2-doc.lisp, in the form (defxdoc note-7-0
...).
- When memoize is called with keyword argument :commutative
having value t, the benefit of that argument can apply to rational number
arguments even when not using static honsing. Moreover, now only one argument
needs to be a rational or to be ``static'' according to the
implementation (technically: to have an hl-staticp value).
- Bug fix: Calls of memoize with keyword argument :commutative
t were sometimes inappropriately treated as redundant redundant-events. This has been fixed. Here is a simple example of what
formerly went wrong.
(defn f (x y) (equal x y))
(memoize 'f :commutative t)
(unmemoize 'f)
(memoize 'f :commutative t) ; was redundant, so did not memoize
(For those who memoized directly in raw Lisp) Memoize-fn now requires
its first argument to be a defined (fboundp) function symbol. (It seemed odd
and needlessly arcane to allow memoize-fn to define an undefined
function.)
(For those who memoized directly in raw Lisp) Memoize-fn now causes
an error when it fails.
Bug fix: It had been possible to lose a memoization setting of :aokp
t when many functions were memoized. For an example, see the comment about
``rememoize-all'' in Community Books file system/doc/acl2-doc.lisp, in
the form (defxdoc note-7-0 ...).
We eliminated undocumented utilities memoize-on and memoize-off,
which were not used as far as we know.
When a memoized function call fails to satisfy the specified
condition, that call is no longer counted as a ``hit'', at least by
default. This can be changed with raw Lisp variable,
*condition-nil-as-hit*.
The utility memsum had reported one more pons call and (CCL only)
one more byte than was correct, and could perhaps report one call when there
were actually zero. That has all been fixed.
Bug fix: Some sorting of results based on ``self'' time and ``other
functions'' time had been wrong. (Technical remark: the problem was that the
implementation confused ``ticks'' with ``time''.) This has been fixed.
Statistics reporting (see memsum) often has a more uniform look.
It is now done with a right margin of 79 instead of 70. For memsum,
thanks to a suggestion from Warren Hunt, the defun formerly printed to
start each entry is now omitted, and after the name is printed at the start, a
newline is printed before the ``hits'' or ``hits/calls'' information is
printed. A related change: when *report-hits* and *report-calls*
are both nil, ``calls'' is no longer printed. Other cosmetic changes
were also made to memsum output.
The output from memsum on the line ``Time of all outermost calls''
no longer includes a percentage, which had been at best misleading and at
worst nonsensical. Suppose for example that f calls g, which does
all the work. Then memsum had reported 50% of the ``Time of all
outermost calls'' for each of f and g, even though 100% of the time
was spent under each.
On Mac OS (Darwin), the physical memory is now accurately computed
(using shell command ``sysctl hw.memsize'', which works in some versions of
Mac OS, maybe all recent ones; tested on 10.6 and 10.7). Before, the physical
memory value had been assumed to be 2^32 bytes. The physical memory value is
used in CCL for triggering garbage collections. (Technical remark: this is
implemented in function start-sol-gc.)
Bug fix: in the pons summary, misses had been reported instead of hits on
the ``hits/calls'' line.
Fixed memsum so that package names are printed with the symbols.
Also, printing is done with respect to the current package, not the
"ACL2" package.
It is now legal to profile functions that take state as an
argument. Thanks to Sol Swords for requesting this change. In the course of
making this change, we took a conservative approach and put the same
requirement regarding illegal memoization of functions involving user-defined
stobjs: that is, when memoization must have value nil for the
:condition keyword, it must also have value nil for the :inline
keyword. We can perhaps remove this additional restriction if necessary.
For every built-in memoized function defined in the ACL2 logic, the
memoization is done in the usual way (during the ACL2 build), using the memoize event during the ACL2 build. Such functions can thus be unmemoized by users in the usual way. Thanks to David Rager for requesting
this enhancement.
A new memoize keyword, :stats, can control whether statistics
will be saved for reporting with (memsum).
Memoization in hons-enabled ACL2(p) is no longer affected by calls
of set-waterfall-parallelism.
(ACL2(p) only, either hons-enabled or not) The function Cpu-core-count is now sensitive to environment variable ACL2_CORE_COUNT.
See cpu-core-count. Thanks to Jared Davis for requesting this
enhancement.
Support for multi-threading has been added for memoization. Thanks to
Jared Davis for contributing an initial implementation. Note that this may
slow down hons-enabled ACL2(p) by several percent on
memoization-intensive applications. Undocumented function
mf-multiprocessing is available for low-level system hackers to turn
on/off this feature, which by default is off for hons-enabled ACL2 and
on for hons-enabled ACL2(p).
(ACL2(p) only, either hons-enabled or not) We fixed a bug in pand, which we believe was also a bug in por, pargs, and
plet. (Technical remark: this bug had a low-level cause, pertaining to
maintenance of a Lisp variable, *ld-level*, that holds the number of
nested calls of ld.) Thanks to Jared Davis for reporting this bug and
to David Rager for assisting in its repair. Below is a slightly simplified
version of Jared's example, which formerly caused an assertion error but now
works as expected.
(defmacro pand* (x y)
`(spec-mv-let (yval)
,y
(mv?-let (xval)
,x
(if xval
yval
nil))))
(defn f3 (x)
(pand* x x))
(defn f4 (x)
(pand x
(f3 x)))
(value-triple (f4 5))
(Only for hons-enabled executables on Windows) Certain memory
management is avoided on Windows (technically: by avoiding a call of source
function start-sol-gc), where it was causing errors. Thanks to Harsh
Raju Chamarthi and Sol Swords for testing on Windows that led us to this
change.
Subtopics
- Note-7-0-memoize
- ACL2 Version 7.0 Notes on Changes to Memoization Implementation
- Note-7-0-books
- Release notes for the ACL2 Community Books for ACL2 7.0 (January
2015)
