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
|
<HTML>
<HEAD><TITLE>ACL2 Version 8.6 News</TITLE></HEAD>
<BODY TEXT="#000000" BGCOLOR="#FFFFFF" STYLE="font-family:'Verdana'">
<H1><A NAME="top"><a href="http://www.cs.utexas.edu/users/moore/acl2/">ACL2</a> Version 8.6 News</A></H1>
<H2>Table of Contents</H2>
<ul>
<LI><A HREF="#bugfix">Bug Fix</A></LI>
<LI><A HREF="#changelog">Changelogs</A></LI>
<LI><A HREF="#git">ACL2 sources availability between releases</A></LI>
<LI><A HREF="#vstte-12">VSTTE 2012 Competition</A></LI>
<LI><A HREF="#acl2-books">ACL2 Books Repository</A></LI>
</ul>
<A NAME="bugfix"><H2>Bug Fix</H2></A>
<p>There was a soundness bug in Version 8.6 and earlier. That bug is
unlikely to affect anyone, as it has probably been present for 30
years without anyone mentioning it to the ACL2 developers. If you
want to fix it, then replace the definition of
function <tt>cl-set-to-implications</tt> with the definition below,
either in source file <tt>proof-builder-a.lisp</tt> before building
your ACL2 executable, or loaded into raw Lisp (so, preceded
by <tt>:q</tt> and followed by <tt>(lp)</tt>, or loaded into ACL2
(so, preceded by <tt>:redef+</tt> and followed by <tt>:redef-</tt>).
The last of these three options will however make it impossible to
certify a book in that session.</p>
<pre>
(defun cl-set-to-implications (cl-set)
(declare (xargs :mode :program))
(if (null cl-set)
nil
(cons (make-implication (dumb-negate-lit-lst (butlast (car cl-set) 1))
(car (last (car cl-set))))
(cl-set-to-implications (cdr cl-set)))))
</pre>
<A NAME="changelog"><H2>Changelogs</H2></A>
<p>The "changelogs" for ACL2 are in
the <a href="http://www.cs.utexas.edu/users/moore/acl2/current/combined-manual/?topic=ACL2____RELEASE-NOTES">release-notes</a>
topics of the manuals. In particular, there
are <a href="http://www.cs.utexas.edu/users/moore/acl2/current/combined-manual/?topic=ACL2____NOTE-8-6">release
notes for Version 8.6</a>.</p>
<A NAME="git"><H2>ACL2 sources availability between releases</H2></A>
<p>ACL2 sources are available between releases at
the <a href="https://github.com/acl2/acl2">ACL2 GitHub
Repository</a>.</p>
<A NAME="vstte-12"><H2>VSTTE 2012 Competition</H2></A>
<p>A team of four ACL2 users entered the VSTTE 2012 competition. For
information, including the team's solution, visit
this <a href="http://www.cs.utexas.edu/users/moore/acl2/vstte-2012/index.html">link</a>.</p>
<A NAME="acl2-books"><H2>ACL2 Books Repository</H2></A>
<p>The <a href="https://github.com/acl2/acl2">ACL2 GitHub
repository</a> allows contributions of ACL2 books (input files), and also
provides between-release updates.</p>
<br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br>
<br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br><br>
</BODY>
</HTML>
|
