From: Matt Kaufmann
Subject: next ACL2 seminar: book distribution

Hi --

In this coming Wednesday's ACL2 seminar, we'll start with an extended
roundtable as is usual now for the first Wednesday.  However, we'll
try to make the roundtable relatively quick so that we have time to
discuss the topic of ACL2 book distribution.

That topic comes up from time to time, but there's been little
progress in producing a clear plan for improving the structure,
documentation, distribution, and contribution of distributed books.
I'm most open to crisp, worked-out ideas for improving the situation,
especially in ways that you think would improve user productivity
(especially yours!) with ACL2.

So I invite you to come to the seminar with reasonably explicit
suggestions on what to change in the ACL2 book distribution mechanism.
Naturally, I'm especially interested in specific suggestions that have
large benefit for relatively little effort, or at least relatively
little effort for the ACL2 implementors!

Here's some relevant background.

Currently, ACL2 books are distributed under the books/ directory,
except that the workshop/ books need to be downloaded separately if
they're desired.  There are some workshop books that could be useful
for other applications.  What's more, it looks like Rockwell will soon
release many of their very nice books (with what I consider a rather
complex Makefile system).  And it's also worth mentioning that some
have been contributing books (following instructions in
http://www.cs.utexas.edu/users/moore/acl2/books/index.html), but I
know there's more good stuff out there that people could contribute.

Regarding the new Rockwell books that I expect soon: A simple way to
incorporate them would be as a separate directory.  But for example,
Eric Smith has his own enhancements of those.  So we might have
books/rockwell/rel1/ and books/rockwell/rel1-e/.  But the "rel" idea
could be asking for trouble.

Here are some aspects that I think are very important for whatever we
come up with.

- Portability: Users should be able to use books on any platform
  supported by ACL2.

- Simplicity: It may well be more disruptive to users than helpful
  (and time-consuming for me!) if version control systems are
  involved, if there is a complex set of tarballs to choose from, or
  if users are required to install software other than Lisp and ACL2.

- Maintainability: It is highly desirable (to me!) that I be able to
  certify the books and diagnose failures in a reliable, simple way,
  as is the case today.  More parallelism would be nice but isn't as
  important as ruggedness.

- Effective submission process: It should be easy for users to
  contribute books.  I'd prefer that J and I not to be in a position
  where we have to choose which books are more "worthy" than other
  books.  The current submission mechanism basically allows anyone to
  contribute a book who follows the instructions (see URL above).

- Ease of use: The current process involves a Readme.lsp file with
  keywords, which was intended to allow implementation of an easy way
  for a user to search for potentially useful books.  But most
  existing directories don't have Readme.lsp files, and maybe there
  are better ways to search anyhow.

- Value-added: There is a long list of pending ACL2 features requested
  by users, so if the plan requires significant time by the ACL2
  implementors, the payoff needs to be relatively significant.

Thanks --
-- Matt