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
|
<HTML>
<HEAD><TITLE>ACL2 Version 8.3 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>
<p>ACL2 Version 8.3<br> Copyright (C) 2020, Regents of the University of
Texas</p>
<p>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>
<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-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>
<p>You can see recent performance numbers by following <a
href="http://www.cs.utexas.edu/users/moore/acl2/v8-3/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".</p>
<H3><A NAME="Obtaining-Lisp">Obtaining Common Lisp</A></H3>
<p>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.</p>
<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-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><B><A NAME="Obtaining-Allegro">Obtaining Allegro Common Lisp</A></B></P>
<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>
<P><B><A NAME="Obtaining-CCL">Obtaining CCL (OpenMCL)</A></B></P>
<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>
<p><font color="red">NOTE</font>:
Certain <a href="http://www.cs.utexas.edu/users/moore/acl2/current/combined-manual/index.html?topic=ACL2____HONS-ENABLED">ACL2
features</a> are optimized for 64-bit CCL. Some large developments
may even fail with 32-bit CCL; so for CCL, the 64-bit version is
preferred. To check if your CCL is a 64-bit CCL, evaluate the
following expression in your CCL; the result should
be <code>YES</code>.</p>
<pre>
#+x86_64 'yes #-x86_64 'no
</pre>
<p>Here
are <a href="http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2____CCL-INSTALLATION">instructions
for fetching and installing CCL</a>.</p>
<P><B><A NAME="Obtaining-GCL">Obtaining GCL</A></B></P>
<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>
<p>Otherwise, it should be easy to obtain and build GCL yourself. Note
that ACL2 requires ANSI GCL version 2.6.12 or later. Perhaps simplest
is to fetch it via git and then build the
executable <code>gcl/gcl/bin/gcl</code> as follows.</p>
<pre>
git clone git://git.sv.gnu.org/gcl.git
cd gcl/gcl
git checkout Version_2_6_13pre
./configure --enable-ansi && make
</pre>
<p>It may also be possible to fetch it 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>,
in which case ANSI GCL can be built as shown above:</p>
<pre>
cd gcl && ./configure --enable-ansi && make
</pre>
<P><B><A NAME="Obtaining-LispWorks">Obtaining LispWorks</A></B></P>
<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>
<P><B><A NAME="Obtaining-SBCL">Obtaining SBCL</A></B></P>
<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>.
You may be able to download a suitable binary distribution from that
website, but for some of the older versions (such as 1.2.11, which as
of April 2020 has been the latest binary available for MacOS from
that website for some years), you will not be able to certify some of
the community books. If you download a binary, you can check that the
form <code>(member :sb-thread *features*)</code> evaluates to a value
other than <code>NIL</code>. To avoid this issue you can build from
source, following instructions from the <code>INSTALL</code> file of
the SBCL distribution using this command:</p>
<pre>
sh make.sh --with-sb-thread
</pre>
<!-- The following is no longer needed, because saved_acl2 deals
directly with dynamic-space-size.
<p>Depending on the platform, 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.</p>
<pre>
#!/bin/sh
<sbcl-dir-path>/src/runtime/sbcl --core <sbcl-dir-path>/output/sbcl.core --dynamic-space-size 2000 "$@"
</pre>
-->
<p>If you try to run large jobs using ACL2 built on SBCL (version
1.2.11 or later), such as building the ACL2+books combined manual,
you may fail with an error, "Immobile space exhausted". We have
avoided this error by building SBCL from source rather than
obtaining a binary, using options as follows:</p>
<pre>
sh make.sh --without-immobile-space --without-immobile-code --without-compact-instance-header
</pre>
<p>Rather comparable test runs produced a significant speed-up when
building with the options above, as shown by the following results
when using the "time" command for such runs.</p>
<pre>
;;; before using the options above in the build
85597.939u 1357.892s 3:27:15.73 699.2% 0+0k 1677680+7635408io 607pf+0w
;;; after using the options above in the build
72693.740u 1565.148s 2:58:36.10 692.9% 0+0k 3778176+7630768io 1250pf+0w
</pre>
<p><b><font size="+2">[<a href="installation.html">Back to Installation Guide.</a>]</font></b></p>
<BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR>
</BODY>
</HTML>
|
