2 # $Id$ |
2 # $Id$ |
3 # |
3 # |
4 # IsaMakefile for HOL |
4 # IsaMakefile for HOL |
5 # |
5 # |
6 |
6 |
7 #### Base system |
7 ## targets |
8 |
8 |
|
9 default: HOL |
|
10 images: HOL TLA |
|
11 test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Integ \ |
|
12 HOL-Auth HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-IOA \ |
|
13 HOL-AxClasses HOL-AxClasses-Group HOL-AxClasses-Lattice \ |
|
14 HOL-AxClasses-Tutorial HOL-Quot HOL-ex TLA-Inc TLA-Buffer TLA-Memory |
|
15 all: images test |
|
16 |
|
17 |
|
18 ## global settings |
|
19 |
|
20 SRC = $(ISABELLE_HOME)/src |
9 OUT = $(ISABELLE_OUTPUT) |
21 OUT = $(ISABELLE_OUTPUT) |
10 LOG = $(OUT)/log |
22 LOG = $(OUT)/log |
11 |
23 |
12 NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \ |
24 |
13 mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \ |
25 ## HOL |
14 Divides Power Sexp Univ List RelPow Option Map |
26 |
15 |
27 HOL: Pure $(OUT)/HOL |
16 PROVERS = hypsubst.ML classical.ML blast.ML \ |
28 |
17 simplifier.ML splitter.ML Arith/nat_transitive.ML Arith/cancel_sums.ML |
29 Pure: |
18 |
30 @cd $(SRC)/Pure; $(ISATOOL) make Pure |
19 TFL = dcterm.sml post.sml rules.new.sml rules.sig \ |
31 |
20 sys.sml tfl.sig tfl.sml thms.sig thms.sml thry.sig thry.sml \ |
32 $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/cancel_sums.ML \ |
21 usyntax.sig usyntax.sml utils.sig utils.sml |
33 $(SRC)/Provers/Arith/nat_transitive.ML $(SRC)/Provers/blast.ML \ |
22 |
34 $(SRC)/Provers/classical.ML $(SRC)/Provers/hypsubst.ML \ |
23 FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \ |
35 $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \ |
24 ind_syntax.ML cladata.ML record.ML simpdata.ML arith_data.ML \ |
36 $(SRC)/Pure/section_utils.ML $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml \ |
25 typedef.ML thy_syntax.ML thy_data.ML $(ISABELLE_HOME)/src/Pure/section_utils.ML \ |
37 $(SRC)/TFL/rules.new.sml $(SRC)/TFL/rules.sig $(SRC)/TFL/sys.sml \ |
26 $(NAMES:%=%.thy) $(NAMES:%=%.ML) $(TFL:%=../TFL/%) \ |
38 $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig \ |
27 $(PROVERS:%=$(ISABELLE_HOME)/src/Provers/%) |
39 $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml \ |
28 |
40 $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig \ |
29 $(OUT)/HOL: $(OUT)/Pure $(FILES) |
41 $(SRC)/TFL/utils.sml Arith.ML Arith.thy Divides.ML Divides.thy \ |
|
42 Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \ |
|
43 Inductive.ML Inductive.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML \ |
|
44 Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy \ |
|
45 Ord.ML Ord.thy Power.ML Power.thy Prod.ML Prod.thy ROOT.ML RelPow.ML \ |
|
46 RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \ |
|
47 Sum.ML Sum.thy Trancl.ML Trancl.thy Univ.ML Univ.thy WF.ML WF.thy \ |
|
48 WF_Rel.ML WF_Rel.thy add_ind_def.ML arith_data.ML cladata.ML \ |
|
49 datatype.ML equalities.ML equalities.thy hologic.ML ind_syntax.ML \ |
|
50 indrule.ML indrule.thy intr_elim.ML intr_elim.thy mono.ML mono.thy \ |
|
51 record.ML simpdata.ML subset.ML subset.thy thy_data.ML thy_syntax.ML \ |
|
52 typedef.ML |
30 @$(ISATOOL) usedir -b $(OUT)/Pure HOL |
53 @$(ISATOOL) usedir -b $(OUT)/Pure HOL |
31 |
54 |
32 $(OUT)/Pure: |
55 |
33 @cd ../Pure; $(ISATOOL) make |
56 ## HOL-Subst |
34 |
57 |
35 |
58 HOL-Subst: HOL $(LOG)/HOL-Subst.gz |
36 #### Tests and examples |
59 |
37 |
60 $(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.ML Subst/AList.thy \ |
38 ## Inductive definitions: simple examples |
61 Subst/ROOT.ML Subst/Subst.ML Subst/Subst.thy Subst/UTerm.ML \ |
39 |
62 Subst/UTerm.thy Subst/Unifier.ML Subst/Unifier.thy Subst/Unify.ML \ |
40 INDUCT_FILES = Perm Comb Mutil SList LList LFilter Acc PropLog Term Simult Com Exp |
63 Subst/Unify.thy |
41 |
64 @$(ISATOOL) usedir $(OUT)/HOL Subst |
42 INDUCT_FILES = Induct/ROOT.ML \ |
65 |
43 $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML) |
66 |
44 |
67 ## HOL-Induct |
45 $(LOG)/HOL-Induct.gz: $(OUT)/HOL $(INDUCT_FILES) |
68 |
|
69 HOL-Induct: HOL $(LOG)/HOL-Induct.gz |
|
70 |
|
71 $(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Acc.ML Induct/Acc.thy \ |
|
72 Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \ |
|
73 Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \ |
|
74 Induct/LList.ML Induct/LList.thy Induct/Mutil.ML Induct/Mutil.thy \ |
|
75 Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML Induct/PropLog.thy \ |
|
76 Induct/ROOT.ML Induct/SList.ML Induct/SList.thy Induct/Simult.ML \ |
|
77 Induct/Simult.thy Induct/Term.ML Induct/Term.thy |
46 @$(ISATOOL) usedir $(OUT)/HOL Induct |
78 @$(ISATOOL) usedir $(OUT)/HOL Induct |
47 |
79 |
48 |
80 |
49 ## IMP-semantics example |
81 ## HOL-IMP |
50 |
82 |
51 IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC |
83 HOL-IMP: HOL $(LOG)/HOL-IMP.gz |
52 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML) |
84 |
53 |
85 $(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.ML IMP/Com.thy IMP/Denotation.ML \ |
54 $(LOG)/HOL-IMP.gz: $(OUT)/HOL $(IMP_FILES) |
86 IMP/Denotation.thy IMP/Expr.ML IMP/Expr.thy IMP/Hoare.ML IMP/Hoare.thy \ |
|
87 IMP/Natural.ML IMP/Natural.thy IMP/ROOT.ML IMP/Transition.ML \ |
|
88 IMP/Transition.thy IMP/VC.ML IMP/VC.thy |
55 @$(ISATOOL) usedir $(OUT)/HOL IMP |
89 @$(ISATOOL) usedir $(OUT)/HOL IMP |
56 |
90 |
57 |
91 |
58 ## Hoare logic |
92 ## HOL-Hoare |
59 |
93 |
60 Hoare_NAMES = Hoare Arith2 Examples |
94 HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz |
61 Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \ |
95 |
62 $(Hoare_NAMES:%=Hoare/%.ML) |
96 $(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.ML Hoare/Arith2.thy \ |
63 |
97 Hoare/Examples.ML Hoare/Examples.thy Hoare/Hoare.ML Hoare/Hoare.thy \ |
64 $(LOG)/HOL-Hoare.gz: $(OUT)/HOL $(Hoare_FILES) |
98 Hoare/ROOT.ML |
65 @$(ISATOOL) usedir $(OUT)/HOL Hoare |
99 @$(ISATOOL) usedir $(OUT)/HOL Hoare |
66 |
100 |
67 |
101 |
68 ## The integers in HOL |
102 ## HOL-Lex |
69 |
103 |
70 INTEG_NAMES = Equiv Integ Group Ring Lagrange IntRingDefs IntRing |
104 HOL-Lex: HOL $(LOG)/HOL-Lex.gz |
71 |
105 |
72 INTEG_FILES = Integ/ROOT.ML \ |
106 $(LOG)/HOL-Lex.gz: $(OUT)/HOL Lex/Auto.thy Lex/Auto.ML \ |
73 $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML) |
107 Lex/AutoChopper.thy Lex/AutoChopper.ML Lex/AutoChopper1.thy \ |
74 |
108 Lex/Chopper.thy Lex/Prefix.thy Lex/Prefix.ML Lex/ROOT.ML \ |
75 $(LOG)/HOL-Integ.gz: $(OUT)/HOL $(INTEG_FILES) |
109 Lex/Regset_of_auto.ML Lex/Regset_of_auto.thy |
|
110 @$(ISATOOL) usedir $(OUT)/HOL Lex |
|
111 |
|
112 |
|
113 ## HOL-Integ |
|
114 |
|
115 HOL-Integ: HOL $(LOG)/HOL-Integ.gz |
|
116 |
|
117 $(LOG)/HOL-Integ.gz: $(OUT)/HOL Integ/Bin.ML Integ/Bin.thy \ |
|
118 Integ/Equiv.ML Integ/Equiv.thy Integ/Group.ML Integ/Group.thy \ |
|
119 Integ/IntRing.ML Integ/IntRing.thy Integ/IntRingDefs.ML \ |
|
120 Integ/IntRingDefs.thy Integ/Integ.ML Integ/Integ.thy Integ/Lagrange.ML \ |
|
121 Integ/Lagrange.thy Integ/ROOT.ML Integ/Ring.ML Integ/Ring.thy |
76 @$(ISATOOL) usedir $(OUT)/HOL Integ |
122 @$(ISATOOL) usedir $(OUT)/HOL Integ |
77 |
123 |
78 |
124 |
79 ## TLA -- Temporal Logic of Actions |
125 ## HOL-Auth |
80 |
126 |
81 TLA_FILES = TLA/Action.ML TLA/Action.thy TLA/IntLemmas.ML \ |
127 HOL-Auth: HOL $(LOG)/HOL-Auth.gz |
82 TLA/Intensional.ML TLA/Intensional.thy TLA/ROOT.ML TLA/Stfun.ML \ |
128 |
83 TLA/Stfun.thy TLA/TLA.ML TLA/TLA.thy TLA/cladata.ML TLA/hypsubst.ML |
129 $(LOG)/HOL-Auth.gz: $(OUT)/HOL Auth/Event.ML Auth/Event.thy \ |
84 |
130 Auth/Message.ML Auth/Message.thy Auth/NS_Public.ML Auth/NS_Public.thy \ |
85 TLA_INC_FILES = TLA/Inc/Inc.thy TLA/Inc/Inc.ML TLA/Inc/Pcount.thy |
131 Auth/NS_Public_Bad.ML Auth/NS_Public_Bad.thy Auth/NS_Shared.ML \ |
86 |
132 Auth/NS_Shared.thy Auth/OtwayRees.ML Auth/OtwayRees.thy \ |
87 TLA_BUFFER_FILES = TLA/Buffer/Buffer.thy TLA/Buffer/Buffer.ML \ |
133 Auth/OtwayRees_AN.ML Auth/OtwayRees_AN.thy Auth/OtwayRees_Bad.ML \ |
88 TLA/Buffer/DBuffer.thy TLA/Buffer/DBuffer.ML |
134 Auth/OtwayRees_Bad.thy Auth/Public.ML Auth/Public.thy Auth/ROOT.ML \ |
89 |
135 Auth/Recur.ML Auth/Recur.thy Auth/Shared.ML Auth/Shared.thy \ |
90 TLA_MEMORY_FILES = TLA/Memory/MIParameters.thy TLA/Memory/MIlive.ML \ |
136 Auth/TLS.ML Auth/TLS.thy Auth/WooLam.ML Auth/WooLam.thy \ |
91 TLA/Memory/MIsafe.ML TLA/Memory/MemClerk.ML TLA/Memory/MemClerk.thy \ |
137 Auth/Yahalom.ML Auth/Yahalom.thy Auth/Yahalom2.ML Auth/Yahalom2.thy |
92 TLA/Memory/MemClerkParameters.ML TLA/Memory/MemClerkParameters.thy \ |
138 @$(ISATOOL) usedir $(OUT)/HOL Auth |
93 TLA/Memory/Memory.ML TLA/Memory/Memory.thy \ |
139 |
94 TLA/Memory/MemoryImplementation.ML TLA/Memory/MemoryImplementation.thy \ |
140 |
95 TLA/Memory/MemoryParameters.ML TLA/Memory/MemoryParameters.thy \ |
141 ## HOL-Modelcheck |
96 TLA/Memory/ProcedureInterface.ML TLA/Memory/ProcedureInterface.thy \ |
142 |
97 TLA/Memory/RPC.ML TLA/Memory/RPC.thy TLA/Memory/RPCMemoryParams.thy \ |
143 HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz |
98 TLA/Memory/RPCParameters.ML TLA/Memory/RPCParameters.thy |
144 |
99 |
145 $(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \ |
100 |
146 Modelcheck/Example.ML Modelcheck/Example.thy Modelcheck/MCSyn.ML \ |
101 $(OUT)/TLA: $(OUT)/HOL $(TLA_FILES) |
147 Modelcheck/MCSyn.thy Modelcheck/MuCalculus.ML \ |
|
148 Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML |
|
149 @$(ISATOOL) usedir $(OUT)/HOL Modelcheck |
|
150 |
|
151 |
|
152 ## HOL-Lambda |
|
153 |
|
154 HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz |
|
155 |
|
156 $(LOG)/HOL-Lambda.gz: $(OUT)/HOL Lambda/Commutation.ML \ |
|
157 Lambda/Commutation.thy Lambda/Eta.ML Lambda/Eta.thy Lambda/Lambda.ML \ |
|
158 Lambda/Lambda.thy Lambda/ParRed.ML Lambda/ParRed.thy Lambda/ROOT.ML |
|
159 @$(ISATOOL) usedir $(OUT)/HOL Lambda |
|
160 |
|
161 |
|
162 ## HOL-W0 |
|
163 |
|
164 HOL-W0: HOL $(LOG)/HOL-W0.gz |
|
165 |
|
166 $(LOG)/HOL-W0.gz: $(OUT)/HOL W0/I.ML W0/I.thy W0/Maybe.ML W0/Maybe.thy \ |
|
167 W0/MiniML.ML W0/MiniML.thy W0/ROOT.ML W0/Type.ML W0/Type.thy W0/W.ML \ |
|
168 W0/W.thy |
|
169 @$(ISATOOL) usedir $(OUT)/HOL W0 |
|
170 |
|
171 |
|
172 ## HOL-MiniML |
|
173 |
|
174 HOL-MiniML: HOL $(LOG)/HOL-MiniML.gz |
|
175 |
|
176 $(LOG)/HOL-MiniML.gz: $(OUT)/HOL MiniML/Generalize.ML \ |
|
177 MiniML/Generalize.thy MiniML/Instance.ML MiniML/Instance.thy \ |
|
178 MiniML/Maybe.ML MiniML/Maybe.thy MiniML/MiniML.ML MiniML/MiniML.thy \ |
|
179 MiniML/ROOT.ML MiniML/Type.ML MiniML/Type.thy MiniML/W.ML MiniML/W.thy |
|
180 @$(ISATOOL) usedir $(OUT)/HOL MiniML |
|
181 |
|
182 |
|
183 ## HOL-IOA |
|
184 |
|
185 HOL-IOA: HOL $(LOG)/HOL-IOA.gz |
|
186 |
|
187 $(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.ML IOA/Asig.thy IOA/IOA.ML \ |
|
188 IOA/IOA.thy IOA/ROOT.ML IOA/Solve.ML IOA/Solve.thy |
|
189 @$(ISATOOL) usedir $(OUT)/HOL IOA |
|
190 |
|
191 |
|
192 ## HOL-AxClasses |
|
193 |
|
194 HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz |
|
195 |
|
196 $(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/ROOT.ML |
|
197 @$(ISATOOL) usedir $(OUT)/HOL AxClasses |
|
198 |
|
199 |
|
200 ## HOL-AxClasses-Group |
|
201 |
|
202 HOL-AxClasses-Group: HOL-AxClasses $(LOG)/HOL-AxClasses-Group.gz |
|
203 |
|
204 $(LOG)/HOL-AxClasses-Group.gz: $(OUT)/HOL AxClasses/Group/Group.ML \ |
|
205 AxClasses/Group/Group.thy AxClasses/Group/GroupDefs.ML \ |
|
206 AxClasses/Group/GroupDefs.thy AxClasses/Group/GroupInsts.thy \ |
|
207 AxClasses/Group/Monoid.thy AxClasses/Group/MonoidGroupInsts.thy \ |
|
208 AxClasses/Group/ROOT.ML AxClasses/Group/Sigs.thy |
|
209 @$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group |
|
210 |
|
211 |
|
212 ## HOL-AxClasses-Lattice |
|
213 |
|
214 HOL-AxClasses-Lattice: HOL-AxClasses $(LOG)/HOL-AxClasses-Lattice.gz |
|
215 |
|
216 $(LOG)/HOL-AxClasses-Lattice.gz: $(OUT)/HOL AxClasses/Lattice/CLattice.ML \ |
|
217 AxClasses/Lattice/CLattice.thy AxClasses/Lattice/LatInsts.ML \ |
|
218 AxClasses/Lattice/LatInsts.thy AxClasses/Lattice/LatMorph.ML \ |
|
219 AxClasses/Lattice/LatMorph.thy AxClasses/Lattice/LatPreInsts.ML \ |
|
220 AxClasses/Lattice/LatPreInsts.thy AxClasses/Lattice/Lattice.ML \ |
|
221 AxClasses/Lattice/Lattice.thy AxClasses/Lattice/OrdDefs.ML \ |
|
222 AxClasses/Lattice/OrdDefs.thy AxClasses/Lattice/OrdInsts.thy \ |
|
223 AxClasses/Lattice/Order.ML AxClasses/Lattice/Order.thy \ |
|
224 AxClasses/Lattice/ROOT.ML AxClasses/Lattice/tools.ML |
|
225 @$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice |
|
226 |
|
227 |
|
228 ## HOL-AxClasses-Tutorial |
|
229 |
|
230 HOL-AxClasses-Tutorial: HOL-AxClasses $(LOG)/HOL-AxClasses-Tutorial.gz |
|
231 |
|
232 $(LOG)/HOL-AxClasses-Tutorial.gz: $(OUT)/HOL \ |
|
233 AxClasses/Tutorial/BoolGroupInsts.thy AxClasses/Tutorial/Group.ML \ |
|
234 AxClasses/Tutorial/Group.thy AxClasses/Tutorial/Monoid.thy \ |
|
235 AxClasses/Tutorial/MonoidGroupInsts.thy \ |
|
236 AxClasses/Tutorial/ProdGroupInsts.thy AxClasses/Tutorial/Product.thy \ |
|
237 AxClasses/Tutorial/ProductInsts.thy AxClasses/Tutorial/ROOT.ML \ |
|
238 AxClasses/Tutorial/Semigroup.thy AxClasses/Tutorial/Semigroups.thy \ |
|
239 AxClasses/Tutorial/Sigs.thy AxClasses/Tutorial/Xor.ML \ |
|
240 AxClasses/Tutorial/Xor.thy |
|
241 @$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial |
|
242 |
|
243 |
|
244 ## HOL-Quot |
|
245 |
|
246 HOL-Quot: HOL $(LOG)/HOL-Quot.gz |
|
247 |
|
248 $(LOG)/HOL-Quot.gz: $(OUT)/HOL Quot/FRACT.ML Quot/FRACT.thy \ |
|
249 Quot/HQUOT.ML Quot/HQUOT.thy Quot/NPAIR.ML Quot/NPAIR.thy Quot/PER.ML \ |
|
250 Quot/PER.thy Quot/PER0.ML Quot/PER0.thy Quot/ROOT.ML |
|
251 @$(ISATOOL) usedir $(OUT)/HOL Quot |
|
252 |
|
253 |
|
254 ## HOL-ex |
|
255 |
|
256 HOL-ex: HOL $(LOG)/HOL-ex.gz |
|
257 |
|
258 $(LOG)/HOL-ex.gz: $(OUT)/HOL ex/BT.ML ex/BT.thy ex/Fib.ML ex/Fib.thy \ |
|
259 ex/InSort.ML ex/InSort.thy ex/MT.ML ex/MT.thy ex/NatSum.ML \ |
|
260 ex/NatSum.thy ex/Primes.ML ex/Primes.thy ex/Primrec.ML ex/Primrec.thy \ |
|
261 ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy ex/ROOT.ML \ |
|
262 ex/Recdef.ML ex/Recdef.thy ex/String.ML ex/String.thy ex/cla.ML \ |
|
263 ex/meson.ML ex/mesontest.ML ex/rel.ML ex/set.ML |
|
264 @$(ISATOOL) usedir $(OUT)/HOL ex |
|
265 |
|
266 |
|
267 ## TLA |
|
268 |
|
269 TLA: HOL $(OUT)/TLA |
|
270 |
|
271 $(OUT)/TLA: $(OUT)/HOL TLA/Action.ML TLA/Action.thy TLA/IntLemmas.ML \ |
|
272 TLA/Intensional.ML TLA/Intensional.thy TLA/ROOT.ML TLA/Stfun.ML \ |
|
273 TLA/Stfun.thy TLA/TLA.ML TLA/TLA.thy TLA/cladata.ML TLA/hypsubst.ML |
102 @cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA |
274 @cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA |
103 |
275 |
104 $(LOG)/TLA-Inc.gz: $(OUT)/TLA $(TLA_INC_FILES) |
276 |
|
277 ## TLA-Inc |
|
278 |
|
279 TLA-Inc: TLA $(LOG)/TLA-Inc.gz |
|
280 |
|
281 $(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy TLA/Inc/Inc.ML \ |
|
282 TLA/Inc/Pcount.thy |
105 @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc |
283 @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc |
106 |
284 |
107 $(LOG)/TLA-Buffer.gz: $(OUT)/TLA $(TLA_BUFFER_FILES) |
285 |
|
286 ## TLA-Buffer |
|
287 |
|
288 TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz |
|
289 |
|
290 $(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy \ |
|
291 TLA/Buffer/Buffer.ML TLA/Buffer/DBuffer.thy TLA/Buffer/DBuffer.ML |
108 @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer |
292 @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer |
109 |
293 |
110 $(LOG)/TLA-Memory.gz: $(OUT)/TLA $(TLA_MEMORY_FILES) |
294 |
|
295 ## TLA-Memory |
|
296 |
|
297 TLA-Memory: TLA $(LOG)/TLA-Memory.gz |
|
298 |
|
299 $(LOG)/TLA-Memory.gz: $(OUT)/TLA TLA/Memory/MIParameters.thy \ |
|
300 TLA/Memory/MIlive.ML TLA/Memory/MIsafe.ML TLA/Memory/MemClerk.ML \ |
|
301 TLA/Memory/MemClerk.thy TLA/Memory/MemClerkParameters.ML \ |
|
302 TLA/Memory/MemClerkParameters.thy TLA/Memory/Memory.ML \ |
|
303 TLA/Memory/Memory.thy TLA/Memory/MemoryImplementation.ML \ |
|
304 TLA/Memory/MemoryImplementation.thy TLA/Memory/MemoryParameters.ML \ |
|
305 TLA/Memory/MemoryParameters.thy TLA/Memory/ProcedureInterface.ML \ |
|
306 TLA/Memory/ProcedureInterface.thy TLA/Memory/RPC.ML TLA/Memory/RPC.thy \ |
|
307 TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.ML \ |
|
308 TLA/Memory/RPCParameters.thy |
111 @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory |
309 @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory |
112 |
310 |
113 |
311 |
114 ## I/O Automata (meta theory only) |
312 ## clean |
115 |
|
116 IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \ |
|
117 IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML |
|
118 |
|
119 $(LOG)/HOL-IOA.gz: $(OUT)/HOL $(IOA_FILES) |
|
120 @$(ISATOOL) usedir $(OUT)/HOL IOA |
|
121 |
|
122 |
|
123 ## Authentication & Security Protocols |
|
124 |
|
125 AUTH_NAMES = Message Event Shared NS_Shared \ |
|
126 OtwayRees OtwayRees_AN OtwayRees_Bad \ |
|
127 Recur WooLam Yahalom Yahalom2 \ |
|
128 Public NS_Public_Bad NS_Public TLS |
|
129 |
|
130 AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML) |
|
131 |
|
132 $(LOG)/HOL-Auth.gz: $(OUT)/HOL $(AUTH_FILES) |
|
133 @$(ISATOOL) usedir $(OUT)/HOL Auth |
|
134 |
|
135 |
|
136 ## Modelchecker invocation |
|
137 |
|
138 MC_FILES = Modelcheck/CTL.thy Modelcheck/Example.ML \ |
|
139 Modelcheck/Example.thy Modelcheck/MCSyn.ML Modelcheck/MCSyn.thy \ |
|
140 Modelcheck/MuCalculus.ML Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML |
|
141 |
|
142 $(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL $(MC_FILES) |
|
143 @$(ISATOOL) usedir $(OUT)/HOL Modelcheck |
|
144 |
|
145 |
|
146 ## Properties of substitutions |
|
147 |
|
148 SUBST_NAMES = AList Subst Unifier UTerm Unify |
|
149 |
|
150 SUBST_FILES = Subst/ROOT.ML \ |
|
151 $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML) |
|
152 |
|
153 $(LOG)/HOL-Subst.gz: $(OUT)/HOL $(SUBST_FILES) |
|
154 @$(ISATOOL) usedir $(OUT)/HOL Subst |
|
155 |
|
156 |
|
157 ## Confluence of Lambda-calculus |
|
158 |
|
159 LAMBDA_NAMES = Lambda ParRed Commutation Eta |
|
160 |
|
161 LAMBDA_FILES = Lambda/ROOT.ML \ |
|
162 $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML) |
|
163 |
|
164 $(LOG)/HOL-Lambda.gz: $(OUT)/HOL $(LAMBDA_FILES) |
|
165 @$(ISATOOL) usedir $(OUT)/HOL Lambda |
|
166 |
|
167 |
|
168 ## Type inference without let |
|
169 |
|
170 W0_NAMES = I Maybe MiniML Type W |
|
171 |
|
172 W0_FILES = W0/ROOT.ML \ |
|
173 $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML) |
|
174 |
|
175 $(LOG)/HOL-W0.gz: $(OUT)/HOL $(W0_FILES) |
|
176 @$(ISATOOL) usedir $(OUT)/HOL W0 |
|
177 |
|
178 |
|
179 ## Type inference with let |
|
180 |
|
181 MINIML_NAMES = Generalize Instance Maybe MiniML Type W |
|
182 |
|
183 MINIML_FILES = MiniML/ROOT.ML \ |
|
184 $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML) |
|
185 |
|
186 $(LOG)/HOL-MiniML.gz: $(OUT)/HOL $(MINIML_FILES) |
|
187 @$(ISATOOL) usedir $(OUT)/HOL MiniML |
|
188 |
|
189 |
|
190 ## Lexical analysis |
|
191 |
|
192 LEX_FILES = Auto AutoChopper Chopper Prefix |
|
193 |
|
194 LEX_FILES = Lex/ROOT.ML \ |
|
195 $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML) |
|
196 |
|
197 $(LOG)/HOL-Lex.gz: $(OUT)/HOL $(LEX_FILES) |
|
198 @$(ISATOOL) usedir $(OUT)/HOL Lex |
|
199 |
|
200 |
|
201 ## Axiomatic type classes examples |
|
202 |
|
203 AXC_GROUP_FILES = Group.ML Group.thy GroupDefs.ML GroupDefs.thy \ |
|
204 GroupInsts.thy Monoid.thy MonoidGroupInsts.thy ROOT.ML Sigs.thy |
|
205 |
|
206 AXC_LATTICE_FILES = CLattice.ML CLattice.thy LatInsts.ML LatInsts.thy \ |
|
207 LatMorph.ML LatMorph.thy LatPreInsts.ML LatPreInsts.thy \ |
|
208 Lattice.ML Lattice.thy OrdDefs.ML OrdDefs.thy OrdInsts.thy \ |
|
209 Order.ML Order.thy ROOT.ML tools.ML |
|
210 |
|
211 AXC_TUTORIAL_FILES = BoolGroupInsts.thy Group.ML Group.thy Monoid.thy \ |
|
212 MonoidGroupInsts.thy ProdGroupInsts.thy Product.thy \ |
|
213 ProductInsts.thy ROOT.ML Semigroup.thy Semigroups.thy Sigs.thy \ |
|
214 Xor.ML Xor.thy |
|
215 |
|
216 $(LOG)/HOL-AxClasses.gz: AxClasses/ROOT.ML $(OUT)/HOL |
|
217 @$(ISATOOL) usedir $(OUT)/HOL AxClasses |
|
218 |
|
219 $(LOG)/HOL-AxClasses-Group.gz: $(LOG)/HOL-AxClasses.gz \ |
|
220 $(AXC_GROUP_FILES:%=AxClasses/Group/%) |
|
221 @$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group |
|
222 |
|
223 $(LOG)/HOL-AxClasses-Lattice.gz: $(LOG)/HOL-AxClasses.gz \ |
|
224 $(AXC_LATTICE_FILES:%=AxClasses/Lattice/%) |
|
225 @$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice |
|
226 |
|
227 $(LOG)/HOL-AxClasses-Tutorial.gz: $(LOG)/HOL-AxClasses.gz \ |
|
228 $(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%) |
|
229 @$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial |
|
230 |
|
231 |
|
232 ## Higher-order quotients and example fractionals |
|
233 |
|
234 QUOT_FILES = Quot/ROOT.ML Quot/PER0.thy Quot/PER0.ML Quot/PER.thy Quot/PER.ML \ |
|
235 Quot/HQUOT.thy Quot/HQUOT.ML Quot/NPAIR.thy Quot/NPAIR.ML \ |
|
236 Quot/FRACT.thy Quot/FRACT.ML |
|
237 |
|
238 $(LOG)/HOL-Quot.gz: $(OUT)/HOL $(QUOT_FILES) |
|
239 @$(ISATOOL) usedir $(OUT)/HOL Quot |
|
240 |
|
241 |
|
242 ## Miscellaneous examples |
|
243 |
|
244 EX_NAMES = Recdef Fib Primes Primrec NatSum String BT InSort Qsort Puzzle MT |
|
245 |
|
246 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \ |
|
247 ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
|
248 |
|
249 $(LOG)/HOL-ex.gz: $(OUT)/HOL $(EX_FILES) |
|
250 @$(ISATOOL) usedir $(OUT)/HOL ex |
|
251 |
|
252 |
|
253 ## Full test |
|
254 |
|
255 ALL_TARGETS = $(OUT)/HOL $(LOG)/HOL-Subst.gz $(LOG)/HOL-Induct.gz \ |
|
256 $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz $(LOG)/HOL-Lex.gz \ |
|
257 $(LOG)/HOL-Integ.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-Modelcheck.gz \ |
|
258 $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \ |
|
259 $(OUT)/TLA $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \ |
|
260 $(LOG)/TLA-Memory.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \ |
|
261 $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \ |
|
262 $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz $(LOG)/HOL-ex.gz |
|
263 |
|
264 test: $(ALL_TARGETS) |
|
265 |
313 |
266 clean: |
314 clean: |
267 @rm -f $(ALL_TARGETS) |
315 @rm -f $(OUT)/HOL $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \ |
268 |
316 $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \ |
269 |
317 $(LOG)/HOL-Lex.gz $(LOG)/HOL-Integ.gz $(LOG)/HOL-Auth.gz \ |
270 .PRECIOUS: $(OUT)/Pure $(OUT)/HOL |
318 $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz \ |
|
319 $(LOG)/HOL-MiniML.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \ |
|
320 $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \ |
|
321 $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \ |
|
322 $(LOG)/HOL-ex.gz $(OUT)/TLA $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz \ |
|
323 $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz |