ACL2 Version 6.2 (June, 2013) 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
The macro top-level has been changed, so that evaluation of a form
The macro the no longer causes an error when guard-checking
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 proposed defpkg events, and it shows the symbols that are imported by one but not the other. Thanks to Jared Davis for requesting this improvement.
Functions open-input-channel and open-output-channel no
longer cause an error when failing to open a channel because of a permissions
problem, but instead return
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-processor rules, much as they are used in hypotheses of meta rules. 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(and meta-extract-global-fact+), which results in a term equating a function application to its result. See meta-extract, in particular the discussion of :fncall.
It is now possible for
It was possible for the guard-debug feature to generate duplicate
When in-theory returns without error, it returns a value
A new keyword parameter for ld is
Even if the function
When the second argument of certify-book is a symbol, that symbol
formerly needed to be
(For system hackers, not standard ACL2 users:) Utilities initialize-event-user and finalize-event-user now each take a list of
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
A new xargs keyword,
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
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 defattach to 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
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
(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 macro
(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., `
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
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 defabsstobj event had a guard of
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 (
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
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
In ACL2(h), print-object$ no longer uses the serialize printer
except in system applications as before (e.g., write out
Jared Davis contributed changes related to the memoize utility of ACL2(h), including some low-level changes as well as the following.
o Never-memoize specifies that a given function should never be memoized.
o Removed the
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