Requirements

[Back to main page of Installation Guide.]

ACL2 is licensed under the terms of the LICENSE file distributed with ACL2. See also the documentation topic, COPYRIGHT.

Obtaining Common Lisp (alphabetical listing)

(Note: Some of the ACL2 community books depend on quicklisp, and those are only guaranteed to work with CCL or SBCL.)

Obtaining Common Lisp

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.

Allegro Common Lisp
CCL (OpenMCL)
CMUCL
GCL
LispWorks
SBCL

Obtaining Allegro Common Lisp

The website for Allegro Common Lisp, a commercial implementation, is http://www.franz.com/. You may be able to obtain a trial version there.

Obtaining CCL (OpenMCL)

Clozure Common Lisp (Clozure CL, or CCL) was formerly known as OpenMCL. Quoting from the Clozure Common Lisp web page (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.''

NOTE: Certain ACL2 features 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 YES.

#+x86_64 'yes #-x86_64 'no

Please see instructions for fetching and installing CCL.

Obtaining CMUCL

The website for CMUCL, a free implementation of Common Lisp, is https://cmucl.org. Follow the Download link on that page to obtain CMUCL.

Obtaining GCL

You might be able to download a binary Debian package for ACL2. 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.

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 gcl/gcl/bin/gcl as follows.

git clone git://git.sv.gnu.org/gcl.git
cd gcl/gcl
git checkout Version_2_6_13pre
./configure --enable-ansi && make

It may also be possible to fetch it from the main GNU website for GCL or perhaps from backports.debian.org, in which case ANSI GCL can be built as shown above:

cd gcl && ./configure --enable-ansi && make

Obtaining LispWorks

LispWorks is a commercial Common Lisp implementation. You can download a free, restricted, version from http://www.lispworks.com/. You may ask the vendor for an evaluation license for the full product if you are considering purchasing a license.

Obtaining SBCL

SBCL (Steel Bank Common Lisp) is a non-commercial Common Lisp implementation, available from http://sbcl.sourceforge.net/.

Please see instructions for fetching and installing SBCL.

[Back to Installation Guide.]

Requirements

Table of Contents

Obtaining Common Lisp