ACL2 Version 4.1 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 Linux/Unix/MacOS

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/v4-1/.
  2. Execute the following to create directory acl2-sources/:
    tar xfz acl2.tar.gz
  3. Obtain a Common Lisp implementation if you don't already have one.
  4. 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>
  5. Certify books (this may take a few hours; you can speed this up with the option -j N if you have an N-core machine, N>1):
    make regression
You now have an ACL2 executable called saved_acl2 (from step 4) and access to certified distributed books (from step 5). Enjoy!

Note: There are many other books available from ACL2 workshops, available here.


More Information