/usr/share/acl2-7.2dfsg/books/misc/process-book-readme.lisp is in acl2-books-source 7.2dfsg-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 | ; Copyright (C) 2013, Regents of the University of Texas
; Written by Matt Kaufmann (dates back to Feb., 2006 or earlier)
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
(in-package "ACL2")
(program)
(set-state-ok t)
(defun next-newline (str pos len)
; Return the position of the next newline character in str starting with pos,
; if any; else return len.
(cond ((int= pos len)
len)
((eql (char str pos) #\Newline)
pos)
(t (next-newline str (1+ pos) len))))
(defun break-string-into-lines-rec (str pos len acc)
; Break str into lines, discarding empty lines.
(cond ((int= pos len)
(reverse acc))
((eql (char str pos) #\Newline)
(break-string-into-lines-rec str (1+ pos) len acc))
(t (let ((new-pos (next-newline str pos len)))
(break-string-into-lines-rec str new-pos len
(cons (subseq str pos new-pos)
acc))))))
(defun find-whitespace-string (string-list)
(cond ((endp string-list)
nil)
((let* ((str (car string-list))
(len (length str)))
(or (member-char-stringp #\Space str (1- len))
(member-char-stringp #\Tab str (1- len))))
(car string-list))
(t (find-whitespace-string (cdr string-list)))))
(defun break-string-into-lines (str msg ctx state)
(let* ((lines (break-string-into-lines-rec str 0 (length str) nil))
(bad-line (find-whitespace-string lines)))
(cond (bad-line (er soft ctx
"Found ~@0 line with whitespace:~%~x1~|"
msg
bad-line))
(t (value lines)))))
(defun process-book-readme-fn (readme-filename state)
(declare (xargs :guard (stringp readme-filename)))
(let ((ctx 'process-book-readme))
(mv-let
(channel state)
(open-input-channel readme-filename :object state)
(cond
((null channel)
(er soft ctx
"Unable to open file ~x0 for input."
readme-filename))
(t (mv-let
(eofp alist state)
(read-object channel state)
(pprogn
(close-input-channel channel state)
(cond (eofp (er soft ctx
"No form could be read from input file ~x0."
readme-filename))
((not (and (true-list-listp alist)
(alistp (strip-cdrs alist))))
(er soft ctx
"The form read from a book's Readme.lsp file should be ~
an list of true lists each with at least two elements, ~
but ~X01 is not."
alist (abbrev-evisc-tuple state)))
(t (let* ((files-entry (assoc-eq :FILES alist))
(title-entry (assoc-eq :TITLE alist))
(author/s-entry (assoc-eq :AUTHOR/S alist))
(keywords-entry (assoc-eq :KEYWORDS alist))
(abstract-entry (assoc-eq :ABSTRACT alist))
(perm-entry (assoc-eq :PERMISSION alist))
(files (and (true-listp files-entry)
(eql (length files-entry) 2)
(stringp (cadr files-entry))
(cadr files-entry)))
(title (and (true-listp title-entry)
(eql (length title-entry) 2)
(stringp (cadr title-entry))
(cadr title-entry)))
(author/s (and (string-listp (cdr author/s-entry))
(cdr author/s-entry)))
(keywords (and (string-listp (cdr keywords-entry))
(cdr keywords-entry)))
(abstract (and (true-listp abstract-entry)
(eql (length abstract-entry) 2)
(stringp (cadr abstract-entry))
(cadr abstract-entry)))
(perm (and (true-listp perm-entry)
(eql (length perm-entry) 2)
(stringp (cadr perm-entry))
(cadr perm-entry))))
(cond
((not (and files title author/s keywords abstract perm))
(er soft ctx
"No valid field for ~x0 in Readme.lsp alist."
(cond
((not files) :FILES)
((not title) :TITLE)
((not author/s) :AUTHOR/S)
((not keywords) :KEYWORDS)
((not abstract) :ABSTRACT)
(t :PERMISSION))))
(t
(pprogn (fms "File ~s0 PASSES the check.~|"
(list (cons #\0 readme-filename))
(standard-co state) state nil)
(value :invisible))))))))))))))
(defmacro process-book-readme (&key dir)
(declare (xargs :guard (or (null dir)
(stringp dir))))
`(process-book-readme-fn
(concatenate
'string
(let ((dir ,dir))
(cond (dir
(cond ((eql (char dir (1- (length dir)))
*directory-separator*)
dir)
(t (concatenate 'string dir
*directory-separator-string*))))
(t (cbd))))
"Readme.lsp")
state))
; Last updated: Fri Feb 24 11:36:55 2006
|