1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
<html>
<head><title>NOTE-2-7.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>NOTE-2-7</h2>ACL2 Version 2.7 (November, 2002) Notes
<pre>Major Section: <a href="RELEASE-NOTES.html">RELEASE-NOTES</a>
</pre><p>
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.<p>
In particular, please see <a href="NOTE-2-7-NEW-FUNCTIONALITY.html">note-2-7-new-functionality</a> for discussion of a
number of new features that you may find useful.<p>
Acknowledgements and elaboration, as well as other changes, can be found in
the subtopics listed below.<p>
o Bug fixes (see <a href="NOTE-2-7-BUG-FIXES.html">note-2-7-bug-fixes</a>):
<blockquote><p>
+ Three soundness bugs were fixed. These bugs were probably rarely hit, so
users may well not notice these changes.<p>
+ <code><a href="CERTIFY-BOOK.html">Certify-book</a></code> now requires <code>:skip-proofs-ok t</code> (respectively,
<code>:defaxioms-okp t</code>) if there are <code><a href="SKIP-PROOFS.html">skip-proofs</a></code> (respectively,
<code><a href="DEFAXIOM.html">defaxiom</a></code>) events in the book or any included sub-books.<p>
+ When <code>:by</code> hints refer to a definition, they now use the original body of
that definition rather than the simplfied (``normalized'') body.<p>
+ When <code><a href="LD.html">ld</a></code> is applied to a stringp file name, it now temporarily sets the
connected book directory (see <a href="CBD.html">cbd</a>) to the directory of that file while
evaluating forms in that file.</blockquote>
<p>
o New functionality (see <a href="NOTE-2-7-NEW-FUNCTIONALITY.html">note-2-7-new-functionality</a>):
<blockquote><p>
+ ACL2 now works harder to apply <code>:</code><code><a href="REWRITE.html">rewrite</a></code> and <code>:</code><code><a href="LINEAR.html">linear</a></code>
rules with free variables in the hypotheses. See <a href="NOTE-2-7-NEW-FUNCTIONALITY.html">note-2-7-new-functionality</a>,
in particular its first two paragraphs, for details. <a href="FORWARD-CHAINING.html">Forward-chaining</a>
also does more with free variables.</blockquote>
<p>
o Changes in proof engine (see <a href="NOTE-2-7-PROOFS.html">note-2-7-proofs</a>):
<blockquote><p>
+ Some prover heuristics have changed slightly. Among other consequences,
this can cause subgoal <a href="HINTS.html">hints</a> 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 <a href="GOAL-SPEC.html">goal-spec</a>.) The full topic has
details (see <a href="NOTE-2-7-PROOFS.html">note-2-7-proofs</a>).</blockquote>
<p>
o Changes in rules and definitions (see <a href="NOTE-2-7-RULES.html">note-2-7-rules</a>):
<blockquote><p>
+ The package name of a generated variable has changed for <code><a href="DEFCONG.html">defcong</a></code>.</blockquote>
<p>
o Guard-related changes (see <a href="NOTE-2-7-GUARDS.html">note-2-7-guards</a>):
<blockquote><p>
+ <code><a href="GUARD.html">Guard</a></code> verification formerly succeeded in a few cases where it should
have failed.<p>
+ Guards generated from type declarations now use functions
<code>signed-byte-p</code> and <code>unsigned-byte-p</code>, now defined in source file
<code>axioms.lisp</code> and formerly defined rather similarly under <code>books/ihs/</code>.</blockquote>
<p>
o Proof-checker changes (see <a href="NOTE-2-7-PROOF-CHECKER.html">note-2-7-proof-checker</a>):
<blockquote><p>
+ See the above doc topic.</blockquote>
<p>
o System-level changes (see <a href="NOTE-2-7-SYSTEM.html">note-2-7-system</a>):
<blockquote><p>
+ See the above doc topic.</blockquote>
<p>
o Other changes (see <a href="NOTE-2-7-OTHER.html">note-2-7-other</a>):
<blockquote><p>
+ A new <code><a href="TABLE.html">table</a></code>, <code><a href="INVISIBLE-FNS-TABLE.html">invisible-fns-table</a></code>, takes the place of the
handling of invisible functions in the <code><a href="ACL2-DEFAULTS-TABLE.html">acl2-defaults-table</a></code>,<p>
+ The <code><a href="THEORY-INVARIANT.html">theory-invariant</a></code> event has been modified so that the default action
is an error rather than a warning.<p>
+ Proof output that reports destructor elimination no longer uses the word
``generalizing''.</blockquote>
<p>
Again, please proceed to the subtopics for more thorough release notes.<p>
<p>
<ul>
<li><h3><a href="NOTE-2-7-BUG-FIXES.html">NOTE-2-7-BUG-FIXES</a> -- ACL2 Version 2.7 Notes on Bug Fixes
</h3>
</li>
<li><h3><a href="NOTE-2-7-GUARDS.html">NOTE-2-7-GUARDS</a> -- ACL2 Version 2.7 Notes on Guard-related Changes
</h3>
</li>
<li><h3><a href="NOTE-2-7-NEW-FUNCTIONALITY.html">NOTE-2-7-NEW-FUNCTIONALITY</a> -- ACL2 Version 2.7 Notes on New Functionality
</h3>
</li>
<li><h3><a href="NOTE-2-7-OTHER.html">NOTE-2-7-OTHER</a> -- ACL2 Version 2.7 Notes on Miscellaneous Changes
</h3>
</li>
<li><h3><a href="NOTE-2-7-PROOF-CHECKER.html">NOTE-2-7-PROOF-CHECKER</a> -- ACL2 Version 2.7 Notes on Proof-checker Changes
</h3>
</li>
<li><h3><a href="NOTE-2-7-PROOFS.html">NOTE-2-7-PROOFS</a> -- ACL2 Version 2.7 Notes on Changes in Proof Engine
</h3>
</li>
<li><h3><a href="NOTE-2-7-RULES.html">NOTE-2-7-RULES</a> -- ACL2 Version 2.7 Notes on Changes in Rules and Constants
</h3>
</li>
<li><h3><a href="NOTE-2-7-SYSTEM.html">NOTE-2-7-SYSTEM</a> -- ACL2 Version 2.7 Notes on System-level Changes
</h3>
</li>
</ul>
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
