		Search-engine friendly clone of the ACL2 documentation.

Installation

Installation-summary

ACL2 installation summary for Unix-like systems

Here, “Unix-like Systems” includes Unix and its Linux variants (e.g., Debian), as well as MacOS X. Note that a quicker install may be possible, by instead obtaining a binary distribution; see pre-built-binary-distributions if one is available for your platform. Otherwise, you can follow the directions below, which start by fetching a file hosted at the GitHub ACL2 System and Books website. The result is a directory containing not only the ACL2 system but, in the books/ subdirectory, the ACL2 libraries; see community-books. The ACL2 system, which has been developed at the University of Texas at Austin, can be obtained or explored separately (though this is rarely done); see obtaining-ACL2.

Change to a directory whose full pathname contains no whitespace and which does not already contain a subdirectory named acl2 or acl2-8.6. Then use either of the following two methods to obtain the ACL2 source code and community books.
- (Recommended if you don't plan to update from git)
  Download gzipped tar file acl2-8.6.tar.gz from GitHub and then execute the following (the rm command is just to make sure you don't already have a subdirectory named acl2-8.6):
```
rm -rf acl2-8.6
tar xfz acl2-8.6.tar.gz
```
  This will create a subdirectory named acl2-8.6. Change to that directory.
- (Development snapshot, required if you want to update from GitHub; see github-commit-code-using-pull-requests)
  Execute the following (the rm command is just to make sure you don't already have a subdirectory named acl2):
```
rm -rf acl2
git clone https://github.com/acl2/acl2
```
  This will create the subdirectory acl2. Change to that directory.

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

Execute the following command.
```
make LISP=<path_to_your_lisp_executable>
```
This will create a script in the current directory for running ACL2. The script is named saved_acl2.
Note: You will need Gnu make (preferably newer than Version 3.8.2).
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 ACL2 executable called saved_acl2 (from step 3) and access to certified community books (from step 4). Enjoy! And please consider contributing to the ACL2 libraries; see how-to-contribute.