ACL2 Version 8.2
Copyright (C) 2019, Regents of the University of
Texas
ACL2 is licensed under the terms of the LICENSE file distributed with ACL2. See also the documentation topic, COPYRIGHT.
You can see recent performance numbers by following this link, or by going to the ACL2 home page on the web and following the link "Recent changes to this page".
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.
The website for Allegro Common Lisp, a commercial implementation, is
http://www.franz.com/.
You may be able to obtain a trial version there.
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
Here are instructions for fetching and installing CCL.
CLISP is a non-commercial Common Lisp implementation, available from
http://clisp.cons.org/.
We do not recommend CLISP as a platform for ACL2, for the following
reasons.
NOTE: ACL2 Version 8.2 cannot be reliably run on CMUCL, so we have disabled building ACL2 on CMUCL. The CMUCL implementor is aware of the problem, and we are hoping for a fix before the next ACL2 release so that we can remove this note.
CMU Common Lisp (sometimes called CMUCL) is a non-commercial Common Lisp
implementation, available from http://www.cons.org/cmucl/.
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
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.
SBCL (Steel Bank Common Lisp) is a non-commercial Common Lisp
implementation, available
from http://sbcl.sourceforge.net/.
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 (member :sb-thread *features*) evaluates to a value
other than NIL. To avoid this issue you can build from
source, following instructions from the INSTALL file of
the SBCL distribution using this command:
sh make.sh --with-sb-thread
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:
sh make.sh --without-immobile-space --without-immobile-code --without-compact-instance-header
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.
;;; 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