1 # |
|
2 # IsaMakefile for HOLCF |
|
3 # |
|
4 |
|
5 ## targets |
|
6 |
|
7 default: HOLCF |
|
8 images: HOLCF IOA |
|
9 test: \ |
|
10 HOLCF-FOCUS \ |
|
11 HOLCF-IMP \ |
|
12 HOLCF-Library \ |
|
13 HOLCF-Tutorial \ |
|
14 HOLCF-ex \ |
|
15 IOA-ABP \ |
|
16 IOA-NTP \ |
|
17 IOA-Storage \ |
|
18 IOA-ex |
|
19 all: images test |
|
20 |
|
21 |
|
22 ## global settings |
|
23 |
|
24 SRC = $(ISABELLE_HOME)/src |
|
25 OUT = $(ISABELLE_OUTPUT) |
|
26 LOG = $(OUT)/log |
|
27 |
|
28 |
|
29 ## HOLCF |
|
30 |
|
31 HOLCF: HOL $(OUT)/HOLCF |
|
32 |
|
33 HOL: |
|
34 @cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL |
|
35 |
|
36 $(OUT)/HOLCF: $(OUT)/HOL \ |
|
37 ROOT.ML \ |
|
38 Adm.thy \ |
|
39 Algebraic.thy \ |
|
40 Bifinite.thy \ |
|
41 Cfun.thy \ |
|
42 CompactBasis.thy \ |
|
43 Completion.thy \ |
|
44 Cont.thy \ |
|
45 ConvexPD.thy \ |
|
46 Cpodef.thy \ |
|
47 Cprod.thy \ |
|
48 Discrete.thy \ |
|
49 Deflation.thy \ |
|
50 Domain.thy \ |
|
51 Domain_Aux.thy \ |
|
52 Fixrec.thy \ |
|
53 Fix.thy \ |
|
54 Fun_Cpo.thy \ |
|
55 HOLCF.thy \ |
|
56 Lift.thy \ |
|
57 LowerPD.thy \ |
|
58 Map_Functions.thy \ |
|
59 One.thy \ |
|
60 Pcpo.thy \ |
|
61 Plain_HOLCF.thy \ |
|
62 Porder.thy \ |
|
63 Powerdomains.thy \ |
|
64 Product_Cpo.thy \ |
|
65 Sfun.thy \ |
|
66 Sprod.thy \ |
|
67 Ssum.thy \ |
|
68 Tr.thy \ |
|
69 Universal.thy \ |
|
70 UpperPD.thy \ |
|
71 Up.thy \ |
|
72 Tools/cont_consts.ML \ |
|
73 Tools/cont_proc.ML \ |
|
74 Tools/holcf_library.ML \ |
|
75 Tools/Domain/domain.ML \ |
|
76 Tools/Domain/domain_axioms.ML \ |
|
77 Tools/Domain/domain_constructors.ML \ |
|
78 Tools/Domain/domain_induction.ML \ |
|
79 Tools/Domain/domain_isomorphism.ML \ |
|
80 Tools/Domain/domain_take_proofs.ML \ |
|
81 Tools/cpodef.ML \ |
|
82 Tools/domaindef.ML \ |
|
83 Tools/fixrec.ML \ |
|
84 document/root.tex |
|
85 @$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF |
|
86 |
|
87 |
|
88 ## HOLCF-Tutorial |
|
89 |
|
90 HOLCF-Tutorial: HOLCF $(LOG)/HOLCF-Tutorial.gz |
|
91 |
|
92 $(LOG)/HOLCF-Tutorial.gz: $(OUT)/HOLCF \ |
|
93 Tutorial/Domain_ex.thy \ |
|
94 Tutorial/Fixrec_ex.thy \ |
|
95 Tutorial/New_Domain.thy \ |
|
96 Tutorial/document/root.tex \ |
|
97 Tutorial/ROOT.ML |
|
98 @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial |
|
99 |
|
100 |
|
101 ## HOLCF-Library |
|
102 |
|
103 HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz |
|
104 |
|
105 $(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \ |
|
106 Library/Defl_Bifinite.thy \ |
|
107 Library/List_Cpo.thy \ |
|
108 Library/Stream.thy \ |
|
109 Library/Sum_Cpo.thy \ |
|
110 Library/HOLCF_Library.thy \ |
|
111 Library/ROOT.ML |
|
112 @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library |
|
113 |
|
114 |
|
115 ## HOLCF-IMP |
|
116 |
|
117 HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz |
|
118 |
|
119 $(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \ |
|
120 IMP/Denotational.thy IMP/ROOT.ML IMP/document/root.tex |
|
121 @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP |
|
122 |
|
123 |
|
124 ## HOLCF-ex |
|
125 |
|
126 HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz |
|
127 |
|
128 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \ |
|
129 ../HOL/Library/Nat_Infinity.thy \ |
|
130 ex/Dagstuhl.thy \ |
|
131 ex/Dnat.thy \ |
|
132 ex/Domain_Proofs.thy \ |
|
133 ex/Fix2.thy \ |
|
134 ex/Focus_ex.thy \ |
|
135 ex/Hoare.thy \ |
|
136 ex/Letrec.thy \ |
|
137 ex/Loop.thy \ |
|
138 ex/Pattern_Match.thy \ |
|
139 ex/Powerdomain_ex.thy \ |
|
140 ex/ROOT.ML |
|
141 @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex |
|
142 |
|
143 |
|
144 ## HOLCF-FOCUS |
|
145 |
|
146 HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz |
|
147 |
|
148 $(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF \ |
|
149 Library/Stream.thy \ |
|
150 FOCUS/Fstreams.thy \ |
|
151 FOCUS/Fstream.thy FOCUS/FOCUS.thy \ |
|
152 FOCUS/Stream_adm.thy ../HOL/Library/Continuity.thy \ |
|
153 FOCUS/Buffer.thy FOCUS/Buffer_adm.thy |
|
154 @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS |
|
155 |
|
156 ## IOA |
|
157 |
|
158 IOA: HOLCF $(OUT)/IOA |
|
159 |
|
160 $(OUT)/IOA: $(OUT)/HOLCF IOA/ROOT.ML IOA/meta_theory/Traces.thy \ |
|
161 IOA/meta_theory/Asig.thy IOA/meta_theory/CompoScheds.thy \ |
|
162 IOA/meta_theory/CompoTraces.thy IOA/meta_theory/Seq.thy \ |
|
163 IOA/meta_theory/RefCorrectness.thy IOA/meta_theory/Automata.thy \ |
|
164 IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/IOA.thy \ |
|
165 IOA/meta_theory/Sequence.thy IOA/meta_theory/CompoExecs.thy \ |
|
166 IOA/meta_theory/RefMappings.thy IOA/meta_theory/Compositionality.thy \ |
|
167 IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy \ |
|
168 IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy \ |
|
169 IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy \ |
|
170 IOA/meta_theory/SimCorrectness.thy |
|
171 @cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA |
|
172 |
|
173 |
|
174 ## IOA-ABP |
|
175 |
|
176 IOA-ABP: IOA $(LOG)/IOA-ABP.gz |
|
177 |
|
178 $(LOG)/IOA-ABP.gz: $(OUT)/IOA IOA/ABP/Abschannel.thy \ |
|
179 IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.thy \ |
|
180 IOA/ABP/Check.ML IOA/ABP/Correctness.thy \ |
|
181 IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \ |
|
182 IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \ |
|
183 IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \ |
|
184 IOA/ABP/Spec.thy |
|
185 @cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP |
|
186 |
|
187 ## IOA-NTP |
|
188 |
|
189 IOA-NTP: IOA $(LOG)/IOA-NTP.gz |
|
190 |
|
191 $(LOG)/IOA-NTP.gz: $(OUT)/IOA \ |
|
192 IOA/NTP/Abschannel.thy IOA/NTP/Action.thy IOA/NTP/Correctness.thy \ |
|
193 IOA/NTP/Impl.thy IOA/NTP/Lemmas.thy IOA/NTP/Multiset.thy \ |
|
194 IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.thy IOA/NTP/Sender.thy \ |
|
195 IOA/NTP/Spec.thy |
|
196 @cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA NTP |
|
197 |
|
198 |
|
199 ## IOA-Storage |
|
200 |
|
201 IOA-Storage: IOA $(LOG)/IOA-Storage.gz |
|
202 |
|
203 $(LOG)/IOA-Storage.gz: $(OUT)/IOA IOA/Storage/Action.thy \ |
|
204 IOA/Storage/Correctness.thy IOA/Storage/Impl.thy \ |
|
205 IOA/Storage/ROOT.ML IOA/Storage/Spec.thy |
|
206 @cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Storage |
|
207 |
|
208 |
|
209 ## IOA-ex |
|
210 |
|
211 IOA-ex: IOA $(LOG)/IOA-ex.gz |
|
212 |
|
213 $(LOG)/IOA-ex.gz: $(OUT)/IOA IOA/ex/ROOT.ML IOA/ex/TrivEx.thy IOA/ex/TrivEx2.thy |
|
214 @cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex |
|
215 |
|
216 |
|
217 ## clean |
|
218 |
|
219 clean: |
|
220 @rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \ |
|
221 $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA \ |
|
222 $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \ |
|
223 $(LOG)/IOA-Storage.gz $(LOG)/HOLCF-Library.gz \ |
|
224 $(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz |
|