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
acl2-sources/directory; then execute the following in
acl2-sources/to create a
tar xfz books-6.4.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 rare problems 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
books/directory (but first create
books/if you skipped that step). 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!