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-7.4.tar.gzonto your system. Put that file in a directory whose pathname does not contain whitespace.
acl2-7.4/. (These installation instructions assume that you don't rename the new subdirectory, though you are welcome to do so.)
tar xfz acl2-7.4.tar.gz
acl2-7.4/directory and typing the following, which may take a few minutes to complete. Note: You will need Gnu make. We have seen problems on some Linux systems with Version 3.81 of that utility, so if you encounter errors, please consider our instructions for downloading and installing GNU make version 3.80.
acl2-7.4directory for running ACL2, 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, see the documentation for BOOKS-CERTIFICATION.
saved_acl2(from step 4) and access to certified community books (from step 5). Enjoy!