Readme.lspfile in its top-level directory. Each
Readme.lspshould 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
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
"directory_path" is the pathname to the directory containing
(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