/usr/share/acl2-8.0dfsg/books/make-event/read-from-file.lisp is in acl2-books-source 8.0dfsg-1.
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 | ; Copyright (C) 2013, Regents of the University of Texas
; Written by Matt Kaufmann
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; The following example shows how to create events by reading a file. It was
; constructed in response to a potential application suggested by David Rager
; and Sandip Ray.
; File read-from-file-data.lsp has the following three forms.
#|
3
a
(x y)
|# ;|
(in-package "ACL2")
; Notice that this inclue-book can be local, even though the make-event just
; after it refers to read-list. That's because this make-event had a default
; :check-expansion field of nil, so expansion is suppressed during subsequent
; include-books.
(local (include-book "misc/file-io" :dir :system))
(make-event
(er-let* ((file-contents (read-list (our-merge-pathnames
(cbd)
"read-from-file-data.lsp")
'top-level
state)))
(value `(defconst *obtained-from-file*
',file-contents))))
(defthm got-it-right
(equal *obtained-from-file*
'(3
a
(x y)))
:rule-classes nil)
; The following two succeed even though misc/file-io is included locally,
; because there is a local around the make-event, so that the make-event is
; skipped entirely on the second pass.
(local
(make-event
(er-let* ((file-contents (read-list (our-merge-pathnames
(cbd)
"read-from-file-data.lsp")
'top-level
state)))
(value `(defconst *obtained-from-file-again*
',file-contents)))
:check-expansion
(defconst *obtained-from-file-again*
'(3
a
(x y))))
)
(local
(make-event
(er-let* ((file-contents (read-list (our-merge-pathnames
(cbd)
"read-from-file-data.lsp")
'top-level
state)))
(value `(defconst *obtained-from-file-again*
',file-contents)))
:check-expansion
t)
)
; We remedy the potential problem of local include-book, mentioned above, by
; doing a non-local include-book of "file-io".
(include-book "misc/file-io" :dir :system)
; Next, using :check-expansion t, we cause a check at include-book time that
; the data file hasn't changed since certify-book time. A fun thing to do is
; to modify read-from-file-data-mod.lsp after the book is certified and then
; watch the include-book fail.
(encapsulate
()
; For the following expansion it is critical that proofs are enabled during
; evaluation of the expansion result when :check-expansion is not nil.
; Very Technical Remark: Otherwise, the second pass of this encapsulate will
; cause the :check-expansion to fail because chk-embedded-event-form returns
; nil for local events done under ld-skip-proofsp = 'include-book. See call of
; do-proofs? in make-event-fn in the ACL2 sources.
(make-event
(er-let* ((file-contents (read-list (our-merge-pathnames
(cbd)
"read-from-file-data.lsp")
'top-level
state)))
(value `(local (defun foo ()
',file-contents))))
:check-expansion
t)
)
(make-event
(er-let* ((file-contents (read-list (our-merge-pathnames
(cbd)
"read-from-file-data.lsp")
'top-level
state)))
(value `(defconst *obtained-from-file-again*
',file-contents)))
:check-expansion
(defconst *obtained-from-file-again*
'(3
a
(x y))))
|