/usr/share/acl2-6.3/books/hacking/evalable-ld-printing.cert is in acl2-books-certs 6.3-5.
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 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
NIL
(("/usr/share/acl2-6.3/books/hacking/evalable-ld-printing.lisp" "evalable-ld-printing" "evalable-ld-printing" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS (:EVALABLE-LD-PRINTING "/usr/share/acl2-6.3/books/hacking/evalable-ld-printing.lisp"))) . 307404439) ("/usr/share/acl2-6.3/books/hacking/raw.lisp" "raw" "raw" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1732285021) ("/usr/share/acl2-6.3/books/hacking/defstruct-parsing.lisp" "defstruct-parsing" "defstruct-parsing" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1553047268) ("/usr/share/acl2-6.3/books/hacking/subsumption.lisp" "subsumption" "subsumption" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 560393729) ("/usr/share/acl2-6.3/books/hacking/defcode.lisp" "defcode" "defcode" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS (:DEFCODE "/usr/share/acl2-6.3/books/hacking/progn-bang-enh.lisp" "/usr/share/acl2-6.3/books/hacking/defcode.lisp"))) . 1845433737) ("/usr/share/acl2-6.3/books/hacking/progn-bang-enh.lisp" "progn-bang-enh" "progn-bang-enh" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS (:DEFCODE "/usr/share/acl2-6.3/books/hacking/progn-bang-enh.lisp"))) . 737908112) ("/usr/share/acl2-6.3/books/hacking/hacker.lisp" "hacker" "hacker" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 197252797) ("/usr/share/acl2-6.3/books/hacking/doc-section.lisp" "doc-section" "doc-section" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1293647265) ("/usr/share/acl2-6.3/books/misc/evalable-printing.lisp" "misc/evalable-printing" "evalable-printing" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 143365839))
121177385
|