Major Section: RELEASE-NOTES
The Version_2.8 notes are divided into the indicated subtopics. Here we give only a brief summary of just a few of the major new features and changes that seem most likely to impact existing proofs. Not included in this brief summary, but included in the subtopics, are descriptions of many improvements (including bug fixes and new functionality) that should not get in the way of existing proof efforts. In the description below we also omit discussion of changes that will become clear by way of error messages if they affect you.
In particular, please see note-2-8-new-functionality for discussion of a number of new features that you may find useful.
Acknowledgements and elaboration, as well as other changes, can be found in the subtopics listed below.
o Some of the bug fixes (see note-2-8-bug-fixes):
+ Some soundness bugs were fixed.
+ The handling of free variables in hypotheses (see free-variables) of rewrite and linear rules had a bug that prevented some proofs from going through. Now that this bug has been fixed, you may find some proofs running much more slowly than before. You can use
add-match-free-overrideto remedy this situation; see note-2-8-bug-fixes for details.
+ The default-hints in the current logical world are no longer ignored by
+ Forms violating guard-checking such as
(defconst *silly* (car 3))are now allowed in books.
o Some of the new functionality (see note-2-8-new-functionality):
+ WARNING: You may find that
control-c control-d) can throw you completely out of Lisp where it had not formerly done so.
+ ACL2 now starts up inside the ACL2 loop -- that is,
)is executed automatically -- when built on CLISP or Allegro CL. This was already the case for GCL and CMUCL, and it still is not true for Lispworks.
+ See note-2-8-ordinals for a discussion of a significant change in ordinal represtation, and in particular, for how to preserve existing proofs that depend on the previous ordinal representation.
mbe(``must be equal''),
mbt(``must be true''), and
defexechave been introduced, which allow the user to attach alternate executable definitions to functions.
+ The user can now control multiple matching for free variables in hypotheses for
forward-chainingrules, as has already been supported for
+ It is no longer necessary to specify
(set-match-free-error nil)in order to avoid errors when a rule with free variables in its hypotheses is missing the
+ The form
(break-on-error)causes, at least for most Lisps, entry into the Lisp debugger whenever ACL2 causes an error.
+ A new
tablehas been provided so that advanced users can override the built-in
untranslatefunctionality. See user-defined-functions-table.
pstack(`process [prover] stack'') mechanism, formerly denoted
checkpoints, has been improved. One of these improvements is to show actual parameters with
(pstack t)rather than formals.
defstobjevent is now allowed to take an
:inlineargument, which can speed up execution.
cw-gstackno longer takes arguments for the
state. To print terms in full rather than abbreviated:
(cw-gstack :evisc-tuple nil).
include-bookevent now has an additional (optional) keyword,
:dir. In particular,
(include-book "foo/bar" :dir :system)will include the indicated book after prepending the path of the built-in
books/directory. You will probably not find
:dir :systemto be useful if you move the executable image or distributed books; see include-book, in particular its ``soundness warning''.
+ The printing of results in raw mode (see set-raw-mode) may now be partially controlled by the user: see add-raw-arity.
+ For those using Unix/Linux
cert.acl2file can contain forms to be evaluated before an appropriate
certify-bookcommand is invoked automatically (not included in
o Some of the changes in the proof engine (see note-2-8-proofs):
+ ACL2 now prevents certain rewriting loops; see rewrite-stack-limit.
+ Small changes have been made to heuristics for controlling rewriting during proofs by induction and in handling certain ``weak'' compound-recognizer rules.
+ The handling of free variables in a hypothesis of a rewrite rule (see free-variables) has been improved in the case that the hypothesis is of the form
(equiv x y), where
equivis a known equivalence relation (see equivalence).
+ We have modified how the ACL2 simplifier handles the application of a defined function symbol to constant arguments, by avoiding the introduction of hide when evaluation fails if the term can be rewritten.
+ The generation of "Goal" for recursive (and mutually-recursive) definitions now uses the subsumption/replacement limitation (default 500). See case-split-limitations.
+ Default hints now apply to hints given in definitions, not just theorems. See default-hints.
+ Linear arithmetic now uses the conclusions of
type-setnow uses a small amount of linear reasoning when deciding inequalities.
o Some of the changes in rules, definitions, and constants (see note-2-8-rules):
+ See the above doc topic.
o Guard-related changes are described in see note-2-8-bug-fixes.
o Some of the proof-checker changes (see note-2-8-proof-checker):
+ Added new proof-checker commands
wrap-induct, to combine multiple conjuncts or goals.
type-alistcommand now takes optional arguments that control whether or not the governors and/or conclusion are used in computing the context.
o Some of the system-level changes (see note-2-8-system):
+ ACL2 now runs on OpenMCL and on MCL 5.0.
o Some of the other changes (see note-2-8-other):
+ Emacs file
emacs/emacs-acl2.elhas been updated (see note-2-8-other for details).
:plis given a term other than a symbol, it will print all rewrite rules that match that term.
+ A new function,
pkg-witness, returns a symbol in the given package.
+ The list constant
*acl2-exports*has been extended.
+ A new release of the rtl library has been included:
books/rtl/rel4/. See the
READMEfile in that directory.
Again, please proceed to the subtopics for more thorough release notes.