| author | wenzelm |
| Thu, 02 Oct 2008 19:59:00 +0200 | |
| changeset 28464 | dcc030b52583 |
| parent 27420 | aa335405f0c5 |
| child 28500 | 4b79e5d3d0aa |
| 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 |
|
| 27420 | 30 |
$(OUT)/HOLCF: $(OUT)/HOL \ |
31 |
ROOT.ML \ |
|
32 |
Adm.thy \ |
|
33 |
Algebraic.thy \ |
|
34 |
Bifinite.thy \ |
|
35 |
Cfun.thy \ |
|
36 |
CompactBasis.thy \ |
|
37 |
Completion.thy \ |
|
38 |
Cont.thy \ |
|
39 |
ConvexPD.thy \ |
|
40 |
Cprod.thy \ |
|
41 |
Discrete.thy \ |
|
42 |
Deflation.thy \ |
|
43 |
Domain.thy \ |
|
44 |
Eventual.thy \ |
|
45 |
Ffun.thy \ |
|
46 |
Fixrec.thy \ |
|
47 |
Fix.thy \ |
|
48 |
HOLCF.thy \ |
|
49 |
Lift.thy \ |
|
50 |
LowerPD.thy \ |
|
51 |
NatIso.thy \ |
|
52 |
One.thy \ |
|
53 |
Pcpodef.thy \ |
|
54 |
Pcpo.thy \ |
|
55 |
Porder.thy \ |
|
56 |
Sprod.thy \ |
|
57 |
Ssum.thy \ |
|
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 \ |
|
70 |
Tools/fixrec_package.ML \ |
|
71 |
Tools/pcpodef_package.ML \ |
|
72 |
holcf_logic.ML \ |
|
73 |
document/root.tex |
|
|
15586
f7f812034707
Added dependency document/root.tex, and -g true option to isatool; document generation should work now.
huffman
parents:
15576
diff
changeset
|
74 |
@$(ISATOOL) 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 |
| 4518 | 83 |
@$(ISATOOL) usedir $(OUT)/HOLCF IMP |
| 2494 | 84 |
|
85 |
||
| 4518 | 86 |
## HOLCF-ex |
87 |
||
88 |
HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz |
|
| 2494 | 89 |
|
| 25161 | 90 |
$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Stream.thy ex/Dagstuhl.thy \ |
| 19742 | 91 |
ex/Dnat.thy ex/Fix2.thy ex/Focus_ex.thy ex/Hoare.thy ex/Loop.thy \ |
92 |
ex/ROOT.ML ex/Fixrec_ex.thy ../HOL/Library/Nat_Infinity.thy |
|
| 4518 | 93 |
@$(ISATOOL) usedir $(OUT)/HOLCF ex |
| 3081 | 94 |
|
95 |
||
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
96 |
## HOLCF-FOCUS |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
97 |
|
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
98 |
HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
99 |
|
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
14535
diff
changeset
|
100 |
$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF FOCUS/Fstreams.thy \ |
| 19759 | 101 |
FOCUS/Fstream.thy FOCUS/FOCUS.thy \ |
102 |
FOCUS/Stream_adm.thy ../HOL/Library/Continuity.thy \ |
|
103 |
FOCUS/Buffer.thy FOCUS/Buffer_adm.thy |
|
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
104 |
@$(ISATOOL) usedir $(OUT)/HOLCF FOCUS |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
105 |
|
| 4518 | 106 |
## IOA |
107 |
||
108 |
IOA: HOLCF $(OUT)/IOA |
|
109 |
||
| 19741 | 110 |
$(OUT)/IOA: $(OUT)/HOLCF IOA/ROOT.ML IOA/meta_theory/Traces.thy \ |
111 |
IOA/meta_theory/Asig.thy IOA/meta_theory/CompoScheds.thy \ |
|
112 |
IOA/meta_theory/CompoTraces.thy IOA/meta_theory/Seq.thy \ |
|
113 |
IOA/meta_theory/RefCorrectness.thy IOA/meta_theory/Automata.thy \ |
|
114 |
IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/IOA.thy \ |
|
115 |
IOA/meta_theory/Sequence.thy IOA/meta_theory/CompoExecs.thy \ |
|
116 |
IOA/meta_theory/RefMappings.thy IOA/meta_theory/Compositionality.thy \ |
|
117 |
IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy \ |
|
118 |
IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy \ |
|
119 |
IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy \ |
|
120 |
IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa_package.ML |
|
| 4518 | 121 |
@cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA |
| 3081 | 122 |
|
123 |
||
| 4518 | 124 |
## IOA-ABP |
125 |
||
126 |
IOA-ABP: IOA $(LOG)/IOA-ABP.gz |
|
| 3081 | 127 |
|
| 4518 | 128 |
$(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
|
129 |
IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.thy \ |
| 19738 | 130 |
IOA/ABP/Check.ML IOA/ABP/Correctness.thy \ |
| 4518 | 131 |
IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \ |
| 19738 | 132 |
IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \ |
| 4518 | 133 |
IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \ |
134 |
IOA/ABP/Spec.thy |
|
| 3081 | 135 |
@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP |
136 |
||
| 4518 | 137 |
## IOA-NTP |
138 |
||
139 |
IOA-NTP: IOA $(LOG)/IOA-NTP.gz |
|
140 |
||
| 19739 | 141 |
$(LOG)/IOA-NTP.gz: $(OUT)/IOA \ |
142 |
IOA/NTP/Abschannel.thy IOA/NTP/Action.thy IOA/NTP/Correctness.thy \ |
|
143 |
IOA/NTP/Impl.thy IOA/NTP/Lemmas.thy IOA/NTP/Multiset.thy \ |
|
144 |
IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.thy IOA/NTP/Sender.thy \ |
|
| 4518 | 145 |
IOA/NTP/Spec.thy |
| 3081 | 146 |
@cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP |
147 |
||
| 3951 | 148 |
|
| 6475 | 149 |
## IOA-Modelcheck |
150 |
||
151 |
IOA-Modelcheck: IOA $(LOG)/IOA-Modelcheck.gz |
|
152 |
||
| 19764 | 153 |
$(LOG)/IOA-Modelcheck.gz: $(OUT)/IOA IOA/Modelcheck/ROOT.ML \ |
| 22819 | 154 |
IOA/Modelcheck/Cockpit.thy IOA/Modelcheck/MuIOA.thy \ |
155 |
IOA/Modelcheck/MuIOAOracle.thy IOA/Modelcheck/Ring3.thy |
|
| 6475 | 156 |
@cd IOA; $(ISATOOL) usedir $(OUT)/IOA Modelcheck |
157 |
||
158 |
||
| 6010 | 159 |
## IOA-Storage |
160 |
||
161 |
IOA-Storage: IOA $(LOG)/IOA-Storage.gz |
|
162 |
||
| 19740 | 163 |
$(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
|
164 |
IOA/Storage/Correctness.thy IOA/Storage/Impl.thy \ |
| 6011 | 165 |
IOA/Storage/ROOT.ML IOA/Storage/Spec.thy |
| 6010 | 166 |
@cd IOA; $(ISATOOL) usedir $(OUT)/IOA Storage |
167 |
||
168 |
||
| 6475 | 169 |
## IOA-ex |
170 |
||
171 |
IOA-ex: IOA $(LOG)/IOA-ex.gz |
|
172 |
||
| 19740 | 173 |
$(LOG)/IOA-ex.gz: $(OUT)/IOA IOA/ex/ROOT.ML IOA/ex/TrivEx.thy IOA/ex/TrivEx2.thy |
| 6475 | 174 |
@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ex |
175 |
||
176 |
||
| 4518 | 177 |
## clean |
| 4447 | 178 |
|
179 |
clean: |
|
| 4518 | 180 |
@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
|
181 |
$(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz \ |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
8602
diff
changeset
|
182 |
$(OUT)/IOA $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz \ |
| 6475 | 183 |
$(LOG)/IOA-NTP.gz $(LOG)/IOA-Modelcheck.gz $(LOG)/IOA-Storage.gz |