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
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
|
<HTML>
<HEAD><TITLE>ACL2 Version 7.2 Installation Guide: Requirements</TITLE></HEAD>
<BODY TEXT="#000000" BGCOLOR="#FFFFFF" STYLE="font-family:'Verdana'">
<H1>Requirements</A></H1>
<b><font>[<a href="installation.html">Back to main page of Installation Guide.</a>]</font></b>
<p><hr size=3 noshade><p>
ACL2 Version 7.2<br> Copyright (C) 2016, Regents of the University of
Texas<br>
ACL2 is licensed under the terms of
the <a href="../LICENSE">LICENSE</a>
file distributed with ACL2. See also the documentation topic,
<a href="../../manual/index.html?topic=ACL2____COPYRIGHT">COPYRIGHT</a>.
<p><hr size=3 noshade><p>
<H3>Table of Contents</H3>
<UL>
<LI><A HREF="#Performance">Performance comparisons</A>
<LI><A HREF="#Obtaining-Lisp">Obtaining Common Lisp</A> (alphabetical listing)
<UL>
<LI><A HREF="#Obtaining-Allegro">Obtaining Allegro Common Lisp</A>
<LI><A HREF="#Obtaining-CCL">Obtaining CCL (OpenMCL)</A>
<LI><A HREF="#Obtaining-CLISP">Obtaining CLISP</A>
<LI><A HREF="#Obtaining-CMUCL">Obtaining CMU Common Lisp</A>
<LI><A HREF="#Obtaining-GCL">Obtaining GCL</A>
<LI><A HREF="#Obtaining-LispWorks">Obtaining LispWorks</A>
<LI><A HREF="#Obtaining-SBCL">Obtaining SBCL</A>
</UL>
</UL>
<p><hr size=3 noshade><p>
<H3><A NAME="Performance">Performance comparisons</A></H3>
You can see recent performance numbers by following <a
href="http://www.cs.utexas.edu/users/moore/acl2/v7-2/HTML/new.html#performance">this
link</a>, or by going to the <a
href="http://www.cs.utexas.edu/users/moore/acl2/">ACL2 home page on
the web</a> and following the link "Recent changes to this page".
<H3><A NAME="Obtaining-Lisp">Obtaining Common Lisp</A></H3>
ACL2 works on Unix, GNU-Linux, and Mac OS X, which we call "Unix-like
systems", as well as many Windows operating systems (at least
including Windows 98, Windows 2000, and Windows XP). It can be built
on top of any of the following Common Lisps, listed here
alphabetically.
<ul>
<LI><A HREF="#Obtaining-Allegro">Allegro Common Lisp</A></B><P>
<LI><A HREF="#Obtaining-CCL">CCL (OpenMCL)</A></B><P>
<LI><A HREF="#Obtaining-CLISP">CLISP</A></B><P>
<LI><A HREF="#Obtaining-CMUCL">CMU Common Lisp</A></B><P>
<LI><A HREF="#Obtaining-GCL">GCL</A></B><P>
<LI><A HREF="#Obtaining-LispWorks">LispWorks</A></B><P>
<LI><A HREF="#Obtaining-SBCL">SBCL</A></B><P>
</ul>
<p>
<P><B><A NAME="Obtaining-Allegro">Obtaining Allegro Common Lisp</A></B><P>
The website for Allegro Common Lisp, a commercial implementation, is
<code><a href="http://www.franz.com/">http://www.franz.com/</a></code>.
You may be able to obtain a trial version there.
<P><B><A NAME="Obtaining-CCL">Obtaining CCL (OpenMCL)</A></B><P>
Clozure Common Lisp (Clozure CL, or CCL) was formerly known as
OpenMCL. Quoting from the <a href="http://ccl.clozure.com/">Clozure
Common Lisp web page</a> (July, 2014): ``Some distinguishing features
of the implementation include fast compilation speed, native threads,
a precise, generational, compacting garbage collector, and a
convenient foreign-function interface.''
<p>
Here is an easy way to obtain and build the latest version (generally
recommended) for Linux (or another OS; see below) running on an x86 or
x86-64. First execute the following shell command to create
a <code>ccl</code> directory, but substituting
for <code>linuxx86</code>, if appropriate, any of
<code>darwinx86</code> (which we use for modern Macs), <code>freebsdx86</code>,
<code>solarisx86</code>, <code>windows</code>, <code>darwinppc</code>,
or <code>linuxppc</code>.
<pre>
svn co http://svn.clozure.com/publicsvn/openmcl/trunk/linuxx86/ccl
</pre>
Note: if however you insist on using the latest release, you can
obtain that instead, for example as follows (but replace "1.9" by the
latest version, for example as described
at <code>http://ccl.clozure.com/download.html</code>, and
replace <code>linuxx86</code> if appropriate as described above).
<pre>
svn co http://svn.clozure.com/publicsvn/openmcl/release/1.9/linuxx86/ccl
</pre>
Next rebuild the executable by issuing the following commands, but
replace "<code>./lx86cl64</code>" by a suitable executable; e.g., for
64-bit Darwin (on Mac OS) use "<code>./dx86cl64</code>".
<hr>
<pre>
./lx86cl64
(rebuild-ccl :full t)
(quit)
./lx86cl64
(rebuild-ccl :full t)
(quit)
</pre>
<hr>
<p>
Now your CCL executable is up to date. Next, create a suitable
script, say as follows, where <code>DIR</code> is the full pathname
for the directory above the new <code>ccl</code> directory.
<hr>
<pre>
#!/bin/sh
tmp=`uname -a | fgrep x86_64`
export CCL_DEFAULT_DIRECTORY=DIR/ccl
# Start up 64-bit or 32-bit lisp, respectively:
if [ "$tmp" != "" ] ; then \
DIR/ccl/scripts/ccl64 $* ; \
else \
DIR/ccl/scripts/ccl $* ; \
fi
</pre>
<hr>
Be sure to make your script executable. For example, if your script
filename is <code>my-script</code> then on linux you might want to
execute the following shell command.
<pre>
chmod +x my-script
</pre>
Your script (invoked with a suitable pathname, or just the filename if
the directory is on your path) will now start the updated CCL lisp
image.
<p>
More details if you want or need them:<br>
Step 3 in
<code><a
href="http://trac.clozure.com/openmcl/wiki/UpdatingFromSource">http://trac.clozure.com/openmcl/wiki/UpdatingFromSource</a></code>
has more details on building from source.
Alternatively, you can download a gzipped tar
file; see <a href="http://trac.clozure.com/openmcl">the main
Clozure CL page</a>. (Note: Subversion and gzipped tar
files are great, but not so much a CCL disk image (<code>.dmg</code>
file), as we have had a report of the extracted CCL opening its own
window when you start it up.) If you don't want to write your own
script (as suggested above) then after obtaining CCL, you may wish to
edit file <code>ccl/scripts/ccl</code> or file
<code>ccl/scripts/ccl64</code>, depending on whether you want to
use a 32-bit or 64-bit version (respectively).
<P><B><A NAME="Obtaining-CLISP">Obtaining CLISP</A></B><P>
CLISP is a non-commercial Common Lisp implementation, available from
<code><a href="http://clisp.cons.org/">http://clisp.cons.org/</a></code>.
We do not recommend CLISP as a platform for ACL2, for the following
reasons.
<ul>
<li>CLISP appears to run ACL2 much more slowly than the other supported
Common Lisp implementations.</li>
<li>Only minimal testing is done for ACL2 built on CLISP.</li>
<li>CLISP does not support building the
default, <a href="http://www.cs.utexas.edu/users/moore/acl2/v7-2/combined-manual/index.html?topic=ACL2____HONS-ENABLED">hons-enabled</a>
ACL2 (ACL2(h)), but only (with the limitations expressed above)
a discontinued version, ACL2(c).</li>
</ul>
<P><B><A NAME="Obtaining-CMUCL">Obtaining CMU Common Lisp</A></B><P>
CMU Common Lisp (sometimes called CMUCL) is a non-commercial Common Lisp
implementation, available from <code><a
href="http://www.cons.org/cmucl/">http://www.cons.org/cmucl/</a></code>.
<P><B><A NAME="Obtaining-GCL">Obtaining GCL</A></B><P>
You might be able
to <A HREF="http://packages.qa.debian.org/a/acl2.html">download a
binary Debian package for ACL2</A>. Thanks to Camm Maguire for
maintaining this package. Note however that it may take some time
after each ACL2 release for this binary Debian package to be updated
for that release.
<p>
Otherwise, it should be easy to obtain and build GCL yourself. Note
that ACL2 requires GCL version 2.6.12 or later, which can be fetched
as a tarball from the <a href="http://www.gnu.org/software/gcl/">main
GNU website for GCL</a> or perhaps
from <code><a href="http://backports.debian.org">backports.debian.org</a></code>.
ACL2 also requires an ANSI Common Lisp executable;
after unpacking the archive, an ANSI GCL can be built as follows.
<pre>
cd gcl && ./configure --enable-ansi && make
</pre>
<P><B><A NAME="Obtaining-LispWorks">Obtaining LispWorks</A></B><P>
LispWorks is a commercial Common Lisp implementation. You can download
a free, restricted, version
from <code><a href="http://www.lispworks.com/">http://www.lispworks.com/</a></code>.
You may ask the vendor for an evaluation license for the full product
if you are considering purchasing a license.
<P><B><A NAME="Obtaining-SBCL">Obtaining SBCL</A></B><P>
SBCL (Steel Bank Common Lisp) is a non-commercial Common Lisp
implementation, available from <code><a
href="http://sbcl.sourceforge.net/">http://sbcl.sourceforge.net/</a></code>.
<p>
Building ACL2 may initially fail with SBCL because of insufficient heap
memory. Harsh Raju Chamarthi points out that a fix is to run SBCL
with an increased heap size limit. As of 2014 we find that the
the option <code>--dynamic-space-size 2000</code> following works well
on 64-bit linux, for example using a script like the following for
SBCL.
<pre>
#!/bin/sh
<sbcl-dir-path>/src/runtime/sbcl --core <sbcl-dir-path>/output/sbcl.core --dynamic-space-size 2000 "$@"
</pre>
<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>
|
