author | haftmann |
Tue, 23 Jun 2009 12:08:35 +0200 | |
changeset 31773 | 4d33c5d7575b |
parent 31738 | 7b9b9ba532ca |
child 32126 | a5042f260440 |
permissions | -rw-r--r-- |
2494 | 1 |
# |
2 |
# IsaMakefile for HOLCF |
|
3 |
# |
|
4 |
||
4518 | 5 |
## targets |
2494 | 6 |
|
4518 | 7 |
default: HOLCF |
8 |
images: HOLCF IOA |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
9 |
test: HOLCF-IMP HOLCF-ex HOLCF-FOCUS \ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
10 |
IOA-ABP IOA-NTP IOA-Modelcheck IOA-Storage IOA-ex |
4518 | 11 |
all: images test |
12 |
||
13 |
||
14 |
## global settings |
|
15 |
||
16 |
SRC = $(ISABELLE_HOME)/src |
|
3118 | 17 |
OUT = $(ISABELLE_OUTPUT) |
4447 | 18 |
LOG = $(OUT)/log |
2494 | 19 |
|
4518 | 20 |
|
21 |
## HOLCF |
|
22 |
||
23 |
HOLCF: HOL $(OUT)/HOLCF |
|
24 |
||
25 |
HOL: |
|
28500 | 26 |
@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL |
2494 | 27 |
|
27420 | 28 |
$(OUT)/HOLCF: $(OUT)/HOL \ |
29 |
ROOT.ML \ |
|
30 |
Adm.thy \ |
|
31 |
Algebraic.thy \ |
|
32 |
Bifinite.thy \ |
|
33 |
Cfun.thy \ |
|
34 |
CompactBasis.thy \ |
|
35 |
Completion.thy \ |
|
36 |
Cont.thy \ |
|
37 |
ConvexPD.thy \ |
|
38 |
Cprod.thy \ |
|
39 |
Discrete.thy \ |
|
40 |
Deflation.thy \ |
|
41 |
Domain.thy \ |
|
42 |
Eventual.thy \ |
|
43 |
Ffun.thy \ |
|
44 |
Fixrec.thy \ |
|
45 |
Fix.thy \ |
|
46 |
HOLCF.thy \ |
|
47 |
Lift.thy \ |
|
48 |
LowerPD.thy \ |
|
49 |
NatIso.thy \ |
|
50 |
One.thy \ |
|
51 |
Pcpodef.thy \ |
|
52 |
Pcpo.thy \ |
|
53 |
Porder.thy \ |
|
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29130
diff
changeset
|
54 |
Product_Cpo.thy \ |
27420 | 55 |
Sprod.thy \ |
56 |
Ssum.thy \ |
|
29534 | 57 |
Sum_Cpo.thy \ |
27420 | 58 |
Tr.thy \ |
59 |
Universal.thy \ |
|
60 |
UpperPD.thy \ |
|
61 |
Up.thy \ |
|
62 |
Tools/adm_tac.ML \ |
|
63 |
Tools/cont_consts.ML \ |
|
64 |
Tools/cont_proc.ML \ |
|
65 |
Tools/domain/domain_extender.ML \ |
|
66 |
Tools/domain/domain_axioms.ML \ |
|
67 |
Tools/domain/domain_library.ML \ |
|
68 |
Tools/domain/domain_syntax.ML \ |
|
69 |
Tools/domain/domain_theorems.ML \ |
|
31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
30920
diff
changeset
|
70 |
Tools/fixrec.ML \ |
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
30920
diff
changeset
|
71 |
Tools/pcpodef.ML \ |
27420 | 72 |
holcf_logic.ML \ |
73 |
document/root.tex |
|
28500 | 74 |
@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF |
2494 | 75 |
|
4518 | 76 |
|
77 |
## HOLCF-IMP |
|
2494 | 78 |
|
4518 | 79 |
HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz |
80 |
||
12433 | 81 |
$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \ |
12599 | 82 |
IMP/Denotational.thy IMP/ROOT.ML IMP/document/root.tex |
28500 | 83 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP |
2494 | 84 |
|
85 |
||
4518 | 86 |
## HOLCF-ex |
87 |
||
88 |
HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz |
|
2494 | 89 |
|
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset
|
90 |
$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \ |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset
|
91 |
../HOL/Library/Nat_Infinity.thy \ |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset
|
92 |
ex/Dagstuhl.thy \ |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset
|
93 |
ex/Dnat.thy \ |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset
|
94 |
ex/Domain_ex.thy \ |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset
|
95 |
ex/Fix2.thy \ |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset
|
96 |
ex/Fixrec_ex.thy \ |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset
|
97 |
ex/Focus_ex.thy \ |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset
|
98 |
ex/Hoare.thy \ |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset
|
99 |
ex/Loop.thy \ |
29992 | 100 |
ex/Powerdomain_ex.thy \ |
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset
|
101 |
ex/Stream.thy \ |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset
|
102 |
ex/ROOT.ML |
28500 | 103 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex |
3081 | 104 |
|
105 |
||
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
106 |
## HOLCF-FOCUS |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
107 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
108 |
HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
109 |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
14535
diff
changeset
|
110 |
$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF FOCUS/Fstreams.thy \ |
19759 | 111 |
FOCUS/Fstream.thy FOCUS/FOCUS.thy \ |
112 |
FOCUS/Stream_adm.thy ../HOL/Library/Continuity.thy \ |
|
113 |
FOCUS/Buffer.thy FOCUS/Buffer_adm.thy |
|
28500 | 114 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
115 |
|
4518 | 116 |
## IOA |
117 |
||
118 |
IOA: HOLCF $(OUT)/IOA |
|
119 |
||
19741 | 120 |
$(OUT)/IOA: $(OUT)/HOLCF IOA/ROOT.ML IOA/meta_theory/Traces.thy \ |
121 |
IOA/meta_theory/Asig.thy IOA/meta_theory/CompoScheds.thy \ |
|
122 |
IOA/meta_theory/CompoTraces.thy IOA/meta_theory/Seq.thy \ |
|
123 |
IOA/meta_theory/RefCorrectness.thy IOA/meta_theory/Automata.thy \ |
|
124 |
IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/IOA.thy \ |
|
125 |
IOA/meta_theory/Sequence.thy IOA/meta_theory/CompoExecs.thy \ |
|
126 |
IOA/meta_theory/RefMappings.thy IOA/meta_theory/Compositionality.thy \ |
|
127 |
IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy \ |
|
128 |
IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy \ |
|
129 |
IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy \ |
|
31773 | 130 |
IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/automaton.ML |
28500 | 131 |
@cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA |
3081 | 132 |
|
133 |
||
4518 | 134 |
## IOA-ABP |
135 |
||
136 |
IOA-ABP: IOA $(LOG)/IOA-ABP.gz |
|
3081 | 137 |
|
4518 | 138 |
$(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
|
139 |
IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.thy \ |
19738 | 140 |
IOA/ABP/Check.ML IOA/ABP/Correctness.thy \ |
4518 | 141 |
IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \ |
19738 | 142 |
IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \ |
4518 | 143 |
IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \ |
144 |
IOA/ABP/Spec.thy |
|
28500 | 145 |
@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP |
3081 | 146 |
|
4518 | 147 |
## IOA-NTP |
148 |
||
149 |
IOA-NTP: IOA $(LOG)/IOA-NTP.gz |
|
150 |
||
19739 | 151 |
$(LOG)/IOA-NTP.gz: $(OUT)/IOA \ |
152 |
IOA/NTP/Abschannel.thy IOA/NTP/Action.thy IOA/NTP/Correctness.thy \ |
|
153 |
IOA/NTP/Impl.thy IOA/NTP/Lemmas.thy IOA/NTP/Multiset.thy \ |
|
154 |
IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.thy IOA/NTP/Sender.thy \ |
|
4518 | 155 |
IOA/NTP/Spec.thy |
28500 | 156 |
@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA NTP |
3081 | 157 |
|
3951 | 158 |
|
6475 | 159 |
## IOA-Modelcheck |
160 |
||
161 |
IOA-Modelcheck: IOA $(LOG)/IOA-Modelcheck.gz |
|
162 |
||
19764 | 163 |
$(LOG)/IOA-Modelcheck.gz: $(OUT)/IOA IOA/Modelcheck/ROOT.ML \ |
22819 | 164 |
IOA/Modelcheck/Cockpit.thy IOA/Modelcheck/MuIOA.thy \ |
165 |
IOA/Modelcheck/MuIOAOracle.thy IOA/Modelcheck/Ring3.thy |
|
28500 | 166 |
@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Modelcheck |
6475 | 167 |
|
168 |
||
6010 | 169 |
## IOA-Storage |
170 |
||
171 |
IOA-Storage: IOA $(LOG)/IOA-Storage.gz |
|
172 |
||
19740 | 173 |
$(LOG)/IOA-Storage.gz: $(OUT)/IOA IOA/Storage/Action.thy \ |
17238
b1cf9189104e
removed IOA/Storage/Impl.ML, IOA/Storage/Action.ML;
wenzelm
parents:
16698
diff
changeset
|
174 |
IOA/Storage/Correctness.thy IOA/Storage/Impl.thy \ |
6011 | 175 |
IOA/Storage/ROOT.ML IOA/Storage/Spec.thy |
28500 | 176 |
@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Storage |
6010 | 177 |
|
178 |
||
6475 | 179 |
## IOA-ex |
180 |
||
181 |
IOA-ex: IOA $(LOG)/IOA-ex.gz |
|
182 |
||
19740 | 183 |
$(LOG)/IOA-ex.gz: $(OUT)/IOA IOA/ex/ROOT.ML IOA/ex/TrivEx.thy IOA/ex/TrivEx2.thy |
28500 | 184 |
@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex |
6475 | 185 |
|
186 |
||
4518 | 187 |
## clean |
4447 | 188 |
|
189 |
clean: |
|
4518 | 190 |
@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
|
191 |
$(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz \ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
192 |
$(OUT)/IOA $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz \ |
6475 | 193 |
$(LOG)/IOA-NTP.gz $(LOG)/IOA-Modelcheck.gz $(LOG)/IOA-Storage.gz |