This is a call for ACL2 users to submit certifiable books, and to document
existing books, for future ACL2 distributions. Of course, we already
distribute quite a few certified books with ACL2, most of which were developed
by ACL2 users other than us; and, we already make available supporting books
from the ACL2 workshops. But we know that ACL2 users have developed many other
certifiable books.
Your contributions will serve several purposes.
1. The ACL2 implementors can update your books as necessary so that they
continue to certify in future ACL2 releases.
2. Your contributions can benefit other ACL2 users.
3. Your contributions can benefit ACL2 development by contributing to the
regression suite and to potential development of query tools.
Our plan is for future ACL2 distributions to include the currently-distributed
books, the workshop books, and additional books contributed in response to this
call. All will have the same "status", indexed by keywords provided by the
contributors. If there is sufficient interest, we might also include on the
web a tarball for each individual contribution together with a bare-bones
distribution in which books/ is empty.
Please see the following URL for directions on how to contribute books,
including creation of a Readme.lsp file with keywords:
http://www.cs.utexas.edu/users/moore/acl2/v2-9/new/books/
NOTE: If you have books that are already in the distribution, including
workshop books, these can be left unchanged, but we would very much appreciate
a suitable Readme.lsp file (follow the above link for explanation of
"suitable"). Moreover, we would appreciate any help for creating Readme.lsp
files for existing book directories in the current distributed or workshop
books, whether they are yours or not. For example, if you are familiar with
books/ihs/ then you could suggest keywords for books/ihs/Readme.lsp.
Matt and J