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.1. Then use either of the following two methods to obtain the ACL2 source code and community books.
acl2-8.1.tar.gzfrom GitHub and then execute:
tar xfz acl2-8.1.tar.gz
acl2-8.1. Connect to
git clone https://github.com/acl2/acl2 acl2-sources
acl2-sources. Connect to
make LISP=<path_to_your_lisp_executable>This will create a script in your connected directory for running ACL2. The script is named
make certify-booksor something fancier such as the following:
(time nice make -j 8 ACL2=/u/smith/bin/acl2 certify-books) >& make-certify-books.logThis may take less than 2 hours or much longer (perhaps 8 hours, perhaps even more), depending on your machine and host Common Lisp. The resulting log file,
make-certify-books.log, should contain no occurrences of the string ``CERTIFICATION FAILED''; a normal exit (status 0) should guarantee this. If you want additional explanation and further options (e.g., about perhaps avoiding root login), see the documentation for BOOKS-CERTIFICATION; for example, use of the target,
basic, as in
cd books ; make -j 8 ACL2=<path_to_acl2> basicwill take considerably less time (perhaps as little as 5 minutes instead of several hours) than using the target
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).