/usr/share/acl2-4.3/books/fix-cert/test-fix-cert0.lisp is in acl2-books-source 4.3-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 | (in-package "ACL2")
(include-book "fix-cert")
(defttag :test-fix-cert)
(progn!
;(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"))
|