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
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
|
<HTML>
<HEAD><TITLE>ACL2 Version 8.6 Installation Guide: Miscellaneous Information</TITLE></HEAD>
<BODY TEXT="#000000" BGCOLOR="#FFFFFF" STYLE="font-family:'Verdana'">
<H1>Miscellaneous Information</A></H1>
<b><font>[<a href="installation.html">Back to main page of Installation Guide.</a>]</font></b>
<p>
<B>Table of Contents</B><BR>
<UL>
<LI><A HREF="#Problems">Problems</A>
<LI><A HREF="#ACL2r">Reasoning about the Real Numbers</A>
<LI><A HREF="#Addresses">Links and Mailing Lists</A>
<LI><A HREF="#Export">Export/Re-Export Limitations</A>
<LI><A HREF="#License-and-Copyright">License and Copyright</A>
</UL>
<p><hr size=3 noshade><p>
Please <A HREF="mailto:kaufmann@cs.utexas.edu,moore@cs.utexas.edu">let us know</A> if there is
other information that you would find of use in this guide.
<BR><HR><BR>
<H3><A NAME="Problems">Problems</A></H3>
If you are having problems using the `make' utility, be sure that you
are using GNU make. We have seen problems with Version 3.81 of that
utility, so if you encounter errors, please consider our <a
href="installing-make.html">instructions for downloading and
installing GNU make version 3.80</a>.
<P>
Building ACL2 with SBCL may require the use
of <code>--dynamic-space-size</code>. This is explained in the
section on <a href="requirements.html#Obtaining-SBCL">Obtaining
SBCL</a>.
<BR><HR><BR>
<H3><A NAME="ACL2r">Reasoning about the Real Numbers</H3>
ACL2 supports rational numbers but not real numbers. However, starting
with Version 2.5, a variant of ACL2 called "ACL2(r)" supports the real
numbers by way of non-standard analysis. ACL2(r) was conceived and
first implemented by Ruben Gamboa in his Ph.D. dissertation work,
supervised by Bob Boyer with active participation by Matt Kaufmann.
See the documentation topic <CODE>REAL</CODE> for information about this
extension and how to build it, and a warning about its experimental nature.
<P>
If you care to use ACL2(r), you will need to build an executable image
and you will probably want to certify books. First, connect to your
new <I>dir</I><code>/acl2-8.6/</code> directory and
execute<BR><BR><CODE>make large-acl2r LISP=</CODE><I>xxx</I><BR>
<BR>
where <I>xxx</I> is the command to run your local Common Lisp.
<P>
By default, if no <CODE>LISP=</CODE><I>xxx</I> is specified,
<CODE>LISP=ccl</CODE> is used. On our hosts, <CODE>ccl</CODE> is the name of
Clozure Common Lisp (CCL), which can be obtained as explained <a
href="obtaining-and-installing.html#Obtaining-CCL">in the Requirements document</a>.
<P>
This will create executable <code>saved_acl2r</code> in the
<I>dir</I><code>/acl2-8.6</code> directory (notice the final
letter <code>r</code> in the executable filename).
<P>
Finally, you can certify books under directory
<code><I>dir</I>/acl2-8.6/books/nonstd/</code> with ACL2(r) in the usual
way; for example, see the documentation topic for
<a href="../../manual/index.html?topic=ACL2____BOOKS-CERTIFICATION">BOOKS-CERTIFICATION</a>.
<BR><HR><BR>
<H3><A NAME="Addresses">Links and Mailing Lists</A></H3>
There are the following mailing lists for ACL2 users. You can post messages to these
lists only if you are a member, but anyone can view the archives.
<ul>
<li><b>acl2 list</b>: General ACL2 list for users and others interested in ACL2
<ul>
<li>To post: <CODE><A HREF="mailto:acl2@utlists.utexas.edu">acl2@utlists.utexas.edu</A></CODE></li>
<li>To subscribe, unsubscribe, or view archives:
<code><a href="https://utlists.utexas.edu/sympa/info/acl2">https://utlists.utexas.edu/sympa/info/acl2</a></code></li>
</ul>
</li>
<li><b>acl2-help list</b>: ACL2 help list, for questions about using
ACL2 <font color="red">(recommended for new users)</font>
<ul>
<li>To post: <CODE><A HREF="mailto:acl2-help@utlists.utexas.edu">acl2-help@utlists.utexas.edu</A></CODE></li>
<li>To subscribe, unsubscribe, or view archives:
<code><a href="https://utlists.utexas.edu/sympa/info/acl2-help">https://utlists.utexas.edu/sympa/info/acl2-help</a></code></li>
</ul>
</li>
<li><b>acl2-books list</b>: Mailing list for discussion of
cutting-edge developments in ACL2 and the ACL2 Community Books
<ul>
<li>To post: <CODE><A
HREF="mailto:acl2-books@googlegroups.com">acl2-books@googlegroups.com</A></CODE></li>
<li>To subscribe, unsubscribe, or view archives:
<code><a href="https://groups.google.com/forum/#!forum/acl2-books">https://groups.google.com/forum/#!forum/acl2-books</a></code></li>
</ul>
</li>
</ul>
<P>
Finally, please report bugs in ACL2 to
<A HREF="mailto:kaufmann@cs.utexas.edu">Matt Kaufmann</A>.
<BR><HR><BR>
<H3><A NAME="Export">Export/Re-Export Limitations</A></H3>
ACL2 may be exported to any countries except those subject to embargoes under
various laws administered by the Office of Foreign Assets Control ("OFAC") of
the U. S. Department of the Treasury.
<BR><HR><BR>
<H3><A NAME="License-and-Copyright">License and Copyright</A></H3>
ACL2 Version 8.6 -- A Computational Logic for Applicative Common Lisp<BR>
Copyright (C) 2024, Regents of the University of Texas
<P>
This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
(C) 1997 Computational Logic, Inc.
<P>
This program is free software; you can redistribute it and/or modify
it under the terms of
the <a href="../LICENSE">LICENSE</a> file
distributed with ACL2.
<P>
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
<a href="../LICENSE">LICENSE</a> for more details.
<P>
Matt Kaufmann (Kaufmann@cs.utexas.edu)<BR>
J Strother Moore (Moore@cs.utexas.edu)<BR>
<BR>
Department of Computer Sciences<BR>
University of Texas at Austin<BR>
Austin, TX 78712-1188 U.S.A.<BR>
<BR>
<p>
For more information on copyright, licensing, and authorship, see the
documentation topic,
<a href="../../manual/index.html?topic=ACL2____COPYRIGHT">COPYRIGHT</a>.
<BR><HR><BR>
<p>Although releases are best obtained according to
the <a href="installation.html">installation instructions</a> by fetching
a <a href="https://github.com/acl2-devel/acl2-devel/releases/download/8.6/acl2-8.6.tar.gz">gzipped
tar file from GitHub</a> containing ACL2 Version 8.6 and the
corresponding Community Books, here we note that the git commit hash
for Version 8.6 of <a href="https://github.com/acl2/acl2">ACL2 on
github</a> is:</p>
<pre>
4fd2eb6bbb3e6a4c66dcbc8aa179272a7a21d51b
</pre>
<BR><HR><BR>
<b><font size="+2">[<a href="installation.html">Back to Installation Guide.</a>]</font></b>
<BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR>
</BODY>
</HTML>
|
