This file is indexed.

/usr/share/acl2-6.3/books/tools/pack.lisp is in acl2-books-source 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
 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
(in-package "ACL2")

(mutual-recursion
 (defun pack-list (args)
   (declare (xargs :measure (acl2-count args)
                   :guard t
                   :verify-guards nil))
   (if (atom args)
       nil
     (if (atom (cdr args))
         (pack-tree (car args))
       (append (pack-tree (car args))
               (cons #\Space
                     (pack-list (cdr args)))))))
 (defun pack-tree (tree)
   (declare (xargs :measure (acl2-count tree)
                   :guard t))
   (if (atom tree)
       (if (or (acl2-numberp tree)
               (characterp tree)
               (stringp tree)
               (symbolp tree))
           (explode-atom tree 10)
         '(#\Space))
     (append (cons #\( (pack-tree (car tree)))
             (cons #\Space (pack-list (cdr tree)))
             (list #\))))))

(defun pack-term (args)
  (declare (xargs :guard t
                  :verify-guards nil))
  (intern (coerce (pack-list args) 'string) "ACL2"))

(defmacro pack (&rest args)
  `(pack-term (list ,@args)))