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
|
<HTML>
<HEAD><TITLE>ACL2 Version 4.3 Installation Guide: Miscellaneous Information</TITLE></HEAD>
<BODY TEXT="#000000">
<BODY BGCOLOR="#FFFFFF">
<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 may fail with 32-bit SBCL because of insufficient heap
memory. Harsh Raju Chamarthi points out that a fix is to run SBCL
with an increased heap size limit, like this:
<pre>
make LISP="<sbcl-path>/sbcl --core <core-path>/sbcl.core --dynamic-space-size 1024"
</pre>
He adds that this issue occurred while building ACL2 4.0 with SBCL v1.0.40 on linux,
and the default heap size for SBCL on a standard 32-bit linux is 512MB,
while for SBCL (64-bit executable) on a 64-bit linux, the default is usually 8GB.
<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), first
<A
HREF="http://www.cs.utexas.edu/users/moore/acl2/v4-3/distrib/acl2-sources/books/nonstd.tar.gz">
download the non-standard analysis books (gzipped tar file)</A> to the
<code>books/</code> subdirectory of your copy of the ACL2 distribution, say,
<I>dir</I>/acl2-sources/books/</code>. Then run:
<pre>
tar xvfz nonstd.tar.gz
</pre>
<p>
Next build an executable image and certify books. First, connect to your
<I>dir</I><code>/acl2-sources/</code> directory and execute<BR><BR> <CODE>cd
acl2-sources</CODE><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=gcl</CODE> is used. On our hosts, <CODE>gcl</CODE> is the name of
GNU Common Lisp, which can be obtained as explained <a
href="obtaining-and-installing.html#Obtaining-GCL">in the Requirements document</a>.
<P>
This will create executable <code>saved_acl2r</code> in the
<I>dir</I><code>/acl2-sources</code> directory (notice the trailing
<code>r</code> in the executable filename).
<P>
Finally, to certify books under directory
<I>dir</I>/acl2-sources/books/nonstd/<code> with ACL2(r), stand in the
</CODE><I>dir</I><CODE>/acl2-sources/</CODE> directory and execute the
following command.
<pre>
make regression-nonstd ACL2=<I>dir</I>/acl2-sources/saved_acl2r
</pre>
<BR><HR><BR>
<H3><A NAME="Addresses">Links and Mailing Lists</A></H3>
There are two mailing lists for ACL2 users. You can post messages to these
lists only if you are a member.
<ul>
<li><CODE><A
HREF="mailto:acl2-help@utlists.utexas.edu">acl2-help@utlists.utexas.edu</A></CODE><br>
ACL2 help list, for questions about using ACL2.
<li><CODE><A
HREF="mailto:acl2@utlists.utexas.edu">acl2@utlists.utexas.edu</A></CODE><br>
General ACL2 list for users and others interested in ACL2.
</ul>
You may subscribe to or unsubscribe from these
lists, or view their archives, at:
<ul>
<li>(<b>acl2</b> list) <code><a href="https://utlists.utexas.edu/sympa/info/acl2">https://utlists.utexas.edu/sympa/info/acl2</a></code></li>
<li>(<b>acl2-help</b> list) <code><a href="https://utlists.utexas.edu/sympa/info/acl2-help">https://utlists.utexas.edu/sympa/info/acl2-help</a></code></li>
</ul>
<P>
You can search the ACL2 documentation, workshops, and publications online from
<CODE><A HREF="http://www.cs.utexas.edu/users/moore/acl2/admin/forms/search.html">
http://www.cs.utexas.edu/users/moore/acl2/admin/forms/search.html</A></CODE>.
<P>
Finally, please report bugs in ACL2 to
<CODE><A HREF="mailto:acl2-bugs@utlists.utexas.edu">acl2-bugs@utlists.utexas.edu</A></CODE>.
<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 4.3 -- A Computational Logic for Applicative Common Lisp<BR>
Copyright (C) 2011 University of Texas at Austin
<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">GNU General Public License</A> as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
<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
GNU General Public License for more details.
<P>
You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
<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>
<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>
|
