Contributing Books to ACL2

NEW!
See the home page for ACL2 books, a project that we hope will continue in the future, described in an email from Jared Davis.

See also the original email request for contributing books to ACL2.

Changes to this process are noted in CHANGELOG.html.

All contributed books will reside under directory books/. Conceptually, the ACL2 distributed books are to be partitioned into contributions. A contribution may be a single flat directory, but it may contain subdirectories. Although distinct contributions are disjoint, one may reside in a subdirectory of another (only rarely; typically, in the case that the subdirectories are old versions).

Below are the steps to follow to submit a book or collection of books. You may find it simplest first to start by looking at these two small examples (which may also be found in a gzipped tar file, examples.tar.gz).

examples/contrib1/
Flat directory example.
examples/contrib2/
Example with subdirectories.

Moreover, we have placed the entire ACL2 2.9.4 books/ directory here, with just a few updates with appropriate Readme.lsp files (as discussed below). Initially we have updated only books/arithmetic/Readme.lsp; we would very much appreciate other updates you care to send us, which we will incorporate into the next release and into this local copy of the ACL2 2.9.4 books/ directory. Note that the current ACL2 books directory is part of the current ACL2 release, available from the ACL2 home page.

1. Makefiles: You can probably produce Makefiles by modifying the examples listed above. But if you need a more complete spec, see :doc book-makefiles for the current ACL2 version. Make sure all books certify by typing make.

2. Include-book commands: When including any book that is not part of your submission, use :dir :system (so that we can move directories around). Do not use absolute pathnames. Avoid circular directory dependencies: for example, if some book in directory D1 includes some book in directory D2, then no book in directory D2 should include any book in directory D1.

3. Readme.lsp: Each top-level directory should have a Readme.lsp file of a very specific format. You can probably produce such files by modifying the examples listed above. For a more detailed spec, see the detailed instructions for Readme.lsp.

4. Checks:

Check that all parentheses are balanced, for example in emacs using meta-x find-unbalanced-parentheses as defined in file emacs/emacs-acl2.el in the ACL2 distribution.

In ACL2, please evaluate (include-book "misc/process-book-readme" :dir :system) and then run (process-book-readme :dir "DIR") where DIR is the top-level directory of your contribution, where you can just type (process-book-readme) if you are already standing in that directory.

5. Submission Process: To submit a contribution, send an email to Matt Kaufmann, kaufmann@cs.utexas.edu. Name the directory, and let us know if you feel it belongs under an existing subdirectory of books/.

6. Frequency: Feel free to submit contributions at any time. They will generally be integrated into the current ACL2 development directory, for inclusion in the next release.

7. Versions: It is up to the contributor to decide how to handle versions, generally by specifying one of the following:

replacement of an existing directory with the newly-submitted one;
addition of a new directory, renaming the old one; or
addition of a new directory that has a new name (typically, a subdirectory, named using a release number, of some main directory; see below).

For example, if you already have a directory vector-spaces/, and you come up with your first revision, then the possibilities above suggest, respectively:

replacing vector-spaces with the new version;
changing the name of the existing vector-spaces/ directory to vector-spaces-1.0/ and putting the new version in vector-spaces; or
[not applicable in this case] adding a new directory, vector-spaces/.

Of course, the last of these three doesn't make sense if vector-spaces/ already exists, so you might propose (for example) one of the following instead:

Create a new vector-spaces/directory, move the existing vector-spaces/ directory to vector-spaces/rel-1.0, and put the new contribution in vector-spaces/rel-2.0.
Move the old vector-spaces/ directory out of the way, put the new version in vector-spaces/, and finally move the old vector-spaces/ version to subdirectory rel-1.0/ of vector-spaces/.

Of course, it would have been best in this case (for backwards compatibility after this change) if the original contribution had been placed in vector-spaces/rel-1.0.

NOTE: New or revised contributions will be included with ACL2 releases. If you want users to know about contributions or revisions inbetween ACL2 releases, feel free to email the acl2 mailing list or acl2-help mailing list; and, we can put up a link to your page on the "Recent changes to this page" link of the ACL2 home page.

Last updated: Fri Feb 24 11:51:12 2006