ACL2 Version 7.0 Installation Guide
NOTE: From time to time we may provide so-called incremental
releases of ACL2. Please follow the recent changes
to this page link on the ACL2 home page for more
information.
Easy Install for Unix-like Systems
Here, "Unix-like Systems" includes Unix, GNU-Linux, and MacOS X. Note
that 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,
you can follow the directions below, which start by fetching a file
hosted at
the github ACL2
System and Books website. The result is a directory containing
not only the ACL2 system but, in the
books/ subdirectory,
the
community
books (libraries). The ACL2
system is developed at the
University of Texas at Austin
and
can also be
obtained or explored separately.
- Fetch a gzipped tar file from GitHub containing ACL2 Version 7.0 and the
corresponding Community Books, which will create file
acl2-7.0.tar.gz on your system.
Note: Avoid doing this in a directory
whose pathname contains whitespace.
- Execute the following to create subdirectory
acl2-7.0/.
(These installation instructions assume that you don't rename that
directory, though you are welcome to do so.)
tar xfz acl2-7.0.tar.gz
- Obtain a Common Lisp implementation if you don't
already have one.
- Build by connecting to the new
acl2-7.0/ directory
and typing the following, which may take a few minutes to complete.
Note: You will need Gnu make. We have seen
problems on some Linux systems 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.
make LISP=<path_to_your_lisp_executable>
This will create a script in your acl2-7.0
directory for running ACL2, named saved_acl2h.
- Certify books, for example with
make certify-books
or something fancier such as the following:
(time nice make -j 8 ACL2=/u/smith/bin/acl2 certify-books)>& make-certify-books.log
This may take up to several hours. The resulting log
file, make-certify-books.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.
You now have an ACL2 executable called
saved_acl2h (from step 4)
and access to certified community books (from step 5). Enjoy!
THE ABOVE INSTRUCTIONS MAY BE ALL THAT YOU
NEED. Otherwise, read on....
More Information