Note-7-2
ACL2 Version 7.2 (January, 2016) 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 7.1 into the
following categories of changes: existing features, new features, heuristic
and 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.
See also note-7-2-books for a summary of changes made to the ACL2
Community Books since ACL2 7.1, including the build system.
Changes to Existing Features
The utility with-guard-checking is now limited to forms that do not
reference the ACL2 state. A related new utility, with-guard-checking-error-triple, may be used for forms that evaluate to
error-triples. For an example showing a bug when
with-guard-checking was applied to forms that access state, see
the comment about ``with-guard-checking'' in Community Books file
system/doc/acl2-doc.lisp, in the form (defxdoc note-7-2 ...).
We thank Jared Davis for sending us an example showing that our preliminary
fix was not adequate; for details, and for how a trust tag can avoid the new
restriction (at the potential cost of unsoundness), see the remark for
advanced users in the documentation for with-guard-checking.
Several built-in functions are now in :logic mode with guards verified: term-order, merge-sort-term-order, arity, termp, term-listp, and term-list-listp —
new functions arities-okp and plist-worldp-with-formals; and (thanks
to Eric Smith for the suggestions) collect-by-position,
make-lambda-application, >=-len, all->=-len, strip-cadrs,
and alist-to-doublets. (Technical note: This enhancement followed the
usual process: adding or extending community books in directory
books/system/, including any new such books in
books/system/top.lisp, and updating source constant
*system-verify-guards-alist*.)
Deprecated utilities clear-hash-tables and wash-memory have been
eliminated. For clear-hash-tables, you can get the same effect by first
invoking clear-memoize-tables, and then invoking either (hons-clear
t) or instead, if your executable uses static honsing, (hons-wash).
For wash-memory you can invoke (clear-memoize-tables) and then
(hons-wash). Thanks to Jared Davis for helpful discussions.
The commands :ubt and :ubu have been
changed. Their previous functionality is available with the commands
:ubt? and :ubu?, respectively. Now, :ubt and :ubu behave much more like :ubt! and
:ubu! (which have not been changed), in that they do not cause
queries; however, unlike :ubt! and :ubu!, the commands :ubt and :ubu do report errors. Thanks to
Eric Smith for requesting this change.
Now, :puff* has an optional argument that can avoid rollback
of the world when there is an error. See puff*.
After invoking :redef and redefining functions in a mutual-recursion event, it was necessary to answer Y repeatedly in order
to complete the redefinitions. A new option, Y!, will complete the
remaining such redefinitions without further query. Thanks to Eric Smith for
requesting this feature.
A harmless but somewhat annoying superfluous declaration (DECLARE (XARGS
:NON-EXECUTABLE T)) was, by default, included in the generated defun
for a defun-sk event. This has been fixed. Thanks to Eric Smith for
bringing this issue to our attention.
The proof-builder command show-rewrites (or sr; see ACL2-pc::show-rewrites) now shows additional bindings of free variables that
would be generated when a third argument of t is supplied for the
rewrite (or r; see ACL2-pc::rewrite) command. Thanks to Ben
Selfridge for noting that this information was missing. Note that we also
made a few trivial formatting changes for sr.
The redundancy check for encapsulate events has changed in
two small ways. One change is described below (see ``Redundancy checking for
encapsulate''). The other change is the redundancy check now properly
identifies a previous subsidiary make-event form with its expansion,
ignoring the record-expansion wrapper. See the example labeled
``Redundant after Version_7.1 (as of mid-September 2015)'' in community book
books/make-event/local-elided.lisp.
A new mechanism for controlling the checking for invariant-risk
replaces the raw Lisp global variable *ignore-invariant-risk*, which is
obsolete. See set-check-invariant-risk. In particular, the default is
now to print a (new) warning when encountering potential slowdown due to
invariant-risk. Note that more functions are now subject to the
invariant-risk check; see the discussion below in the section on Bug Fixes
that pertains to invariant-risk.
The (undocumented) system utility with-ubt!, which continues to be
used in trace! and disassemble$ and is now also used in set-check-invariant-risk, now binds ld special ld-pre-eval-print to nil. Thus, when with-ubt! is invoked,
subsidiary forms will not be printed to the screen even when the above LD
special is non-nil.
Formerly, certify-book, include-book, and puff
operated with guard-checking off; technically, with state global
guard-checking-on bound to nil. Now, that value is bound to t,
which matches the default value in the top-level loop. Thanks to Eric Smith
for suggesting this change to certify-book and to Jared Davis for a
helpful conversation about it.
For guard proof obligations, all conjuncts from stobj
declarations (supplied as :stobjs keywords in xargs declarations)
preceded all other conjuncts (i.e., from type declarations or xargs :guard declarations). Previously, this was only true within a
given declare form. Thanks to Dave Greve for bringing this issue to
our attention.
A new runic abbreviation has been added: :r, which abbreviates
:rewrite. For example, you may use (:r app-assoc) in a theory
expression to denote the rune (:rewrite app-assoc). See theories.
It is now possible to monitor rules by supplying a symbol or other
runic designator other than a theory (see theories), thus relaxing the
previous requirement that a rune is supplied. For example, the form
:monitor nth t is legal, as is :monitor (:d nth) t, where before the
corresponding command would necessarily have been :monitor (:definition
nth) t. Thanks to Eric Smith for requesting this enhancement.
Suitable warnings are now printed when attempting to monitor
simple rules of class :definition. These had only been
printed for simple rules of class :rewrite, because of potential
inefficiency in computing for such warnings in the case of large mutual-recursion events, but that problem has been addressed in the
ACL2 source code using fast-alists.
ACL2 sometimes produces smaller .cert files, by avoiding certain
macroexpansion. Formerly, for each macro call encountered in a certification
world or make-event expansion, ACL2 performed repeated single-step
macroexpansion until an event form was obtained, and replaced the original
form with that result. The reason for this replacement was to modify certain
include-book forms involving relative pathnames (though only under
specific conditions). Now, no such replacement is made except when such a
modification is made to an include-book call. This change could result
in smaller certificate (.cert) files; for example, if a portcullis command is a macro call, (foo), that expands into a
very large defun or defthm event, the certificate file will
contain (foo) rather than its macroexpansion. Of course, this change
could result in longer times for processing an include-book forms,
because now macroexpansion may need to be done when they are processed; but
such macroexpansion has always been necessary for all forms within a
book, so such behavior is at least more consistent than before. If you really
want a portcullis macro call to be expanded, wrap it in a make-event
call, for example, (make-event '(foo)) instead of (foo).
The macros defund and defthmd now produce less output. In
fact, the output is the same as for defun and defthm,
respectively, except for the printing of the return value, which (as before)
looks like (:DEFUND NAME) or (:DEFTHMD NAME). Thanks to Jared Davis
for suggesting such a change.
Remaining traces of legacy documentation have generally been eliminated,
including all vestiges of the obsolete command, defdoc. (Documentation is now generally provided through the xdoc system.) In
particular, optional and keyword arguments, doc, have been eliminated for
the following macros.
Note that defabbrev, defconst, defmacro, defpkg, and defun may still be supplied documentation strings, as a
nod to Common Lisp. In particular, for defun and defmacro this can
ease the porting of Common Lisp code to ACL2.
Several source-level definitions have changed, many of them unadvertised.
Some are for unadvertised event commands like defthm-fn, which no longer
have a doc argument (see ``traces of legacy documentation have generally
been eliminated'' above). Others, like flambda-applicationp, are macros
that were formerly defined with defabbrev but now are defined with
defmacro; thanks to Eric Smith for suggesting such
simplifications.
In prover output, terms of the form (not (not expr)) had been printed
simply as expr. That could cause confusion; for example, the following
form would lead to the checkpoint (EQUAL (ALISTP X) (ALISTP X)), where
actually the checkpoint was (EQUAL (NOT (NOT (ALISTP X))) (ALISTP X)).
This ``feature'' has been eliminated. Thanks to Shilpi Goel for bringing this
issue to our attention and supplying an illustrative example.
A warning was formerly printed when encountering a macro call with
duplicate keys, for example (foo 3 :y 4 :y 5) where :y is a keyword
argument of the macro, foo. Now, this is an error by default, in order
to make it easier for users to catch bugs due to accidental repetition of a
keyword argument. However, the utility set-duplicate-keys-action can
be used to allow such duplicate keys, with or without a warning. Thanks to
Jared Davis for requesting these changes.
Warnings are no longer printed for :use hints applied to functional
instances of enabled rules. Thanks to Eric Smith for suggesting this
change.
The second (optional) argument of show-accumulated-persistence may now
have a new value, :list, which causes the results to be displayed as a
single list with entries of the form (frames tries xrune). Thanks to
David Rager for requesting a way to display useless runes, sorted in a
manner that can help with automating the creation of in-theory forms that
disable unnecessary runes; also thanks for his
helpful discussions in designing its functionality. See accumulated-persistence; in particular, (show-accumulated-persistence
:useless :list) can display a list of runes to consider disabling.
The utility print-gv now takes additional keyword arguments,
:conjunct and :substitute, which respectively show a specific
conjunct of the guard evaluation that produced nil, and avoid
flet in favor of substituting actuals (even at the risk of
duplication). See print-gv, and see set-print-gv-defaults for a
utility that sets default values for the keyword arguments. Thanks to Eric
Smith for requesting these enhancements and for helpful discussions. Note
that the system default value for the :evisc-tuple keyword is now the
value of the form (print-gv-evisc-tuple).
State global variable global-enabled-structure is now
untouchable (see remove-untouchable).
Users may see a change in the order, number, and size of termination proof
obligations because of an optimization that removes trivial equality tests
generated by case and cond statements. (The removal of the
tests can affect subsumption, which is how the order and number of proof
obligations may change.)
Once again, all documented constant, function, and macro symbols in the
"ACL2" package are included in the constant, *ACL2-exports*.
Community book books/misc/check-acl2-exports.lisp has been updated for
the current documentation system to enforce this invariant in the future.
Thanks to Jared Davis for pointing out that the symbol extend-pe-table
was missing from *acl2-exports* and would be a good addition; that led us
to this change. As also suggested by Jared, we added the symbols exists and forall to *acl2-exports*, as well.
The quantifier forall or exists used in the body of a
defun-sk call must now be in the "ACL2" package. Many users
will not notice this change, since the symbols forall and exists in
the "ACL2" package are now in the list *ACL2-exports*; see the
paragraph just above. Thanks to Alessandro Coglio for a remark leading to
this change.
Definitions are no longer redundant that have different values specified
for their xargs keyword, :normalize. (See redundant-events.) Although we are not aware of a need to make this change,
this change eliminates a possible unsoundness.
It is now the case that open-output-channel and
open-output-channel! will attempt to create missing directories as
needed. (This had formerly been observed to be the case in CCL but not other
Lisp implementations.) Thanks to Jared Davis for requesting this
enhancement.
New Features
It is now possible to make ACL2 avoid the well-formedness checks done when
metafunctions and clause processors are run. By default, when a metafunction
or clause processor is run, ACL2 calls termp or term-list-listp, respectively, on the new value to make sure it is
well-formed. Now, if you prove and provide a :well-formedness-guarantee with the :meta or :clause-processor
rule-class, you can skip these checks. This can speed up the use of
metafunctions and clause processors on big terms and formulas.
It is now possible to ensure the integrity of statistics produced by memsum after functions are memoized. See protect-memoize-statistics. Thanks to Alessandro Coglio for noticing
oddities in those statistics and to Jared Davis for providing an
implementation of this new feature.
Function read-file-into-string provides an efficient way to return
the contents of a file as a string, without returning an ACL2 state.
Thanks to Jared Davis for pointing out a logical flaw in the initial
implementation.
A new function, get-skipped-proofs-p, can tell system programmers
whether or not a given event name was introduced with proofs skipped, as with
skip-proofs or using set-ld-skip-proofsp. See system-utilities. Thanks to Eric Smith for requesting such a capability.
A new table permits the association of names with substitute event
forms, for use by history commands that print event forms, including
:pe, :pc, :pcb, and :pcb!.
See extend-pe-table. Thanks to Eric Smith for requesting such a
capability. Note that :pe! now avoids use of this table.
A new macro, ffn-symb-p, has been introduced and then used in the
source code to simplify some definitions. Thanks to Jared Davis for a remark
that led us to define and introduce this macro. See system-utilities
for a description of this and many other low-level system utilities.
It is now possible to give hints that specify the use of termination
or guard theorems for existing function symbols. See lemma-instance, termination-theorem-example, and guard-theorem-example. Also see gthm and tthm for related
query utilities. Thanks to Alessandro Coglio and Eric Smith for requesting
these features.
See set-print-gv-defaults for a new utility for setting default
values for the keyword arguments of print-gv. Thanks to Eric Smith
for requesting this feature and for helpful discussions.
For history commands and the function disabledp, the notion
of ``disabled'' is now computed inside the break-rewrite loop
with respect to the enabled status at the current point of the current
proof attempt, rather than with respect to the global state. Thanks to David
Rager for suggesting this enhancement. Note that this change only affects
history commands and disabledp, not other utilities (for example
tau-status and guard-obligation).x
New system utility getpropc is a convenient abbreviation for getprop.
A new utility causes some warnings to be printed in a ``raw'' s-expression
format. See set-raw-warning-format. Thanks to Shilpi Goel for
requesting this utility.
The macro accumulated-persistence-oops undoes the effect of
accidentally clearing statistics with (accumulated-persistence t) or
(accumulated-persistence :all). See accumulated-persistence.
Thanks to Jared Davis for requesting this feature.
Heuristic and Efficiency Improvements
The redundancy check for defconst has been sped up in cases with a
very large term, as in the following example. Thanks to David Rager and Jared
Davis for helpful related discussions.
(defun make-tree (n)
(declare (type (integer 0 *) n))
(if (zp n)
nil
(let ((x (make-tree (1- n))))
(cons x x))))
(make-event
`(defconst *a* (hons-copy ',(make-tree 50))))
; Redundant, and formerly very slow:
(make-event
`(defconst *a* (hons-copy ',(make-tree 50))))
Processing of defpkg forms may be faster, thanks to a change
suggested by Jared Davis (who observed significant speedup in SBCL).
Optimizations have been made that can speed up include-book
for some large books, as follows. In particular, for the form (time$
(include-book "centaur/sv/tutorial/alu" :dir :system)) we have seen a 25%
reduction (on Mac OS) for the first item below, and an additional 29%
reduction (also on Mac OS) for the second item.
- Various optimizations have been made for theory manipulation,
including some to make processing more efficient for defund and defthmd. Thanks to Sol Swords for bringing this issue to our attention in
GitHub Issue #401 and for reporting bugs in our initial implementations.
- Redundancy checking for encapsulate events can be much
faster. The only functional change (with one small exception, described in an
item above) is to check for a sub-event of the proposed encapsulate event
that is attempting to introduce a new name; if no such name is found, then the
redundancy check is skipped, and the proposed encapsulate event is
evaluated. This new check is quite thorough (see redundant-encapsulate), so we expect it to be rare that an encapsulate
event that was formerly redundant is no longer redundant.
Certify-book is faster in some cases; for example, we found the
time required to certify a book whose only event is (include-book
"centaur/gl/gl" :dir :system) was reduced from 57 seconds to 10 seconds.
(Implementation note: The change was to avoid installing worlds in function
defpkg-items. That had probably been done in order to speed up calls of
simple-translate-and-eval in defpkg-items-rec, but that speed-up
seems to be dwarfed by the expense of extend-world1 in such cases.)
We tweaked a part of the so-called ``clausify'' process for doing Boolean
simplification towards producing subgoals of a given goal, namely, the
so-called ``subsumption-replacement-loop'' (specifically, source function
find-subsumer-replacement). Thanks to Jared Davis for helpful
discussions that led us to make this change.
Defevaluator is faster, especially so when many functions are to be
interpreted by the new evaluator. The new version is a refactored version of
community book books/tools/defevaluator-fast.lisp used with the
permission of its original authors Sol Swords and Jared Davis. Thanks!
The Common Lisp code generated for stobj accessors and updaters has
been improved in the case that the :type is T or of the form
(array T ...). In particular, we have seen efficiency improvements for
host Lisp CCL when the value read from or written to the array is a
fixnum (integers that are sufficiently small in absolute value). Thanks to
Bob Boyer and Gary Byers for helpful discussions that led to this
improvement.
Bug Fixes
We fixed a soundness bug pertaining to local defpkg events. See community books directory misc/hidden-defpkg-checks/ for an
example that exploits this bug to prove nil in Version 7.1 and perhaps
some other previous ACL2 versions. Thanks to Sol Swords for helping us set up
that test (specifically, suggesting addition of the comment ``; no_port''
after an include-book call that is not to be put into a .port
file).
The use of set-deferred-ttag-notes during make-event
expansion could cause some TTAG NOTE messages never to be printed. Thanks to
Jared Davis for a remark that led us to discover this bug, which could be
considered a soundness bug since the TTAG NOTE mechanism is a key part of the
soundness story. With this change, the effects of
set-deferred-ttag-notes persist past make-event expansion.
It was possible to use :program mode functions to write past
the end of an array, leading to unsoundness. This has been fixed. Now,
updaters for stobj array fields are marked as having so-called
``invariant-risk'', even when the element type of the array is
t (unconstrained). Also marked with invariant-risk are built-in
functions aset1 and aset2. See program-wrapper, invariant-risk and set-check-invariant-risk, which is discussed above
in the section Changes to Existing Features. Thanks to Jared Davis and Sol
Swords for sending an example to illustrate the bug.
When ACL2 was interrupted while debugging was on (see set-debugger-enable), it was possible later to get the following error
repeatedly:
HARD ACL2 ERROR in TIME-TRACKER: It is illegal to specify :START for
tag :TAU, because tracking for this tag is already in an active state.
This problem has been fixed, by defining a new keyword argument for time-tracker, :start!, and using it to track the use of the tau-system; see time-tracker and time-tracker-tau.
ACL2 would cause an error at startup when the value of environment variable
ACL2_SYSTEM_BOOKS was a string starting with the tilde
character (~). This has been fixed. Thanks to Shilpi Goel and Warren
Hunt for bringing this bug to our attention.
(GCL only) It had not been possible to define a stobj with more than
64 fields in GCL. We have removed that restriction. (Technical note: GCL
disallows calls of the function, vector, with more than 64 arguments. So
instead we now build a list of stobj fields that is coerced to a vector,
rather than calling vector directly.)
Fixed deftheory-static by declaring the world to be
ignorable, thus avoiding errors for forms that don't reference the
world. Thanks to Jared Davis for pointing out this bug with the example,
(deftheory-static my-theory '(car-cons)).
Fixed a bug that was causing the hiding-cars component of the ld-evisc-tuple to be ignored when printing evaluation results.
We avoid an error in the case that skip-proofs is used around a
definition with no tests above a recursive call, as in the following
example.
(skip-proofs (defun foo (x)
(declare (xargs :measure (acl2-count x)))
(identity
(cond ((zp x) 17)
(t (foo (1- x)))))))
Thanks to Dave Greve for bringing this bug to our attention. Note that
such a definitional event may be unsound (not surprisingly, because of the use
of skip-proofs). For example, the following form succeeds:
(thm nil :hints (("Goal" :induct (foo x)))).
Several improvements have been made to avoid errors in the execution of
:puff and :puff*. Thanks to Eric Smith for
reporting this issue. (Technical implementation note: a bug in source
function find-longest-common-retraction1-event, used in reverting logical
worlds, was fixed in support of this work.)
When the default-defun-mode was :logic, then a mutual-recursion form with xargs declaration of :program
mode, which also had one or more defund events, would cause a
error when attempting to disable new function symbols after admitting
their definitions. This has been fixed. Thanks to Jared Davis for bringing
this bug to our attention (GitHub Issue #464).
We fixed some printing bugs for :psof, :pso, and
raw proof format (see set-raw-proof-format). Both :psof
and :pso were printing explicit splitter notes (see splitter) — and worse yet, and thanks to David Rager for pointing this
out, :psof was printing them to the terminal. Those explicit
splitter notes were not appropriate during proof replay, where instead
parenthetical phrases like ``(if-intro)'' are sufficient; those phrases
continue to be printed during proof replay, just as when gag-mode is
off. Raw proof format had a couple of whitespace bugs, but more important was
its failure to indicate any information about splitters; so now it prints the
same explicit splitter notes as are printed for gag-mode.
Insufficient checking has been fixed for signatures. Thanks to
Jared Davis for sending the example ((f * *) => * :formals (x) :guard (natp
x)), which was not flagged as illegal by ACL2 even though the specified
arity of 2 did not match the length of the specified :formals. There
could also be mismatches between the stobjs specified, for example,
with (((f * st1) => * :formals (x st2) :guard (natp x))), that were not
flagged as illegal.
The inclusion of uncertified books was leading to some incorrect messages
about other books that are also uncertified. This has been fixed (though the
messages can still be verbose at times). Thanks to Eric Smith for sending an
example to bring this problem to our attention.
There were some incorrect error messages produced for bad calls of ec-call; these have been fixed.
Fixed a bug in memoization that could occur when multiprocessing is
turned on, as in the call (acl2::mf-multiprocessing t) in community book
books/centaur/vl/server/server-raw.lsp. Thanks to Sol Swords for
reporting a bad report from memsum when profiling function
include-book-fn before including system book "doc/top".
Guard violation error messages printed 'ACL2_INVISIBLE::|The
Live State Itself| where they should have printed STATE; similarly for
the utility print-gv, which also failed to print entirely in
user-level ``untranslated'' syntax. These problems have been fixed. Thanks
to Eric Smith for bringing the ``STATE'' bug to our attention.
Infinite loops occurred for calls of (close-output-channel *standard-co*
state) after redirecting standard output using set-standard-co. A
clean error now occurs instead.
We fixed a bug in state-global-let* — actually, in its
supporting system utility acl2-unwind-protect — that allowed
capture of a lexical variable, temp, to produce bad results, for example
as follows.
(defun foo (temp state)
(declare (xargs :stobjs state :mode :program))
(state-global-let*
((x 3))
(pprogn
(fms "TEMP = ~x0~%X = ~x1~%" (list (cons #0 temp) (cons #1 (@ x)))
*standard-co* state nil)
(value nil))))
(foo 17 state) ; should show TEMP = 17 and X = 3, but caused Lisp error
ACL2 no longer prints a message for a failed :induct hint (in the case
that gag-mode is off), saying that a definition is disabled when
that is not the case.
(CCL only, probably only 32-bit CCL) We fixed a bug manifested with an
error, ``is not of the expected type (UNSIGNED-BYTE 32).'' (Technical note:
Function ccl::set-lisp-heap-gc-threshold requires a fixnum, but was
passed a bignum.) Thanks to Harsh Raju Chamarthi for sending us a log that
exhibited this bug, namely
books/oracle/stv-invariant-extraction-pitfall/alu.lisp, which seems to
have evoked the bug by using an unusually large amount of memory.
One might reasonably expect that for a rewrite or linear rule
with a hypothesis of the form (force ...) or (case-split ...), an
attempt to relieve that hypothesis should be successful when forcing is
enabled. The situation is a bit tricky if the hypothesis has free variables,
but even then, one would expect success if the :match-free value is the
default, :all, or if no suitable bindings are found. Such attempts had
however not always been successful; but they are now, and the relevant
documentation on free-variables has been clarified. For an example
exhibiting the bug, see the comment about ``free variables'' in Community
Books file system/doc/acl2-doc.lisp, in the form (defxdoc note-7-2
...).
An inappropriate warning has been eliminated for some type-prescription rules, for example the following.
(defthm foo
(implies (alistp mem)
(or (equal (assoc loc mem) nil)
(consp (assoc loc mem))))
:rule-classes :type-prescription)
The warning had claimed that the rule ``may be weaker than you expect''
because the theorem itself ``is not provable using type-set reasoning''. But
the theorem is provable when guard-holders are removed, as could
generally be expected; so now, the check is applied after removing
guard-holders from the theorem.
The guards stored for macros now include type
declarations. Formerly the guards stored for macros were based only on the
:xargs :guard keyword. Consider for example the following
definition.
(defmacro foo (x)
(declare (type integer x))
x)
(defun bar (y)
(foo y))
Formerly, no error occurred when processing the definition of bar,
because the guard stored for foo was t. Now, the guard stored for
foo is (integerp x); since the variable y is not an integer (it
is a symbol), the attempted defun for bar causes an error.
Changes at the System Level
ACL2 is now defined to incorporate its hons-enabled features. We
formerly supported building ACL2 without these features, resulting in
so-called Classic ACL2, also called ``ACL2(c)''. Such builds are no longer
supported: although it is still technically possible to build ACL2(c), we do
not stand behind such builds; in particular, we do not test them, and we have
removed the GNUmakefile target, saved_acl2c.
(CCL only) Starting with CCL Version 16384, EGC (the ephemeral garbage
collector) is enabled in ACL2 by default, in place of a ``start-sol-gc''
memory management scheme, but with some of the delay in full garbage
collection that had been provided by that scheme. That scheme is still
available to users, under a different name and inside the ACL2 loop; see set-gc-strategy. (Note that both set-gc-strategy and gc-strategy
have been added to *ACL2-exports*.) Thanks to Gary Byers for CCL
improvements leading to this change, and to him, Bob Boyer, Jared Davis, and
Sol Swords for helpful discussions. The default behavior can be restored to
the previous behavior at ACL2 build time, by setting Make variable
ACL2_EGC_ON=nil when building an ACL2 executable.
A new mechanism allows importing of theorems into the ACL2 source code,
thus extending the existing mechanism for importing termination and guard
verification for system functions (see the item above about term-order, merge-sort-term-order, and so on). Using this mechanism,
some theorems have been imported from a new community book,
books/system/termp.lisp. (For an example of how ACL2 developers use this
mechanism, see the call of system-events in ACL2 source file
boot-strap-pass-2.lisp.)
File GNUmakefile in the (top-level) ACL2 sources directory now sets
environment variable TIME_CERT so that regressions will generate timing
information.
(SBCL only) The --control-stack-size argument for ACL2 executables
saved for SBCL is now 64 (formerly 16). Thanks to Jared Davis for requesting
this increase.
The existing utility get-event-data is now documented. Moreover,
it can be used for determining whether an interrupt (Control-C) occurred
during execution of an event. (This capability is used in a new utility,
removable-runes.) See get-event-data.
The startup banner now shows the git commit hash for development
snapshots. Thanks to Bob Boyer for suggesting such a modification and to
Jared Davis for bringing to our attention the appropriate git command for
retrieving the hash.
(CMUCL only) It is now the case for CMUCL that setenv$ modifies the
environment of the underlying Lisp process. Thanks to Jared Davis for this
suggestion, and for pointing out that CCL and SBCL [at least] already have
this behavior.
A new optimize declaration for defun, (:stack-access 3), can
result in some speed up for evaluations done when the host Lisp is CCL (but is
likely to be a no-op in other host Lisps). Thus, you may write: (defun
foo (x) (declare (optimize (:stack-access 3))) ...). Thanks to Gary Byers
and the CCL team for their excellent compiler work, including the new
stack-access feature, and to Bob Boyer and Warren Hunt for helpful
discussions. To build ACL2 on CCL with this feature, add the variable setting
ACL2_STACK_ACCESS=3 to the make command that you invoke to build
ACL2. NOTE: The use of ACL2_STACK_ACCESS relies on recognition by CCL of the
:stack-access keyword for optimize expressions, hence will only have
effect for CCL versions starting with 16678.
(CMUCL only) Updated saved_acl2 for CMUCL to use maximum heap for CMU
Common Lisp snapshot-2016-01 and beyond. Thanks to Raymond Toy for updating
CMUCL such that one can specify with -dynamic-space-size 0 that the
maximum heap is used.
EMACS Support
We made several improvements in the ACL2-doc browser.
- A bug has been fixed in the S command (acl2-doc-re-search).
- The help message is displayed more often (but only, we think, when
appropriate) in the echo area (i.e., below the mode line).
- The q command (acl2-doc-quit) now can be run from any buffer in
acl2-doc mode, for example after typing the H command. Moreover,
all such buffers will be buried after q; formerly, if you quit from the
main acl2-doc buffer you could have been left in the
acl2-doc-history buffer.
Verify-termination calls are now indented like defun calls.
Thanks to Alessandro Coglio for suggesting this change to
emacs/emacs-acl2.el.
The ACL2-doc Emacs browser now allows handling of topics with square
brackets. This fix was necessary because a new topic, SV::4VEC-[=,
broke acl2-doc; it wouldn't initialize. The fix simply replaces characters
#\[ and #\] with #\< and #\>, respectively. It's not
a perfect fix, but it seems awkward to try to escape #\[ (which Emacs
Lisp thinks starts a vector). See community book
system/doc/render-doc-base.lisp.
Experimental Versions
Fixed some interleaved output that could appear with waterfall-parallelism enabled. Thanks to Eric Smith for reporting this
problem and to David Rager for a helpful chat.
Subtopics
- Note-7-2-books
- Release notes for the ACL2 Community Books for ACL2 7.2 (Jan 2016)
