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.0. Then use either of the following two methods to obtain the ACL2 source code and community books.
acl2-8.0.tar.gzfrom GitHub and then execute:
tar xfz acl2-8.0.tar.gz
acl2-8.0. Connect to
git clone https://github.com/acl2/acl2 acl2-sources
acl2-sources. Connect to
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, see the documentation for BOOKS-CERTIFICATION.
saved_acl2(from step 3) and access to certified community books (from step 4). Enjoy!