author | nipkow |
Sun, 22 Dec 2002 10:43:43 +0100 | |
changeset 13763 | f94b569cd610 |
parent 12599 | 8bc47cf91bf6 |
child 14535 | 7cb26928e70d |
permissions | -rw-r--r-- |
2494 | 1 |
# |
2 |
# $Id$ |
|
3 |
# |
|
4 |
# IsaMakefile for HOLCF |
|
5 |
# |
|
6 |
||
4518 | 7 |
## targets |
2494 | 8 |
|
4518 | 9 |
default: HOLCF |
10 |
images: HOLCF IOA |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
11 |
test: HOLCF-IMP HOLCF-ex HOLCF-FOCUS \ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
12 |
IOA-ABP IOA-NTP IOA-Modelcheck IOA-Storage IOA-ex |
4518 | 13 |
all: images test |
14 |
||
15 |
||
16 |
## global settings |
|
17 |
||
18 |
SRC = $(ISABELLE_HOME)/src |
|
3118 | 19 |
OUT = $(ISABELLE_OUTPUT) |
4447 | 20 |
LOG = $(OUT)/log |
2494 | 21 |
|
4518 | 22 |
|
23 |
## HOLCF |
|
24 |
||
25 |
HOLCF: HOL $(OUT)/HOLCF |
|
26 |
||
27 |
HOL: |
|
28 |
@cd $(SRC)/HOL; $(ISATOOL) make HOL |
|
2494 | 29 |
|
4518 | 30 |
$(OUT)/HOLCF: $(OUT)/HOL Cfun1.ML Cfun1.thy Cfun2.ML Cfun2.thy \ |
31 |
Cfun3.ML Cfun3.thy Cont.ML Cont.thy Cprod1.ML Cprod1.thy Cprod2.ML \ |
|
32 |
Cprod2.thy Cprod3.ML Cprod3.thy Discrete.ML Discrete.thy Discrete0.ML \ |
|
33 |
Discrete0.thy Discrete1.ML Discrete1.thy Fix.ML Fix.thy Fun1.ML \ |
|
34 |
Fun1.thy Fun2.ML Fun2.thy Fun3.ML Fun3.thy HOLCF.ML HOLCF.thy Lift.ML \ |
|
12027 | 35 |
Lift.thy One.ML One.thy Pcpo.ML Pcpo.thy Porder.ML Porder.thy Porder0.ML \ |
4518 | 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 |
|
6213 | 42 |
@$(ISATOOL) usedir -b -r $(OUT)/HOL HOLCF |
2494 | 43 |
|
4518 | 44 |
|
45 |
## HOLCF-IMP |
|
2494 | 46 |
|
4518 | 47 |
HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz |
48 |
||
12433 | 49 |
$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \ |
12599 | 50 |
IMP/Denotational.thy IMP/ROOT.ML IMP/document/root.tex |
4518 | 51 |
@$(ISATOOL) usedir $(OUT)/HOLCF IMP |
2494 | 52 |
|
53 |
||
4518 | 54 |
## HOLCF-ex |
55 |
||
56 |
HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz |
|
2494 | 57 |
|
4518 | 58 |
$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Dagstuhl.ML ex/Dagstuhl.thy \ |
12035 | 59 |
ex/Dnat.thy ex/Fix2.ML ex/Fix2.thy ex/Focus_ex.ML \ |
4518 | 60 |
ex/Focus_ex.thy ex/Hoare.ML ex/Hoare.thy ex/Loop.ML ex/Loop.thy \ |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
61 |
ex/ROOT.ML ex/Stream.ML ex/Stream.thy ex/loeckx.ML \ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
62 |
../HOL/Library/Nat_Infinity.thy |
4518 | 63 |
@$(ISATOOL) usedir $(OUT)/HOLCF ex |
3081 | 64 |
|
65 |
||
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
66 |
## HOLCF-FOCUS |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
67 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
68 |
HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
69 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
70 |
$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF FOCUS/Fstream.thy FOCUS/Fstream.ML \ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
71 |
FOCUS/FOCUS.thy FOCUS/FOCUS.ML \ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
72 |
FOCUS/Stream_adm.thy FOCUS/Stream_adm.ML ../HOL/Library/Continuity.thy \ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
73 |
FOCUS/Buffer.thy FOCUS/Buffer.ML FOCUS/Buffer_adm.thy FOCUS/Buffer_adm.ML |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
74 |
@$(ISATOOL) usedir $(OUT)/HOLCF FOCUS |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
75 |
|
4518 | 76 |
## IOA |
77 |
||
78 |
IOA: HOLCF $(OUT)/IOA |
|
79 |
||
80 |
$(OUT)/IOA: $(OUT)/HOLCF IOA/ROOT.ML IOA/meta_theory/Traces.thy \ |
|
3081 | 81 |
IOA/meta_theory/Asig.ML IOA/meta_theory/Asig.thy \ |
82 |
IOA/meta_theory/CompoScheds.thy IOA/meta_theory/CompoExecs.ML \ |
|
83 |
IOA/meta_theory/CompoTraces.thy IOA/meta_theory/CompoScheds.ML \ |
|
84 |
IOA/meta_theory/CompoTraces.ML IOA/meta_theory/Sequence.ML \ |
|
85 |
IOA/meta_theory/Seq.thy IOA/meta_theory/RefCorrectness.thy \ |
|
86 |
IOA/meta_theory/Automata.thy IOA/meta_theory/Traces.ML \ |
|
87 |
IOA/meta_theory/Seq.ML IOA/meta_theory/RefMappings.ML \ |
|
88 |
IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/ShortExecutions.ML \ |
|
89 |
IOA/meta_theory/IOA.thy IOA/meta_theory/IOA.ML \ |
|
90 |
IOA/meta_theory/Sequence.thy IOA/meta_theory/Automata.ML \ |
|
91 |
IOA/meta_theory/CompoExecs.thy IOA/meta_theory/RefMappings.thy \ |
|
92 |
IOA/meta_theory/RefCorrectness.ML IOA/meta_theory/Compositionality.ML \ |
|
4562 | 93 |
IOA/meta_theory/Compositionality.thy \ |
94 |
IOA/meta_theory/TL.thy IOA/meta_theory/TL.ML IOA/meta_theory/TLS.thy \ |
|
95 |
IOA/meta_theory/TLS.ML IOA/meta_theory/LiveIOA.thy IOA/meta_theory/LiveIOA.ML \ |
|
96 |
IOA/meta_theory/Pred.thy IOA/meta_theory/Abstraction.thy \ |
|
6475 | 97 |
IOA/meta_theory/Abstraction.ML \ |
4566 | 98 |
IOA/meta_theory/Simulations.thy IOA/meta_theory/Simulations.ML \ |
6475 | 99 |
IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/SimCorrectness.ML \ |
100 |
IOA/meta_theory/ioa_syn.ML IOA/meta_theory/ioa_package.ML |
|
4518 | 101 |
@cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA |
3081 | 102 |
|
103 |
||
4518 | 104 |
## IOA-ABP |
105 |
||
106 |
IOA-ABP: IOA $(LOG)/IOA-ABP.gz |
|
3081 | 107 |
|
4518 | 108 |
$(LOG)/IOA-ABP.gz: $(OUT)/IOA IOA/ABP/Abschannel.thy \ |
8602
f077613e8e7b
mods because of weak_case_cong -> removed Action.ML twice
nipkow
parents:
6475
diff
changeset
|
109 |
IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.thy \ |
4518 | 110 |
IOA/ABP/Check.ML IOA/ABP/Correctness.ML IOA/ABP/Correctness.thy \ |
111 |
IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \ |
|
112 |
IOA/ABP/Lemmas.ML IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \ |
|
113 |
IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \ |
|
114 |
IOA/ABP/Spec.thy |
|
3081 | 115 |
@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP |
116 |
||
4518 | 117 |
## IOA-NTP |
118 |
||
119 |
IOA-NTP: IOA $(LOG)/IOA-NTP.gz |
|
120 |
||
121 |
$(LOG)/IOA-NTP.gz: $(OUT)/IOA IOA/NTP/Abschannel.ML \ |
|
8602
f077613e8e7b
mods because of weak_case_cong -> removed Action.ML twice
nipkow
parents:
6475
diff
changeset
|
122 |
IOA/NTP/Abschannel.thy IOA/NTP/Action.thy \ |
4518 | 123 |
IOA/NTP/Correctness.ML IOA/NTP/Correctness.thy IOA/NTP/Impl.ML \ |
124 |
IOA/NTP/Impl.thy IOA/NTP/Lemmas.ML IOA/NTP/Lemmas.thy \ |
|
125 |
IOA/NTP/Multiset.ML IOA/NTP/Multiset.thy IOA/NTP/Packet.ML \ |
|
126 |
IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.ML \ |
|
127 |
IOA/NTP/Receiver.thy IOA/NTP/Sender.ML IOA/NTP/Sender.thy \ |
|
128 |
IOA/NTP/Spec.thy |
|
3081 | 129 |
@cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP |
130 |
||
3951 | 131 |
|
6475 | 132 |
## IOA-Modelcheck |
133 |
||
134 |
IOA-Modelcheck: IOA $(LOG)/IOA-Modelcheck.gz |
|
135 |
||
136 |
$(LOG)/IOA-Modelcheck.gz: $(OUT)/IOA IOA/Modelcheck/ROOT.ML IOA/Modelcheck/Cockpit.ML\ |
|
137 |
IOA/Modelcheck/Cockpit.thy IOA/Modelcheck/MuIOA.ML IOA/Modelcheck/MuIOA.thy \ |
|
138 |
IOA/Modelcheck/MuIOAOracle.ML IOA/Modelcheck/MuIOAOracle.thy \ |
|
139 |
IOA/Modelcheck/Ring3.ML IOA/Modelcheck/Ring3.thy |
|
140 |
@cd IOA; $(ISATOOL) usedir $(OUT)/IOA Modelcheck |
|
141 |
||
142 |
||
6010 | 143 |
## IOA-Storage |
144 |
||
145 |
IOA-Storage: IOA $(LOG)/IOA-Storage.gz |
|
146 |
||
6011 | 147 |
$(LOG)/IOA-Storage.gz: $(OUT)/IOA IOA/Storage/Action.ML \ |
148 |
IOA/Storage/Action.thy IOA/Storage/Correctness.ML \ |
|
149 |
IOA/Storage/Correctness.thy IOA/Storage/Impl.ML IOA/Storage/Impl.thy \ |
|
150 |
IOA/Storage/ROOT.ML IOA/Storage/Spec.thy |
|
6010 | 151 |
@cd IOA; $(ISATOOL) usedir $(OUT)/IOA Storage |
152 |
||
153 |
||
6475 | 154 |
## IOA-ex |
155 |
||
156 |
IOA-ex: IOA $(LOG)/IOA-ex.gz |
|
157 |
||
158 |
$(LOG)/IOA-ex.gz: $(OUT)/IOA IOA/ex/ROOT.ML \ |
|
159 |
IOA/ex/TrivEx.thy IOA/ex/TrivEx.ML \ |
|
160 |
IOA/ex/TrivEx2.thy IOA/ex/TrivEx2.ML |
|
161 |
@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ex |
|
162 |
||
163 |
||
4518 | 164 |
## clean |
4447 | 165 |
|
166 |
clean: |
|
4518 | 167 |
@rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \ |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
168 |
$(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz \ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
169 |
$(OUT)/IOA $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz \ |
6475 | 170 |
$(LOG)/IOA-NTP.gz $(LOG)/IOA-Modelcheck.gz $(LOG)/IOA-Storage.gz |