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:
acl2/v6-1/
.acl2-sources/
:tar xfz acl2.tar.gz
acl2-sources/
directory; then execute the following
in acl2-sources/
to create
directory books/
:tar xfz books-6.1.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.)
make LISP=<path_to_your_lisp_executable>
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 ACL2_JOBS=8 ACL2=/u/smith/bin/acl2 regression) >& make-regression.logSee :DOC regression for explanation and further options, e.g. for using ACL2(h).
saved_acl2
(from step 5)
and access to certified community books (from step 7). Enjoy!