/usr/share/acl2-7.1/books/tools/plev-ccl.lisp is in acl2-books-source 7.1-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 | (in-package "ACL2")
(include-book "plev")
(include-book "include-raw")
(include-book "xdoc/top" :dir :system)
; The following is already in plev.lisp.
; (defpointer plev-info plev)
(defun plev-info ()
(declare (xargs :guard t))
(er hard? 'plev-info "raw lisp definition not installed?"))
(defttag plev-ccl)
(include-raw "plev-ccl-raw.lsp")
|