equal
deleted
inserted
replaced
3 # |
3 # |
4 # IsaMakefile for CTT |
4 # IsaMakefile for CTT |
5 # |
5 # |
6 |
6 |
7 OUT = $(ISABELLE_OUTPUT) |
7 OUT = $(ISABELLE_OUTPUT) |
|
8 LOG = $(OUT)/log |
8 |
9 |
9 FILES = ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \ |
10 FILES = ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \ |
10 Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML |
11 Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML |
11 |
12 |
12 EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML |
13 EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML |
15 @$(ISATOOL) usedir -b $(OUT)/Pure CTT |
16 @$(ISATOOL) usedir -b $(OUT)/Pure CTT |
16 |
17 |
17 $(OUT)/Pure: |
18 $(OUT)/Pure: |
18 @cd ../Pure; $(ISATOOL) make |
19 @cd ../Pure; $(ISATOOL) make |
19 |
20 |
20 test: ex/ROOT.ML $(OUT)/CTT $(EX_FILES) |
21 $(LOG)/CTT-ex.gz: ex/ROOT.ML $(OUT)/CTT $(EX_FILES) |
21 @$(ISATOOL) usedir $(OUT)/CTT ex |
22 @$(ISATOOL) usedir $(OUT)/CTT ex |
22 |
23 |
|
24 test: $(OUT)/CTT $(LOG)/CTT-ex.gz |
|
25 |
|
26 clean: |
|
27 @rm -f $(OUT)/CTT $(LOG)/CTT-ex.gz |
|
28 |
|
29 |
23 .PRECIOUS: $(OUT)/Pure $(OUT)/CTT |
30 .PRECIOUS: $(OUT)/Pure $(OUT)/CTT |