This file is indexed.

/usr/share/acl2-6.3/books/models/y86-target.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
; Silly file to support ../../Makefile

(in-package "ACL2")
; cert_param: (hons-only)

#||
(include-book "arithmetic-5/top" :dir :system)
(include-book "arithmetic/top-with-meta" :dir :system)
(include-book "arithmetic/top" :dir :system)
(include-book "centaur/gl/gl" :dir :system)
(include-book "centaur/misc/memory-mgmt-logic" :dir :system)
(include-book "defexec/other-apps/records/records" :dir :system)
(include-book "misc/check-state" :dir :system)
(include-book "misc/defp" :dir :system)
(include-book "rtl/rel8/lib/top" :dir :system)
(include-book "std/lists/list-defuns" :dir :system)
(include-book "tools/bstar" :dir :system)
||#