NOTE-2-7

ACL2 Version 2.7 (November, 2002) Notes 
Major Section:  RELEASE-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.

o Bug fixes (see note-2-7-bug-fixes):

+ 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 simplfied (``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.

o New functionality (see note-2-7-new-functionality):

+ ACL2 now works harder to apply :rewrite and :linear rules with free variables in the hypotheses. See note-2-7-new-functionality, in particular its first two paragraphs, for details. Forward-chaining also does more with free variables.

o Changes in proof engine (see note-2-7-proofs):

+ 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).

o Changes in rules and definitions (see note-2-7-rules):

+ The package name of a generated variable has changed for defcong.

o Guard-related changes (see note-2-7-guards):

+ 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 books/ihs/.

o Proof-checker changes (see note-2-7-proof-checker):

+ See the above doc topic.

o System-level changes (see note-2-7-system):

+ See the above doc topic.

o Other changes (see note-2-7-other):

+ 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 ``generalizing''.

Again, please proceed to the subtopics for more thorough release notes.