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-0/
.acl2-sources/
:tar xfz acl2.tar.gz
acl2-sources/
directory.
acl2-sources/
to create
directory books/
: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.)
make LISP=<path_to_your_lisp_executable>
books/
directory. (Further
instructions are
here.)
make regressionThis may take a few hours; you can speed this up by specifying a value for
ACL2_JOBS
if you have an N-core
machine, N>1, for example as
follows. WARNING: if instead you use
`make
' option -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 6)
and access to certified community books (from step 8). Enjoy!