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
|
<HTML>
<HEAD><TITLE>ACL2 Version 8.6 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.6<br> Copyright (C) 2024, 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="#Obtaining-Lisp">Obtaining Common Lisp</A> (alphabetical listing)
<UL>
<LI><A HREF="#Obtaining-Allegro">Obtaining Allegro Common Lisp</A></LI>
<LI><A HREF="#Obtaining-CCL">Obtaining CCL (OpenMCL)</A></LI>
<LI><A HREF="#Obtaining-CMUCL">Obtaining CMUCL</A></LI>
<LI><A HREF="#Obtaining-GCL">Obtaining GCL</A></LI>
<LI><A HREF="#Obtaining-LispWorks">Obtaining LispWorks</A></LI>
<LI><A HREF="#Obtaining-SBCL">Obtaining SBCL</A></LI>
</UL>
</UL>
<p><b><font color="red">(Note: Some of the
ACL2 <a href='https://www.cs.utexas.edu/users/moore/acl2/manuals/latest/?topic=ACL2____COMMUNITY-BOOKS'>community
books</a> depend on quicklisp, and those are only guaranteed to
work with CCL or SBCL.)</font></b></p>
<p><hr size=3 noshade></p>
<H3><A NAME="Obtaining-Lisp">Obtaining Common Lisp</A></H3>
<p>ACL2 has been built and tested on x86-64 Linux and on Mac OS X
(Darwin), which we call "Unix-like systems", as well as (from time to
time) some Windows operating systems. It has been successfully run on
other platforms as well, including FreeBSD and on ARM architectures.
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></LI>
<LI><A HREF="#Obtaining-CCL">CCL (OpenMCL)</A></B></LI>
<LI><A HREF="#Obtaining-CMUCL">CMUCL</A></B></LI>
<LI><A HREF="#Obtaining-GCL">GCL</A></B></LI>
<LI><A HREF="#Obtaining-LispWorks">LispWorks</A></B></LI>
<LI><A HREF="#Obtaining-SBCL">SBCL</A></B></LI>
</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>Please
see <a href="http://www.cs.utexas.edu/users/moore/acl2/manuals/latest/index.html?topic=ACL2____CCL-INSTALLATION">instructions
for fetching and installing CCL</a>.</p>
<P><B><A NAME="Obtaining-CMUCL">Obtaining CMUCL</A></B></P>
<p>The website for CMUCL, a free implementation of Common Lisp,
is <code><a href='https://cmucl.org'>https://cmucl.org</a></code>.
Follow the <a href='https://cmucl.org/download.html'>Download</a>
link on that page to obtain CMUCL.</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>.
<p>Please
see <a href="http://www.cs.utexas.edu/users/moore/acl2/manuals/latest/index.html?topic=ACL2____SBCL-INSTALLATION">instructions
for fetching and installing SBCL</a>.</p>
<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>
|
