ACL2 Version 7.3 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.
  1. Fetch a gzipped tar file from GitHub containing ACL2 Version 7.3 and the corresponding Community Books, which will download file acl2-7.3.tar.gz onto your system. Put that file in a directory whose pathname does not contain whitespace.
  2. Execute the following to create subdirectory acl2-7.3/. (These installation instructions assume that you don't rename the new subdirectory, though you are welcome to do so.)
    tar xfz acl2-7.3.tar.gz
  3. Obtain a Common Lisp implementation if you don't already have one.
  4. Build by connecting to the new acl2-7.3/ 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>
    5. This will create a script in your acl2-7.3 directory for running ACL2, named saved_acl2.
  5. 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 less than 2 hours or much longer (perhaps 8 hours, perhaps even more), depending on your machine and host     Common Lisp. 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_acl2 (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