books/subdirectory, the community books (libraries). The ACL2 system is developed at the University of Texas at Austin and can also be obtained or explored separately.
acl2-8.5. Then use either of the following two methods to obtain the ACL2 source code and community books.
acl2-8.5.tar.gzfrom GitHub and then execute:
tar xfz acl2-8.5.tar.gz
acl2-8.5. Change to that directory.
git clone https://github.com/acl2/acl2
acl2. Change to that directory.
make LISP=<path_to_your_lisp_executable>This will create a script in the current directory for running ACL2. The script is named
make basicor something fancier such as the following:
(time nice make -j 8 ACL2=/u/smith/bin/acl2 basic) >& make-basic.logThis 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 the documentation for BOOKS-CERTIFICATION.
saved_acl2(from step 3) and access to certified community books (from step 4). Enjoy!
Note: To build variants of ACL2, see the documentation topic REAL for ACL2(r) and COMPILING-ACL2P for ACL2(p).