The ACL2 theorem proving environment consists of two parts: The ACL2 System and The ACL2 Books. This repository contains both.
The included version of the ACL2 System is the latest, under-development version of the ACL2 Theorem Prover. It is updated only by the ACL2 authors, Matt Kaufmann and J Moore.
WARNING: The ACL2 System authors consider the snapshots of the system in this repository to be experimental; they may be incomplete, fragile, and unable to pass our own regression. If you want a stable system, you should instead download an official, released version of ACL2 from the ACL2 Home Page.
The books/ directory of this repository comprises the Community Books, which are the canonical collection of open-source libraries for the ACL2 System.
The Combined ACL2 + Books Manual has extensive documentation for many books, and also for ACL2 itself. You can follow a link on that page to download an offline copy. That manual corresponds to the most recent ACL2 release; there is also a reasonably up-to-date manual that corresponds to this repository.
You can download a gzipped tarfile or zip file for the latest release, which includes the ACL2 system and the community books. Simply click on the "release" button at the top of github.com/acl2/acl2. Alternatively you get a copy from git as follows:
git clone git://github.com/acl2/acl2 acl2; cd acl2; git checkout -b acl2-7.4-local-branch v7.4
Your current directory is now a copy of ACL2 Version 7.4. Please see the ACL2 home page, specifically its installation instructions, for how to build an executable and certify books in your new directory.
To check out the latest development branch of the repository omit the last checkout command using git, run:
git clone git://github.com/acl2/acl2
See the documentation for how to contribute.
Even though we have merged the Community Books (formerly acl2-books) and
ACL2 System (formerly acl2-devel) repositories into one, changes should
be made only to the books/ subdirectory unless you are Matt Kaufmann
or J Moore, since everything outside books/ is part of the ACL2
system. (If you have suggestions for system changes, they should be
emailed to Matt or J, as has been done
in the past.)
We invite anyone who is using this repository to join the acl2-books mailing list, which receives commit messages and other discussion related to ACL2 system- and book-related development.
Everyone can contribute documentation and advice to our wiki and discuss problems and feature requests.
If you would like to contribute to this repository, see the documentation topic git-quick-start. Please note the guidelines for book development.