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
|
<html>
<head><title>NOTE-2-6-SYSTEM.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>NOTE-2-6-SYSTEM</h3>ACL2 Version 2.6 Notes on System-level Changes
<pre>Major Section: <a href="NOTE-2-6.html">NOTE-2-6</a>
</pre><p>
We modified the tracking of <code><a href="SKIP-PROOFS.html">skip-proofs</a></code> events and the use of
<code><a href="STATE.html">state</a></code> global <code>ld-skip-proofsp</code> in order to avoid some soundness
issues. For example, <code><a href="SKIP-PROOFS.html">skip-proofs</a></code> events buried in locally-included
books are now tracked. The ``Essay on Skip-proofs'' in source file
<code>axioms.lisp</code> gives several examples of dicey behavior that is no
longer supported.<p>
We fixed a problem with some of the makefiles, so that recursive invocations
of <code>make</code> now use the version of <code>make</code> specified on the command line.<p>
Files were fixed to help non-Unix/Linux users with book
certification. Thanks to John Cowles for finding some problems
and suggesting fixes to <code>books/certify-numbers.lisp</code>,
<code>books/arithmetic/certify.lsp</code>, and <code>books/cowles/certify.lsp</code>.
We thank Scott Burson for noticing and fixing some other such
problems. Moreover, a bdd test was being ignored entirely in
Version 2.5; this problem has been fixed as well.<p>
A minor change in system function save-acl2-in-allegro will allow
this function to continue to work in Allegro CL versions starting
(someday) with 10.0. Thanks to Art Flatau for suggesting such a
fix.<p>
The <code>books/case-studies/</code> directory has been removed. These books are
in support of the first (1998) ACL2 workshop, and are accessible via the
ACL2 home page on the Web at
<code>http://www.cs.utexas.edu/users/moore/acl2/</code>. Also, the
<code>books/cli-misc</code> directory has been renamed <code>books/misc</code>, and the
<code>books/nqthm</code> directory has been removed.<p>
The notion of ACL2 version has been slightly modified to catch
unsoundness due to implementation dependencies. See <a href="VERSION.html">version</a>.
Another change to eliminate such unsoundness is that built-in
symbols now have a <code><a href="SYMBOL-PACKAGE-NAME.html">symbol-package-name</a></code> of <code>"COMMON-LISP"</code>; formerly,
this string was <code>"LISP"</code> for ACL2 images built on GCL.
See <a href="SYMBOL-PACKAGE-NAME.html">symbol-package-name</a>. At a low level, the (undocumented) constant
<code>*main-lisp-package-name*</code> is now <code>"COMMON-LISP"</code>; before, it was
<code>"LISP"</code> for GCL.<p>
<p>
<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>
|
