NOTE: A quicker and even easier install may be possible, by instead obtaining a pre-built binary distribution if one is available for your platform. Otherwise:
tar xfz acl2.tar.gz
http://acl2.org. In the latter case, stand in your new
acl2-sources/directory and execute the following to create a
tar xfz books-6.5.tar.gz
acl2-sources/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-sourcesdirectory for running ACL2, named
http://acl2.org. Further instructions are here.
books/if you skipped that step), for example with
make regressionor something fancier such as:
(time nice make -j 8 ACL2=/u/smith/bin/acl2 regression) >& make-regression.logThe resulting log file,
make-regression.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 5) and access to certified community books (from step 7). Enjoy!