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
|
<html>
<head><title>NOTE-2-2.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>NOTE-2-2</h2>ACL2 Version 2.2 (August, 1998) Notes
<pre>Major Section: <a href="RELEASE-NOTES.html">RELEASE-NOTES</a>
</pre><p>
Important changes: <p>
A bug was fixed in the compile command, <code>:comp</code>. The compiled code
produced by <code>:comp</code> in previous versions could be wildly incorrect
because of a confusion between the printer and the reader regarding
what was the current Lisp <code>*package*</code>. This bug could manifest itself
only if you used the <code>:comp</code> command to compile previously uncompiled
functions while the current package was different from <code>"ACL2"</code>.
What happened in that situation depended upon what symbols were
imported into your current package. The most likely behavior is
that the compiler would break or complain or the resulting compiled
code would call functions that did not exist.<p>
There have been no other important changes to the code.
However, this release contains some useful new books, notably those on
the <code>books</code> subdirectories <code>cli-misc</code> and <code>ihs</code>. Both have
<code>README</code> files. The <code>ihs</code> books provide support for integer
hardware specifications. These books were crucial to Bishop Brock's
successful modeling of the Motorola CAP. We thank Bishop for producing
them and we thank all those who worked so hard to get these books released.
We highly recommend the <code>ihs</code> books to those modeling ALUs and other
arithmetic components of microprocessors or programming languages.<p>
In previous versions of ACL2, the arithmetic books, found on
<code>books/arithmetic/</code>, included the addition of several unproved axioms
stating properties of the rationals that we believed could be derived from
our ``official'' axioms but which we had not mechanically proved. The axioms
were found in the book <code>rationals-with-axioms.lisp</code>,
which was then used in the uppermost arithmetic books <code>top.lisp</code> and
<code>top-with-meta.lisp</code>. John Cowles has now provided us with ACL2 proofs
of those ``axioms'' and so in this release you will find both
<code>rationals-with-axioms.lisp</code> and <code>rationals-with-axioms-proved.lisp</code>.
The former is provided for compatibility's sake. The latter is identical
but contains <code>defthm</code>s where the former contains <code>defaxiom</code>s.
The top-most books have been rebuilt using ``<code>-axioms-proved</code>'' book.
Thanks John.
<p>
Less important notes:<p>
Bishop Brock found a bug in <code>translated-acl2-unwind-protectp4</code>.
Jun Sawada reported a bug in linear arithmetic that caused us not to
prove certain trivial theorems concluding with <code>(not (equal i j))</code>.
We have fixed both.<p>
We now prohibit definitions that call certain event commands
such as <code>DEFTHM</code> and <code>TABLE</code> because our Common Lisp implementations
of them differ from their ACL2 meanings (so that compiled books
can be loaded correctly and efficiently).<p>
Minor bugs in the documentation were fixed.
<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>
|
