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 the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. 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)
The ACL2 implementors plan to 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