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 6.1 into the following categories of changes: existing features, new features, heuristic 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.
CHANGES TO EXISTING FEATURES
top-level has been changed, so that evaluation of a form
(top-level x) results in an error when evaluation of
x results in an
error. Thanks to Jared Davis for observing that when evaluating a file using
ld, an interrupt of a call of a
top-level call in that file would
not prevent evaluation of later forms in the file.
THE no longer causes an error when guard-checking is
:NONE. For example, it had been the case that evaluation of
(the integer t) always caused an error; but now, there is no error after
:NONE. Thanks to Jared
Davis for asking for a way to avoid such errors.
The error printed when attempting to ``reincarnate'' a package -- that is,
to define a package that is not part of the ACL2 logical world but
exists in raw Lisp because it was once part of the world -- is now much
more instructive. In particular, it shows pathnames for the previous and
defpkg events, and it shows the symbols that are imported by
one but not the other. Thanks to Jared Davis for requesting this
open-output-channel no longer
cause an error when failing to open a channel because of a permissions
problem, but instead return
(mv nil state). Thanks to Jared Davis for
requesting this change. (Note: this change does not apply if the host Lisp
is non-ANSI, i.e., if the host Lisp is non-ANSI GCL.)
The advanced meta-extract mechanisms, provided for using facts from the world or metafunction context, have been enhanced in the following ways, in collaboration with Sol Swords. See meta-extract for more details.
It is now permissible to use calls of
meta-extract-global-factin hypotheses of
clause-processorrules, much as they are used in hypotheses of
metarules. See meta-extract. Thanks to Sol Swords for requesting this feature.
meta-extract-global-factis now a macro, which expands to a corresponding call of the new function,
meta-extract-global-fact+. This new function takes an alternate, extra state as an argument; it is not to be executed, and it operates on the alternate state, whose logical world is intended to be the same as that of the ``live'' (usual) state.
A new sort of value for the
objargument is supported for
meta-extract-global-fact+), which results in a term equating a function application to its result. See meta-extract, in particular the discussion of
It is now possible for
trace$ to avoid printing prefixes of the form
"n> " and
"<n ", while also (optionally) avoiding indentation.
See trace$, in particular the discussion of
:fmt!. Thanks to Shilpi Goel
for requesting this feature.
It was possible for the guard-debug feature to generate duplicate calls
extra-info in hypotheses generated for guard verification. We have
eliminated duplicates of this sort.
in-theory returns without error, it returns a value
(:NUMBER-OF-ENABLED-RUNES k), where
k is the length of the new
current theory. (Formerly,
k was returned.) This value is thus printed
in-theory event is submitted at the top level. Thanks to Gisela
Rossi for feedback that led us to make this change.
A new keyword parameter for
default value is
nil, which causes an error, as before, upon failure to
open a specified file. Other legal values are
see ld-missing-input-ok and see ld.
*acl2-exports*, in particular adding
SIGNED-BYTE-P (thanks to a suggestion by Jared Davis)
Even if the function
f is defined to take one or more stobj
arguments, the form
(ec-call (f ...)) is now legal if all arguments of
the call of
f are non-stobj objects, in any context where only ordinary
object return values are expected.
When the second argument of
certify-book is a symbol, that symbol
formerly needed to be
t, in the
"ACL2" package. Now, the
symbol-package-name of the second argument is ignored: any symbol whose
"T" is treated the same in that
argument position as the symbol
t in the
respectively. Thanks to Warren Hunt and Nathan Wetzler for suggesting
consideration of a more relaxed criterion for that second argument.
(For system hackers, not standard ACL2 users:) Utilities
finalize-event-user now each take a
list of three arguments,
(ctx body state). Thanks to Harsh Raju
Chamarthi for requesting this change.
It is now permissible to specify a stobj field that is itself either a
stobj or an array of stobjs. A new primitive,
stobj-let, is provided
in order to access or update such fields; see stobj-let. Thanks to Warren
Hunt and Sol Swords for requesting the ability to specify nested stobjs.
New accessor function
(mfc-world mfc) returns the world component of a
metafunction context. See extended-metafunctions.
:SPLIT-TYPES, can be used to ``split'' the
type declarations from the guard in the following sense. By
default, or when
:SPLIT-TYPES has value
nil, one gets the existing
behavior: the terms corresponding to type declarations are conjoined into the
guard. However, if
:SPLIT-TYPES t is specified, then that is not the
case; instead, guard verification will require that these terms are proved
under the hypothesis that the guard holds. In this way, one can add type
declarations to assist the host Lisp compiler without cluttering the
function's guard. See xargs. Thanks to Jared Davis for requesting this
Advanced users may want to see quick-and-dirty-subsumption-replacement-step for a way to turn off a prover heuristic. Thanks to those who have mentioned to us potential issues with this heuristic, most recently Dave Greve.
We made changes to the ``ancestors check'' heuristic (source function
ancestors-check-builtin), as follows.
The heuristic could prevent a rewrite rule's hypothesis from being rewritten to true, even when that hypothesis is of the form
(force <term>). Now, forcing will take place as expected; see force. Thanks to Robert Krug for bringing this issue to our attention and sending an example, which we include as a comment in the ACL2 source code (see
(deflabel note-6-2 ...)).
The heuristic is now delayed until after we check whether the hypothesis is already known, using type-set reasoning alone (in particular, not using rewriting), to be true or to be false. We believe that this is now the ``right'' order for those two operations. We saw a slight speed up in the regression tests (about a percent) with this change, but that might be in the noise.
A technical change makes the heuristic slightly less aggressive in preventing backchaining. Roughly speaking, ordering checks based on function symbol counts could suffice to permit backchaining, where now variable counts also suffice. Thanks to Robert Krug for showing us an example where backchaining led to a term with no free variables that was nevertheless subject to the ancestors check, preventing it from being rewritten.
(For those who use
defattachto attach to
ancestors-check) We have used
defrecto introduce an `
ancestor' data structure. A new function,
strip-ancestor-literals, should be used to obtain the literals from a list of ancestors, although
strip-carswill still work at this time.
When we rewrite the current literal of the current clause we assume the falsity of the other literals and of the conclusions produced by forward chaining. We have changed the order in which those assumptions are made, which affects the type-alist used during rewriting. This has three effects: the new type-alist, which is sometimes stronger than the old one, may allow additional rules to fire, the choice of free vars may be different, and the order of the literals in forced subgoals may be different. Should ``legacy'' proofs fail under the new type-alist, we recommend looking for rules that are fired in the new proof that were not fired (on that same subgoal) in the old one. Thanks to Dave Greve for sending us an example that led us to make this change.
We fixed a soundness bug that could be exploited by calling system functions
acl2-magic-canonical-pathname. Thanks to Sol
Swords for bringing this bug to our attention.
We fixed a soundness bug in the handling of stobjs, in which strings
were recognized as stobjs in raw Lisp. Thanks to Jared Davis for sending us
a proof of
nil that exploited this bug. We now have a much simpler
example of this bug, as follows.
(defstobj st fld) (defthm bad (stp "abc") :rule-classes nil) (defthm contradiction nil :hints (("Goal" :in-theory (disable (stp)) :use bad)) :rule-classes nil)
We fixed bugs in extended metafunctions (see extended-metafunctions). The
mfc-ap no longer takes a
:TTREEP keyword argument, because this
argument could allow returning a tag tree that does not properly account for
forcing. The remaining
mfc-xx macros --
mfc-ts -- still take a
argument, but the corresponding functions when
mfc-ts-ttree -- were introduced with incorrect output signatures. A
complication is that
mfc-relieve-hyp-ttree was improperly defined in raw
Lisp in a way that actually matched the incorrect signature! All of these
bugs have been fixed. Perhaps any of them could have made it possible to
nil, though we have not tried to do so.
(Windows only) On Windows, it had been possible for ACL2 not to consider two
pathnames to name the same file when the only difference is the case of the
drive, e.g., `
C:' vs. `
c:'. This has been fixed. Thanks to Sol
Swords for reporting this issue.
Fixed a bug in the storing of rules for the tau system; see tau-system. (The error message mentions PARTITION-SIGNATURE-HYPS-INTO-TAU-ALIST-AND-OTHERS.) Thanks to Sol Swords for reporting this bug and sending a simple example to illustrate it.
It had been possible to admit the missing
defthm events printed by
defabsstobj, and yet get an error when subsequently submitting the same
defabsstobj event, stating: ``Note discrepancy with existing formula''.
The problem could occur when an expression of the form
(or X Y) occurred
in one of those missing events, because ACL2 created it from the term
(if X 't Y) but then translated
(or X Y) to
(if X X Y), resulting
in a mismatch. This has been fixed. Thanks to Jared Davis for reporting
this bug using a simple example.
A hard Lisp error was possible for certain illegal functional substitutions (see lemma-instance). Thanks to Sol Swords for reporting this bug.
We fixed a bug in the case that an exported function of a
event had a guard of
t. Thanks to Jared Davis for sending a simple
example when reporting this bug.
We now avoid an infinite loop that could occur when attempting to close the standard character output channel (see standard-co). Instead, an error message explains how to accomplish what was probably intended. Thanks to Shilpi Goel for bringing this issue to our attention.
(Windows only) Fixed a bug that was causing a hard error on Windows when ACL2
encountered filenames starting with the tilde character (
(ld "~/acl2-customization.lsp"). Thanks to Sol Swords for
bringing this bug to our attention. Also thanks to Harsh Raju Chamarthi for
a useful conversation that led to a better fix than our first one.
CHANGES AT THE SYSTEM LEVEL
ACL2 may now be built on recent versions of a new host Lisp, ANSI Gnu Common Lisp (GCL). Traditional (non-ANSI) GCL was the original host Lisp underlying ACL2, and we are grateful for GCL support that we received from the late Bill Schelter and, more recently and particularly for ANSI GCL, from Camm Maguire.
The `make' process suggested for book certification has changed
substantially, thanks in large part to contributions from Jared Davis and Sol
Swords. We have seen the new process provide better performance on machines
with many cores, and we expect maintenance advantages such as eliminating the
need for Makefiles in individual book directories. The ``classic'' process,
which was based on community books file
books/Makefile-generic, is still
supported (see books-certification-classic) but may disappear in a future
release of ACL2. See books-certification. Most changes should be invisible
to the user, other than improved `make'-level parallelism, with the exception
of the following.
ACL2_JOBSis no longer supported, nor is it necessary; simply use `make' option `-j' instead.
o Regressions now use `make' option
-kby default, which causes the regression to keep going after errors, rather than
-i, which ignores errors. If you encounter problems because of this change, use
ACL2_IGNORE=-iwith your `make' command.
o The `regression' target works for the experimental extension, ACL2(h) (see hons-and-memoization); target `regression-hons' no longer exists.
Please let us know if you run into problems with the new infrastructure, as we consider the legacy infrastructure to be deprecated and we will probably eliminate much of it in the future. In particular, circular dependencies were formerly prohibited at the directory level, but that is no longer the case, and we expect such cycles to occur in the future.
Although ACL2 users don't typically modify raw Lisp variables, we have
arranged to reset Lisp variable
*default-pathname-defaults* if necessary
at startup so that it will not interfere with ACL2, in particular by messing
up the initial connected book directory (see cbd). Thanks to Jared Davis,
Sol Swords, and Raymond Toy for helping us to identify this issue.
print-object$ no longer uses the serialize printer except
in system applications as before (e.g., write out
.cert files). Thanks
to Dave Greve for bringing this issue to our attention.
Jared Davis contributed changes related to the
memoize utility of
ACL2(h), including some low-level changes as well as the following.
Never-memoize specifies that a given function should never
memoize-let, which may never have ever been used.
o Removed the
:inline keyword option to memoize, which was just an alias
For ACL2(p), some anomalous behavior may no longer occur because prover calls (more specifically, trips through the ACL2 ``waterfall'') will return only after all sub-computations (threads) have finished. Thanks to David Rager for contributing this improvement.
ACL2(pr), which includes parallelism (as for ACL2(p)) and non-standard
analysis support for the reals (as for ACL2(r)), now builds and can
certify the community
nonstd/ books. Thanks to David Rager for his
contribution to this capability.