ACL2 Version 2.7 (November, 2002) Notes
The Version_2.7 notes are divided into the subtopics below. Here
we give only a brief summary of a few of the changes that seem most likely to
impact existing proofs. Not included in this brief summary, but included in
the subtopics, are descriptions of improvements (including bug fixes and new
functionality) that should not get in the way of existing proof efforts.
In particular, please see note-2-7-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.
- Three soundness bugs were fixed. These bugs were probably rarely hit, so
users may well not notice these changes.
- Certify-book now requires :skip-proofs-ok t (respectively,
:defaxioms-okp t) if there are skip-proofs (respectively, defaxiom) events in the book or any included sub-books.
- When :by hints refer to a definition, they now use the original body
of that definition rather than the simplified (``normalized'') body.
- When ld is applied to a stringp file name, it now temporarily
sets the connected book directory (see cbd) to the directory of that
file while evaluating forms in that file.
- Some prover heuristics have changed slightly. Among other consequences,
this can cause subgoal hints to change. For example, suppose that the
Version_2.6 proof of a particular theorem generated "Subgoal 2" and
"Subgoal 1" while Version_2.7 only generates the second of these. Then a
subgoal hint attached to "Subgoal 1" in Version_2.6 would have to be
attached to "Goal'" in Version_2.7. (See goal-spec.) The full topic
has details (see note-2-7-proofs).
Changes in rules and definitions (see note-2-7-rules)
- The package name of a generated variable has changed for defcong.
- Guard verification formerly succeeded in a few cases where it
should have failed.
- Guards generated from type declarations now use functions
signed-byte-p and unsigned-byte-p, now defined in source file
axioms.lisp and formerly defined rather similarly under
- A new table, invisible-fns-table, takes the place of the
handling of invisible functions in the ACL2-defaults-table,
- The theory-invariant event has been modified so that the default
action is an error rather than a warning.
- Proof output that reports destructor elimination no longer uses the word
Again, please proceed to the subtopics for more thorough release
- ACL2 Version 2.7 Notes on Bug Fixes
- ACL2 Version 2.7 Notes on New Functionality
- ACL2 Version 2.7 Notes on Changes in Proof Engine
- ACL2 Version 2.7 Notes on Miscellaneous Changes
- ACL2 Version 2.7 Notes on System-level Changes
- ACL2 Version 2.7 Notes on Changes in Rules and Constants
- ACL2 Version 2.7 Notes on Guard-related Changes
- ACL2 Version 2.7 Notes on proof-builder Changes