equal
deleted
inserted
replaced
2 # $Id$ |
2 # $Id$ |
3 # |
3 # |
4 # IsaMakefile for CTT |
4 # IsaMakefile for CTT |
5 # |
5 # |
6 |
6 |
|
7 ## targets |
|
8 |
|
9 default: CTT |
|
10 images: CTT |
|
11 test: CTT-ex |
|
12 all: images test |
|
13 |
|
14 |
|
15 ## global settings |
|
16 |
|
17 SRC = $(ISABELLE_HOME)/src |
7 OUT = $(ISABELLE_OUTPUT) |
18 OUT = $(ISABELLE_OUTPUT) |
8 LOG = $(OUT)/log |
19 LOG = $(OUT)/log |
9 |
20 |
10 FILES = ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \ |
|
11 Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML |
|
12 |
21 |
13 EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML |
22 ## CTT |
14 |
23 |
15 $(OUT)/CTT: $(OUT)/Pure $(FILES) |
24 CTT: Pure $(OUT)/CTT |
|
25 |
|
26 Pure: |
|
27 @cd $(SRC)/Pure; $(ISATOOL) make Pure |
|
28 |
|
29 $(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.ML Arith.thy \ |
|
30 Bool.ML Bool.thy CTT.ML CTT.thy ROOT.ML rew.ML |
16 @$(ISATOOL) usedir -b $(OUT)/Pure CTT |
31 @$(ISATOOL) usedir -b $(OUT)/Pure CTT |
17 |
32 |
18 $(OUT)/Pure: |
|
19 @cd ../Pure; $(ISATOOL) make |
|
20 |
33 |
21 $(LOG)/CTT-ex.gz: ex/ROOT.ML $(OUT)/CTT $(EX_FILES) |
34 ## CTT-ex |
|
35 |
|
36 CTT-ex: CTT $(LOG)/CTT-ex.gz |
|
37 |
|
38 $(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/elim.ML ex/equal.ML \ |
|
39 ex/synth.ML ex/typechk.ML |
22 @$(ISATOOL) usedir $(OUT)/CTT ex |
40 @$(ISATOOL) usedir $(OUT)/CTT ex |
23 |
41 |
24 test: $(OUT)/CTT $(LOG)/CTT-ex.gz |
42 |
|
43 ## clean |
25 |
44 |
26 clean: |
45 clean: |
27 @rm -f $(OUT)/CTT $(LOG)/CTT-ex.gz |
46 @rm -f $(OUT)/CTT $(LOG)/CTT.gz $(LOG)/CTT-ex.gz |
28 |
|
29 |
|
30 .PRECIOUS: $(OUT)/Pure $(OUT)/CTT |
|