2 # $Id$ |
2 # $Id$ |
3 # |
3 # |
4 # IsaMakefile for HOLCF |
4 # IsaMakefile for HOLCF |
5 # |
5 # |
6 |
6 |
7 #### Base system |
7 ## targets |
8 |
8 |
|
9 default: HOLCF |
|
10 images: HOLCF IOA |
|
11 test: HOLCF-IMP HOLCF-ex IOA-ABP IOA-NTP |
|
12 all: images test |
|
13 |
|
14 |
|
15 ## global settings |
|
16 |
|
17 SRC = $(ISABELLE_HOME)/src |
9 OUT = $(ISABELLE_OUTPUT) |
18 OUT = $(ISABELLE_OUTPUT) |
10 LOG = $(OUT)/log |
19 LOG = $(OUT)/log |
11 |
20 |
12 THYS = Porder.thy Porder0.thy Pcpo.thy \ |
|
13 Fun1.thy Fun2.thy Fun3.thy \ |
|
14 Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \ |
|
15 Cprod1.thy Cprod2.thy Cprod3.thy \ |
|
16 Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \ |
|
17 Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \ |
|
18 Up1.thy Up2.thy Up3.thy Fix.thy \ |
|
19 One.thy Tr.thy\ |
|
20 Discrete0.thy Discrete1.thy Discrete.thy\ |
|
21 Lift1.thy Lift2.thy Lift3.thy Lift.thy HOLCF.thy |
|
22 |
21 |
23 ONLYTHYS = |
22 ## HOLCF |
24 |
23 |
25 FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) adm.ML \ |
24 HOLCF: HOL $(OUT)/HOLCF |
26 holcf_logic.ML cont_consts.ML \ |
|
27 domain/library.ML domain/syntax.ML domain/axioms.ML \ |
|
28 domain/theorems.ML domain/extender.ML domain/interface.ML |
|
29 |
25 |
30 $(OUT)/HOLCF: $(OUT)/HOL $(FILES) |
26 HOL: |
|
27 @cd $(SRC)/HOL; $(ISATOOL) make HOL |
|
28 |
|
29 $(OUT)/HOLCF: $(OUT)/HOL Cfun1.ML Cfun1.thy Cfun2.ML Cfun2.thy \ |
|
30 Cfun3.ML Cfun3.thy Cont.ML Cont.thy Cprod1.ML Cprod1.thy Cprod2.ML \ |
|
31 Cprod2.thy Cprod3.ML Cprod3.thy Discrete.ML Discrete.thy Discrete0.ML \ |
|
32 Discrete0.thy Discrete1.ML Discrete1.thy Fix.ML Fix.thy Fun1.ML \ |
|
33 Fun1.thy Fun2.ML Fun2.thy Fun3.ML Fun3.thy HOLCF.ML HOLCF.thy Lift.ML \ |
|
34 Lift.thy Lift1.ML Lift1.thy Lift2.ML Lift2.thy Lift3.ML Lift3.thy \ |
|
35 One.ML One.thy Pcpo.ML Pcpo.thy Porder.ML Porder.thy Porder0.ML \ |
|
36 Porder0.thy ROOT.ML Sprod0.ML Sprod0.thy Sprod1.ML Sprod1.thy \ |
|
37 Sprod2.ML Sprod2.thy Sprod3.ML Sprod3.thy Ssum0.ML Ssum0.thy Ssum1.ML \ |
|
38 Ssum1.thy Ssum2.ML Ssum2.thy Ssum3.ML Ssum3.thy Tr.ML Tr.thy Up1.ML \ |
|
39 Up1.thy Up2.ML Up2.thy Up3.ML Up3.thy adm.ML cont_consts.ML \ |
|
40 domain/axioms.ML domain/extender.ML domain/interface.ML \ |
|
41 domain/library.ML domain/syntax.ML domain/theorems.ML holcf_logic.ML |
31 @$(ISATOOL) usedir -b $(OUT)/HOL HOLCF |
42 @$(ISATOOL) usedir -b $(OUT)/HOL HOLCF |
32 |
43 |
33 $(OUT)/HOL: |
44 |
34 @cd ../HOL; $(ISATOOL) make |
45 ## HOLCF-IMP |
|
46 |
|
47 HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz |
|
48 |
|
49 $(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/Denotational.ML \ |
|
50 IMP/Denotational.thy IMP/ROOT.ML |
|
51 @$(ISATOOL) usedir $(OUT)/HOLCF IMP |
35 |
52 |
36 |
53 |
|
54 ## HOLCF-ex |
37 |
55 |
38 #### Tests and examples |
56 HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz |
39 |
57 |
40 ## IOA meta theory and examples |
58 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Dagstuhl.ML ex/Dagstuhl.thy \ |
|
59 ex/Dnat.ML ex/Dnat.thy ex/Fix2.ML ex/Fix2.thy ex/Focus_ex.ML \ |
|
60 ex/Focus_ex.thy ex/Hoare.ML ex/Hoare.thy ex/Loop.ML ex/Loop.thy \ |
|
61 ex/ROOT.ML ex/Stream.ML ex/Stream.thy ex/loeckx.ML |
|
62 @$(ISATOOL) usedir $(OUT)/HOLCF ex |
41 |
63 |
42 |
64 |
43 IOA_FILES = IOA/ROOT.ML IOA/meta_theory/Traces.thy \ |
65 ## IOA |
|
66 |
|
67 IOA: HOLCF $(OUT)/IOA |
|
68 |
|
69 $(OUT)/IOA: $(OUT)/HOLCF IOA/ROOT.ML IOA/meta_theory/Traces.thy \ |
44 IOA/meta_theory/Asig.ML IOA/meta_theory/Asig.thy \ |
70 IOA/meta_theory/Asig.ML IOA/meta_theory/Asig.thy \ |
45 IOA/meta_theory/CompoScheds.thy IOA/meta_theory/CompoExecs.ML \ |
71 IOA/meta_theory/CompoScheds.thy IOA/meta_theory/CompoExecs.ML \ |
46 IOA/meta_theory/CompoTraces.thy IOA/meta_theory/CompoScheds.ML \ |
72 IOA/meta_theory/CompoTraces.thy IOA/meta_theory/CompoScheds.ML \ |
47 IOA/meta_theory/CompoTraces.ML IOA/meta_theory/Sequence.ML \ |
73 IOA/meta_theory/CompoTraces.ML IOA/meta_theory/Sequence.ML \ |
48 IOA/meta_theory/Seq.thy IOA/meta_theory/RefCorrectness.thy \ |
74 IOA/meta_theory/Seq.thy IOA/meta_theory/RefCorrectness.thy \ |
52 IOA/meta_theory/IOA.thy IOA/meta_theory/IOA.ML \ |
78 IOA/meta_theory/IOA.thy IOA/meta_theory/IOA.ML \ |
53 IOA/meta_theory/Sequence.thy IOA/meta_theory/Automata.ML \ |
79 IOA/meta_theory/Sequence.thy IOA/meta_theory/Automata.ML \ |
54 IOA/meta_theory/CompoExecs.thy IOA/meta_theory/RefMappings.thy \ |
80 IOA/meta_theory/CompoExecs.thy IOA/meta_theory/RefMappings.thy \ |
55 IOA/meta_theory/RefCorrectness.ML IOA/meta_theory/Compositionality.ML \ |
81 IOA/meta_theory/RefCorrectness.ML IOA/meta_theory/Compositionality.ML \ |
56 IOA/meta_theory/Compositionality.thy |
82 IOA/meta_theory/Compositionality.thy |
|
83 @cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA |
57 |
84 |
58 |
85 |
59 IOA_ABP_FILES = IOA/ABP/Abschannel.thy \ |
86 ## IOA-ABP |
60 IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.ML \ |
87 |
61 IOA/ABP/Action.thy IOA/ABP/Check.ML \ |
88 IOA-ABP: IOA $(LOG)/IOA-ABP.gz |
62 IOA/ABP/Correctness.ML IOA/ABP/Correctness.thy \ |
89 |
63 IOA/ABP/Env.thy IOA/ABP/Impl.thy \ |
90 $(LOG)/IOA-ABP.gz: $(OUT)/IOA IOA/ABP/Abschannel.thy \ |
64 IOA/ABP/Impl_finite.thy IOA/ABP/Lemmas.ML \ |
91 IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.ML IOA/ABP/Action.thy \ |
65 IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \ |
92 IOA/ABP/Check.ML IOA/ABP/Correctness.ML IOA/ABP/Correctness.thy \ |
66 IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy \ |
93 IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \ |
67 IOA/ABP/Sender.thy IOA/ABP/Spec.thy |
94 IOA/ABP/Lemmas.ML IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \ |
|
95 IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \ |
|
96 IOA/ABP/Spec.thy |
|
97 @cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP |
68 |
98 |
69 |
99 |
70 IOA_NTP_FILES = IOA/NTP/Abschannel.ML \ |
100 ## IOA-NTP |
71 IOA/NTP/Abschannel.thy IOA/NTP/Action.ML \ |
|
72 IOA/NTP/Action.thy IOA/NTP/Correctness.ML \ |
|
73 IOA/NTP/Correctness.thy IOA/NTP/Impl.ML \ |
|
74 IOA/NTP/Impl.thy IOA/NTP/Lemmas.ML \ |
|
75 IOA/NTP/Lemmas.thy IOA/NTP/Multiset.ML \ |
|
76 IOA/NTP/Multiset.thy IOA/NTP/Packet.ML \ |
|
77 IOA/NTP/Packet.thy IOA/NTP/ROOT.ML \ |
|
78 IOA/NTP/Receiver.ML IOA/NTP/Receiver.thy \ |
|
79 IOA/NTP/Sender.ML IOA/NTP/Sender.thy \ |
|
80 IOA/NTP/Spec.thy |
|
81 |
101 |
82 |
102 IOA-NTP: IOA $(LOG)/IOA-NTP.gz |
83 $(OUT)/IOA: $(OUT)/HOLCF $(IOA_FILES) |
|
84 @cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA |
|
85 |
103 |
86 $(LOG)/IOA-ABP.gz: $(OUT)/IOA $(IOA_ABP_FILES) |
104 $(LOG)/IOA-NTP.gz: $(OUT)/IOA IOA/NTP/Abschannel.ML \ |
87 @cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP |
105 IOA/NTP/Abschannel.thy IOA/NTP/Action.ML IOA/NTP/Action.thy \ |
88 |
106 IOA/NTP/Correctness.ML IOA/NTP/Correctness.thy IOA/NTP/Impl.ML \ |
89 $(LOG)/IOA-NTP.gz: $(OUT)/IOA $(IOA_NTP_FILES) |
107 IOA/NTP/Impl.thy IOA/NTP/Lemmas.ML IOA/NTP/Lemmas.thy \ |
|
108 IOA/NTP/Multiset.ML IOA/NTP/Multiset.thy IOA/NTP/Packet.ML \ |
|
109 IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.ML \ |
|
110 IOA/NTP/Receiver.thy IOA/NTP/Sender.ML IOA/NTP/Sender.thy \ |
|
111 IOA/NTP/Spec.thy |
90 @cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP |
112 @cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP |
91 |
113 |
92 |
114 |
93 ## IMP |
115 ## clean |
94 |
|
95 IMP_THYS = IMP/Denotational.thy |
|
96 IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML) |
|
97 |
|
98 $(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF $(IMP_FILES) |
|
99 @$(ISATOOL) usedir $(OUT)/HOLCF IMP |
|
100 |
|
101 |
|
102 ## Miscellaneous examples |
|
103 |
|
104 EX_THYS = ex/Dnat.thy ex/Stream.thy \ |
|
105 ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy \ |
|
106 ex/Hoare.thy ex/Loop.thy |
|
107 |
|
108 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
|
109 |
|
110 $(LOG)/HOLCF-ex.gz: ex/ROOT.ML $(EX_FILES) |
|
111 @$(ISATOOL) usedir $(OUT)/HOLCF ex |
|
112 |
|
113 |
|
114 ## Full test |
|
115 |
|
116 ALL_TARGETS = $(OUT)/HOLCF $(OUT)/IOA $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \ |
|
117 $(LOG)/HOLCF-IMP.gz $(LOG)/HOLCF-ex.gz |
|
118 |
|
119 test: $(ALL_TARGETS) |
|
120 |
116 |
121 clean: |
117 clean: |
122 @rm -f $(ALL_TARGETS) |
118 @rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \ |
123 |
119 $(LOG)/HOLCF-ex.gz $(OUT)/IOA $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz \ |
124 |
120 $(LOG)/IOA-NTP.gz |
125 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF |
|