ACL2 Books Development

This site is for community-driven development for the basic ACL2 libraries, which deal with topics like arithmetic, data structures, and hardware modelling. We're working with the authors of ACL2 and our changes are eventually incorporated into official ACL2 releases.

Our latest and greatest

In order to download our development books, you'll need to have Subversion installed. You may either anonymously check out a read-only copy of the code, or become a project member and check out a read-write version.

To get a version of the books that work with ACL2 3.5, run:

svn checkout http://acl2-books.googlecode.com/svn/branches/3.5 <target_directory>

for anonymous read-only access, or use https:// instead of http:// for read-write access and use your googlecode.com password, which you can find here (this is not the same as your Google account password; it is specifically for googlecode.com SVN repositories.)

A bleeding-edge version of the books is available in the trunk of the repository. There may be more books available in this version or more advanced versions of existing books, but they may not all work with the released version of ACL2.

In addition to making their own improvements, members are welcome to backport changes and new books from the trunk into release branches.

Searching the books

If you're looking for a particular library but can't remember where it is, you may want to search the trunk.

Contributors wanted!

Everyone can contribute documentation and advice to our Wiki and discuss problems and feature requests.

If you would like to be able to do book development (adding documentation to the books, cleaning up the books, contributing new books), you can join our mailing list and we'll make you an account.