ACL2 Version 6.5 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: 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:

  1. Fetch acl2.tar.gz into a new directory, say acl2/v6-5/.
  2. Execute the following to create directory acl2-sources/:
    tar xfz acl2.tar.gz
  3. We strongly suggest that you fetch the ACL2 community books, for example via SVN from the Google Code acl2-books project website or as a gzipped tarfile from http://acl2.org. In the latter case, stand in your new acl2-sources/ directory and execute the following to create a books/ subdirectory:
    tar xfz books-6.5.tar.gz
  4. Obtain a Common Lisp implementation if you don't already have one.
  5. Build by connecting to your 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 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>
    6. This will create a script in your acl2-sources directory for running ACL2, named saved_acl2.
  6. OPTIONAL (and only if you obtained a gzipped tarfile above for the books instead of using SVN): Download a gzipped tarfile for the workshops books from http://acl2.org. Further instructions are here.
  7. Certify books (but first create books/ if you skipped that step), for example with 
    make regression
    or something fancier such as: 
    (time nice make -j 8 ACL2=/u/smith/bin/acl2 regression) >& make-regression.log
    The 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.
You now have an ACL2 executable called saved_acl2 (from step 5) and access to certified community books (from step 7). Enjoy!
THE ABOVE INSTRUCTIONS MAY BE ALL THAT YOU NEED. Otherwise, read on....

More Information