Note: We have been informed of a Slovenian translation of this page, created by NextRanks. Note that these links take you out of the ACL2 web space and are not under our control.
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
books/directory under your
acl2-sources/directory, preferably as follows: connect to your
acl2-sources/directory, then fetch the ACL2 community books as a tarball from the Google Code website, and finally execute the following to create subdirectory
tar xfz books-6.0.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. (Further instructions are here.)
make regressionThis may take a few hours; you can speed this up by specifying a value for
ACL2_JOBSif you have an N-core machine, N>1, for example as follows. WARNING: if instead you use `
-j, you will not see parallel certification for books in the ~c[centaur/] directory.
make regression ACL2_JOBS=8If your system has difficulty certifying the books in the ~c[centaur/] directory, say because of issues with Perl, you can skip them by specifying
ACL2_CENTAUR=skip, for example as follows.
make regression ACL2_CENTAUR=skip
saved_acl2(from step 5) and access to certified community books (from step 7). Enjoy!