|
1 # |
|
2 # $Id$ |
|
3 # |
|
4 # IsaMakefile for HOLCF |
|
5 # |
|
6 |
|
7 #### Base system |
|
8 |
|
9 OUT = $(ISABELLE_OUTPUT_DIR) |
|
10 |
|
11 THYS = Void.thy Porder.thy Pcpo.thy \ |
|
12 Fun1.thy Fun2.thy Fun3.thy \ |
|
13 Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \ |
|
14 Cprod1.thy Cprod2.thy Cprod3.thy \ |
|
15 Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \ |
|
16 Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \ |
|
17 Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy One.thy \ |
|
18 Tr1.thy Tr2.thy Lift1.thy Lift2.thy Lift2.thy HOLCF.thy |
|
19 |
|
20 FILES = ROOT.ML Porder0.thy $(THYS) $(THYS:.thy=.ML) |
|
21 |
|
22 $(OUT)/HOLCF: $(OUT)/HOL $(FILES) |
|
23 @$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu -c $(OUT)/HOL HOLCF |
|
24 @chmod -w $@ |
|
25 |
|
26 $(OUT)/HOL: |
|
27 @cd ../HOL; $(ISATOOL) make |
|
28 |
|
29 |
|
30 |
|
31 #### Tests and examples |
|
32 |
|
33 ## Miscellaneous examples |
|
34 |
|
35 EX_THYS = ex/Fix2.thy ex/Hoare.thy \ |
|
36 ex/Loop.thy |
|
37 |
|
38 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
|
39 |
|
40 test: ex/ROOT.ML $(OUT)/HOLCF $(EX_FILES) |
|
41 @$(ISATOOL) testdir $(OUT)/HOLCF ex |
|
42 |
|
43 |
|
44 ## Explicit domains |
|
45 |
|
46 EXPLICIT_DOMAINS_THYS = explicit_domains/Coind.thy explicit_domains/Dlist.thy \ |
|
47 explicit_domains/Dnat2.thy explicit_domains/Stream.thy \ |
|
48 explicit_domains/Dagstuhl.thy explicit_domains/Dnat.thy \ |
|
49 explicit_domains/Focus_ex.thy explicit_domains/Stream2.thy |
|
50 |
|
51 EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS) \ |
|
52 $(EXPLICIT_DOMAINS_THYS:.thy=.ML) |
|
53 |
|
54 test2: explicit_domains/ROOT.ML $(OUT)/HOLCF $(EXPLICIT_DOMAINS_FILES) |
|
55 @$(ISATOOL) testdir $(OUT)/HOLCF explicit_domains |
|
56 |
|
57 |
|
58 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF |