acl2-books


Libraries for the ACL2 Theorem Prover

ACL2 Community Books

The Community Books are now included in the ACL2+books github repository at https://github.com/acl2/acl2. Please note that as before, the books/ directory may be edited by everyone in the project, but only the ACL2 authors should edit files outside books/.

We leave the old version of this page here for reference, and have made the repository "read-only".

```

```

The Community Books are the canonical collection of open-source libraries for the ACL2 theorem prover.

Documentation

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.

Download -- Latest Stable Release

You may wish to download a gzipped tarfile to use with ACL2 Version 6.5, or you can check out the books using Subversion. * For anonymous read-only access: svn checkout http://acl2-books.googlecode.com/svn/branches/6.5 <target_directory> * For read-write access, become a member of the project by contacting one of the project administrators. (We are listed on the left under Members; to un-obscure the addresses, click one, click the "..." again, and answer the captcha.) Then: svn checkout https://acl2-books.googlecode.com/svn/branches/6.5 <target> --username <name>

(Note that this uses https not http.) You will be prompted for a password the first time; the password that is required is different from your Google account password and may be found here.

Download -- Experimental Development Version

A bleeding-edge version of the books is available in the trunk of the repository. This version typically requires an experimental, development copy of ACL2, which you can get from the acl2-devel project. (When you check out acl2-devel, you will automatically get the latest trunk from acl2-books.)

Occasionally, updates from the trunk may be backported into release branches.

Searching and browsing the books

If you're looking for a particular library but can't remember where it is, you may want to search the trunk, which can be done from the Source tab above. You may also view recent changes or browse the repository through a web interface.

You may search or browse the trunk with Ohloh Code Search using the widgets below. Ohloh's version of the code may be a few days old. | <wiki:gadget url="http://www.ohloh.net/p/17163/widgets/project_search_code.xml" height="160" width="355" border="0"/> | <wiki:gadget url="http://www.ohloh.net/p/17163/widgets/project_browse_code.xml" height="170" width="355" border="0"/> | |:------------------------------------------------------------------------------------------------------------------------------|:------------------------------------------------------------------------------------------------------------------------------|

Contributors wanted!

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

If you would like to do book development (add documentation to the books, clean up the books, contribute new books), just email Jared Davis and ask him to add you to the project. See below if you would also like to join the mailing list. Please note the guidelines for book development.

We encourage all book developers, as well as anyone who would like to follow development of the books or the ACL2 system, to join the acl2-books mailing list, which also serves as the mailing list for the related acl2-devel project.

Project Information

Labels:
acl2 lisp theoremproving