		Search-engine friendly clone of the ACL2 documentation.

Installation

Installation-instructions

ACL2 installation instructions for Unix-like systems

These instructions describe how to install ACL2 on “Unix-like systems”, including Linux, macOS (with Intel or ARM processors), and FreeBSD. To install ACL2 on Windows, see windows-installation.

ACL2 installations include both the ACL2 system and the open-source ACL2 libraries developed by the ACL2 community, called the Community Books.

Decide which of the following you want to install:
- The latest ACL2 release (version 8.6). The release is stable and very well tested but does not include any improvements or fixes made since October, 2024. It may be appropriate if you do not need the very latest tools and libraries and do not plan to contribute to the community-books. A pre-built binary distribution of the release may be available for your platform, which can let you avoid following these installation instructions.
- The latest development snapshot from GitHub (likely at most a few days old). Development snapshots are only minimally tested and may (rarely) have problems. However, they provide the latest iteration of ACL2 and the community-books. Use a development snapshot if you plan to contribute additions or changes to the community-books, or if you plan to update your copy of ACL2 later. Pre-built binary distributions of development snapshots are generally not available.

Obtain a Common Lisp implementation if you don't already have one; see obtaining-common-lisp. (Note: Some of the community-books depend on Quicklisp, and those are only guaranteed to work with CCL or SBCL.)

Depending on your decision in Step 1, download ACL2 by doing either of the following:
- For the latest ACL2 release (version 8.6):
  1. Change to a directory that does not already contain a subdirectory called acl2-8.6.
  2. Download acl2-8.6.tar.gz to that directory.
  3. Execute the following:
```
tar xfz acl2-8.6.tar.gz
cd acl2-8.6
```
  The new subdirectory acl2-8.6 should now be your shell's current directory.
- Or, for the latest development snapshot:
  1. Change to a directory that does not already contain a subdirectory named acl2.
  2. Execute the following:
```
git clone https://github.com/acl2/acl2
cd acl2
```
  The new subdirectory acl2 should now be your shell's current directory.

Compile ACL2:
```
make LISP=<path_to_your_lisp_executable>
```
Note: You will need GNU Make (preferably newer than Version 3.82). This will create an executable script named saved_acl2 (in the current directory) that can be used to run ACL2.

Optionally, test ACL2 as follows:
```
./saved_acl2
:mini-proveall
(quit)
```
You should see "Mini-proveall completed successfully." a few lines above the bottom of the output.

Certify some books, for example with
```
make basic
```
or something fancier such as the following.
```
(time nice make -j 8 ACL2=/u/smith/bin/acl2 basic) >& make-basic.log
```
This may take only a few minutes, depending your -j value, your machine, and your host Common Lisp. The resulting log should contain no occurrences of the string “CERTIFICATION FAILED”; a normal exit (status 0) should guarantee this. If you want further options or additional explanation (e.g., you can certify many more books with make regression, and there is a discussion of avoiding root login), see books-certification.

You now have an executable script called saved_acl2 and access to certified community books. Enjoy! And please consider contributing to the ACL2 libraries; see how-to-contribute.