Pre-built binary distributions of ACL2
Visit the “Recent changes to this page” link on the ACL2 home page to see if there are other shortcuts available.
WARNING: Some of these packages might be for old versions of ACL2. We recommend that you use the latest version of ACL2 (Version 8.5).
The ACL2 Sedan (see ACL2-sedan), also known as ACL2s, is an
Eclipse-based IDE for ACL2 that is distributed with pre-certified books and
pre-built binaries, though it is not always based on the latest ACL2 version.
If you use an alternative development environment (such as Emacs), you can
still fetch a tarball
for your x86-based Linux/Mac/Windows system that contains a pre-built binary
of (pure) ACL2, using the following instructions based on information kindly
provided by Harsh Raju Chamarthi. Just extract the appropriate tarball (using
In the past, a Windows Installer for ACL2 has included a Unix environment, pre-certified standard and workshop books, and a copy of Gnu Emacs. This capability has largely been superseded in the installation instructions' section on Building an Executable Image on Some Particular Systems and the Shortcut using the ACL2 Sedan, above. See also windows-installation.
ACL2 versions are sometimes been made available under MacPorts.
A Debian Gnu Linux package is available, which is likely to work on other
Linux systems as well. Thanks to Camm Maguire for maintaining this package,
and for pointing out that as Debian packages are simply ar and tar archives,
they can be unpacked on any linux system, and who has said: “If someone
is running Debian, all they want to do is 'apt-get install acl2', doing
likewise for any optional add-on package they wish as well, e.g. emacs, infix,
etc.” Alternatively, Debian GNU Linux users may wish to download the ACL2 Debian
package for Linux. An alternate location you might want to check is