/usr/share/acl2-6.5/books/fix-cert/test-fix-cert0.lisp is in acl2-books-source 6.5-2.
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 | (in-package "ACL2")
(include-book "fix-cert")
(defttag :test-fix-cert)
(progn!
; The following assign was added by Matt K. after the addition of bookdata in
; 10/2013 (see :DOC bookdata). It seemed necessary; apparently some defpkg
; forms were placed into the top level of the world, but bookdata processing
; assumes that defpkg forms do not appear in a book.
(assign write-bookdata nil)
;(trace$ fix-cert-fn) ; for debugging
;(trace$ parse-book-name) ; for debugging
(fix-cert ("moved/test1bb" "moved/test1bp"))
(fix-cert '("moved/test1pp" "moved/test1pb"))
(fix-cert "moved/test1b")
(fix-cert "moved/test1p")
(fix-cert "moved/test1")
(fix-cert "moved/test2"))
|