Directions for Readme.lsp file for Books Contributed to ACL2

Each submission should include a Readme.lsp file in its top-level directory. Each Readme.lsp should consist entirely of plain ascii, such that ACL2 can read one form from the file (which may be preceded by lisp comments and followed by arbitrary text of your choice). That form should be an alist with the keys indicated by the example below.

((:FILES "
.:
Makefile
Readme.lsp
fs.lisp
fs-helper.lisp
") ; a single string with files listed as with Unix command "-ls -1R"
 (:TITLE    "Finite Set Theory in ACL2")
 (:AUTHOR/S "Joe User" "Aunt Acid")     ; non-empty list of author strings
 (:KEYWORDS
  "verification" "set theory") ; non-empty list of keywords, case-insensitive
 (:ABSTRACT
"In this book we provide the functions
foo, bar and mumble and a bunch of
lemmas about them.")
  (:PERMISSION ; author/s permission for distribution and copying:
"Sets Library for ACL2
Copyright (C) 2006 Joe User and Aunt Acid

This program is free software; you can redistribute it and/or modify
it under the terms of Version 2 of the GNU General Public License as
published by the Free Software Foundation.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
02110-1301, USA."))

You are welcome to provide a different :PERMISSION field, provided it permits we, the ACL2 implementors, to distribute modified copies, for example so that they certify in future ACL2 versions. We will attempt to make such modifications, but we may ask the submitters to help us out on occasion. Our experience with the workshop contributions is that we have only rarely, if ever, asked for such assistance.

Here is the general form of the association list shown above, where the three indicated lists are to be non-empty. An additional :VERSION field is optional (a string); feel free to suggest others.

((:FILES      string-containing-recursive-directory-listing)
 (:TITLE      title-string)
 (:AUTHOR/S . nonempty-author-string-list)
 (:KEYWORDS . nonempty-keyword-string-list)
 (:ABSTRACT   abstract-string)
 (:PERMISSION permission-string))
To obtain the string-containing-recursive-directory-listing, simply connect to the top-level directory of the contribution, submit the Unix command "ls -1R", edit the result to omit backup files and anything else you do not intend to include (such as subdirectories containing separate contributions, if any), and put the result inside double-quotation marks "...".

You can check the form of the above association list by running the following macro, defined in the book process-book-readme.lisp, where "directory_path" is the pathname to the directory containing the Readme.lsp file.

(process-book-readme :dir "directory_path")
; or, if you are already in the directory with the Readme.lsp file:
(process-book-readme)

Perhaps in the future, someone will build an index automatically from the list of keywords strings, titles, and top-level directory name, so we would greatly appreciate careful choices for these.


Last updated: Tue Feb 28 13:43:30 2006