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
56
57
58
59
60
|
include ../Makefile-generic
# Unfortunately, we cannot certify top-with-meta until we have completed
# certification in the meta/ directory. So we set BOOKS so that
# top-with-meta.cert is not made by default. The ":=" makes the assignment
# non-recursive.
BOOKS := $(filter-out top-with-meta,$(BOOKS))
# Dependencies:
abs.cert: abs.lisp
abs.cert: top.cert
binomial.cert: binomial.lisp
binomial.cert: top.cert
binomial.cert: factorial.cert
binomial.cert: sumlist.cert
equalities.cert: equalities.lisp
equalities.cert: ../cowles/acl2-crg.cert
equalities.cert: equalities.acl2
factorial.cert: factorial.lisp
idiv.cert: idiv.lisp
idiv.cert: top.cert
inequalities.cert: inequalities.lisp
inequalities.cert: equalities.cert
mod-gcd.cert: mod-gcd.lisp
mod-gcd.cert: inequalities.cert
natp-posp.cert: natp-posp.lisp
natp-posp.cert: inequalities.cert
rational-listp.cert: rational-listp.lisp
rationals.cert: rationals.lisp
rationals.cert: inequalities.cert
rationals.cert: inequalities.cert
rationals.cert: mod-gcd.cert
sumlist.cert: sumlist.lisp
# Added manually:
top-with-meta.cert: top-with-meta.lisp
top-with-meta.cert: top.cert
top-with-meta.cert: ../meta/meta.cert
top.cert: top.lisp
top.cert: equalities.cert
top.cert: rational-listp.cert
# The following two are for the nonstd books (ACL2(r)) only.
# top.cert: realp.cert
# top.cert: real-listp.cert
top.cert: inequalities.cert
top.cert: natp-posp.cert
top.cert: rationals.cert
|
