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.0.tar.gzon your system
acl2-7.0/. (These installation instructions assume that you don't rename that directory, though you are welcome to do so.)
tar xfz acl2-7.0.tar.gz
acl2-7.0/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.0directory 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 up to several hours. 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_acl2h(from step 4) and access to certified community books (from step 5). Enjoy!