/usr/share/acl2-6.3/books/paco/paco.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 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 | #|
; Instructions for rebuilding Paco:
cd /u/moore/paco
make tags - make the tags file
make clean - delete .cert, etc., files
make - recertify as necessary
; ---------------------------------------------------------------------------
; To load
V27
:paco ; load load paco (if unloaded) and switch to PACO pkg
; "paco.boot" goes a little further and loads "ptrace.lisp" and cheats
; to make paco::prove look Common Lisp compliant.
v27
(value :q)
(load "paco.boot")
(lp)
(in-package "PACO")
; ---------------------------------------------------------------------------
; To test
(ld ;; newline to fool dependency scanner
"books/proveall.lisp" :ld-pre-eval-print t)
; ---------------------------------------------------------------------------
; To change the "PACO" package definition
; Edit the defpkg in utilities.acl2.
; ---------------------------------------------------------------------------
; To play
; Load all but the last form in utilities.acl2 and then these files
(include-book "utilities")
(include-book "foundations")
(include-book "type-set")
(include-book "rewrite")
(include-book "simplify")
(include-book "induct")
(include-book "prove")
(include-book "database")
; ---------------------------------------------------------------------------
|#
(in-package "PACO")
; This file is actually empty! The portculis, set up by paco.acl2,
; includes "database", which includes "prove", etc.
|