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-input.lsp" :ld-pre-eval-print t)
; ---------------------------------------------------------------------------
; To change the "PACO" package definition
; Edit the defpkg in package.lsp.
; ---------------------------------------------------------------------------
; 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.
|
