ACL2 Version 6.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.

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.


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-0/.
  2. Execute the following to create directory acl2-sources/:
    tar xfz acl2.tar.gz
  3. Create a 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 books/:
    tar xfz books-6.0.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 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>
    
  6. OPTIONAL: Download gzipped tarfiles for workshops books and/or nonstd books from the Google Code website into the books/ directory. (Further instructions are here.)
  7. Certify books:
    make regression
    
    This 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=8
    
    If 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
    
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