2 # $Id$ |
2 # $Id$ |
3 # |
3 # |
4 # IsaMakefile for CCL |
4 # IsaMakefile for CCL |
5 # |
5 # |
6 |
6 |
|
7 ## targets |
|
8 |
|
9 default: CCL |
|
10 images: CCL |
|
11 test: CCL-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 SET_FILES = ROOT.ML Set.thy Set.ML subset.ML equalities.ML mono.ML \ |
|
11 Gfp.thy Gfp.ML Lfp.thy Lfp.ML |
|
12 |
21 |
13 CCL_FILES = CCL.thy CCL.ML Term.thy Term.ML Type.thy Type.ML \ |
22 ## CCL |
14 coinduction.ML Hered.thy Hered.ML Trancl.thy Trancl.ML \ |
|
15 Wfd.thy Wfd.ML genrec.ML typecheck.ML eval.ML Fix.thy Fix.ML |
|
16 |
23 |
17 EX_FILES = ex/ROOT.ML ex/Flag.ML ex/Flag.thy ex/List.ML ex/List.thy \ |
24 CCL: FOL $(OUT)/CCL |
18 ex/Nat.ML ex/Nat.thy ex/Stream.ML ex/Stream.thy |
25 |
|
26 FOL: |
|
27 @cd $(SRC)/FOL; $(ISATOOL) make FOL |
|
28 |
|
29 $(OUT)/CCL: $(OUT)/FOL CCL.ML CCL.thy Fix.ML Fix.thy Gfp.ML Gfp.thy \ |
|
30 Hered.ML Hered.thy Lfp.ML Lfp.thy ROOT.ML Set.ML Set.thy Term.ML \ |
|
31 Term.thy Trancl.ML Trancl.thy Type.ML Type.thy Wfd.ML Wfd.thy \ |
|
32 coinduction.ML equalities.ML eval.ML genrec.ML mono.ML subset.ML \ |
|
33 typecheck.ML |
|
34 @$(ISATOOL) usedir -b $(OUT)/FOL CCL |
19 |
35 |
20 |
36 |
21 $(OUT)/CCL: $(OUT)/FOL $(SET_FILES) $(CCL_FILES) |
37 ## CCL-ex |
22 @$(ISATOOL) usedir -b $(OUT)/FOL CCL |
|
23 |
38 |
24 $(OUT)/FOL: |
39 CCL-ex: CCL $(LOG)/CCL-ex.gz |
25 @cd ../FOL; $(ISATOOL) make |
|
26 |
40 |
27 $(LOG)/CCL-ex.gz: ex/ROOT.ML $(OUT)/CCL $(EX_FILES) |
41 $(LOG)/CCL-ex.gz: $(OUT)/CCL ex/Flag.ML ex/Flag.thy ex/List.ML \ |
|
42 ex/List.thy ex/Nat.ML ex/Nat.thy ex/ROOT.ML ex/Stream.ML ex/Stream.thy |
28 @$(ISATOOL) usedir $(OUT)/CCL ex |
43 @$(ISATOOL) usedir $(OUT)/CCL ex |
29 |
44 |
30 test: $(OUT)/CCL $(LOG)/CCL-ex.gz |
45 |
|
46 ## clean |
31 |
47 |
32 clean: |
48 clean: |
33 @rm -f $(OUT)/CCL $(LOG)/CCL-ex.gz |
49 @rm -f $(OUT)/CCL $(LOG)/CCL.gz $(LOG)/CCL-ex.gz |
34 |
|
35 |
|
36 .PRECIOUS: $(OUT)/FOL $(OUT)/CCL |
|