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 directory
tar xfz books-6.3.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 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. (That said, in builds with Allegro Common Lisp we have seen problems certifying books with GNU make version 3.80 that seemed to be solved with version 3.81.)
books/directory (but first create
books/if you skipped that step). Further instructions are here.
books/if you skipped that step), for example as follows.
make regression (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!