|
2494
|
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
|