/usr/share/acl2-8.0dfsg/books/acl2s/mode-acl2s-dependencies.lisp is in acl2-books-source 8.0dfsg-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 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 | #|$ACL2s-Preamble$;
(ld ;; Newline to fool ACL2/cert.pl dependency scanner
"acl2s/package.lsp" :dir :system)
(include-book ;; Newline to fool ACL2/cert.pl dependency scanner
"std/portcullis" :dir :system)
; cert-flags: ? t :ttags :all
(begin-book t :ttags :all);$ACL2s-Preamble$|#
;; Note: This book just gathers in one place all ACL2 books
;; that need to be certified for acl2s-mode to be used in emacs.
(in-package "ACL2")
(include-book "misc/expander" :dir :system)
(include-book "misc/bash" :dir :system)
(include-book "ordinals/lexicographic-ordering" :dir :system)
(include-book "hacking/all" :dir :system :ttags :all)
(include-book "hacking/evalable-ld-printing" :dir :system :ttags :all)
(include-book "make-event/inline-book" :dir :system)
(include-book "make-event/defconst-fast" :dir :system)
(include-book "misc/evalable-printing" :dir :system)
(include-book "misc/trace-star" :dir :system)
(include-book "coi/symbol-fns/symbol-fns" :dir :system)
(include-book "data-structures/utilities" :dir :system)
(include-book "tools/templates" :dir :system)
(include-book "tools/rulesets" :dir :system)
(include-book "coi/util/pseudo-translate" :dir :system)
(include-book "std/lists/top" :dir :system)
(include-book "std/alists/top" :dir :system)
(include-book "acl2s/cgen/top" :dir :system :ttags :all)
; Added for fixers support. [2016-02-19 Fri]
;; (make-event
;; (if ACL2S::*fixers-enabled*
;; '(progn
;; (include-book "centaur/gl/gl" :dir :system)
;; (include-book "centaur/satlink/top" :dir :system)
;; (include-book "centaur/gl/bfr-satlink" :dir :system :ttags :all)
;; (include-book "centaur/satlink/check-config" :dir :system))
;; '(value-triple :invisible)))
|