1.1 --- a/src/HOL/IsaMakefile Fri Dec 19 10:18:03 1997 +0100
1.2 +++ b/src/HOL/IsaMakefile Fri Dec 19 10:18:58 1997 +0100
1.3 @@ -7,6 +7,7 @@
1.4 #### Base system
1.5
1.6 OUT = $(ISABELLE_OUTPUT)
1.7 +LOG = $(OUT)/log
1.8
1.9 NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \
1.10 mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
1.11 @@ -41,7 +42,7 @@
1.12 INDUCT_FILES = Induct/ROOT.ML \
1.13 $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML)
1.14
1.15 -Induct: $(OUT)/HOL $(INDUCT_FILES)
1.16 +$(LOG)/HOL-Induct.gz: $(OUT)/HOL $(INDUCT_FILES)
1.17 @$(ISATOOL) usedir $(OUT)/HOL Induct
1.18
1.19
1.20 @@ -50,7 +51,7 @@
1.21 IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
1.22 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
1.23
1.24 -IMP: $(OUT)/HOL $(IMP_FILES)
1.25 +$(LOG)/HOL-IMP.gz: $(OUT)/HOL $(IMP_FILES)
1.26 @$(ISATOOL) usedir $(OUT)/HOL IMP
1.27
1.28
1.29 @@ -60,7 +61,7 @@
1.30 Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
1.31 $(Hoare_NAMES:%=Hoare/%.ML)
1.32
1.33 -Hoare: $(OUT)/HOL $(Hoare_FILES)
1.34 +$(LOG)/HOL-Hoare.gz: $(OUT)/HOL $(Hoare_FILES)
1.35 @$(ISATOOL) usedir $(OUT)/HOL Hoare
1.36
1.37
1.38 @@ -71,7 +72,7 @@
1.39 INTEG_FILES = Integ/ROOT.ML \
1.40 $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
1.41
1.42 -Integ: $(OUT)/HOL $(INTEG_FILES)
1.43 +$(LOG)/HOL-Integ.gz: $(OUT)/HOL $(INTEG_FILES)
1.44 @$(ISATOOL) usedir $(OUT)/HOL Integ
1.45
1.46
1.47 @@ -97,16 +98,16 @@
1.48 TLA/Memory/RPCParameters.ML TLA/Memory/RPCParameters.thy
1.49
1.50
1.51 -TLA: $(OUT)/HOL $(TLA_FILES)
1.52 +$(OUT)/TLA: $(OUT)/HOL $(TLA_FILES)
1.53 @cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA
1.54
1.55 -TLA_Inc: $(OUT)/TLA $(TLA_INC_FILES)
1.56 +$(LOG)/TLA-Inc.gz: $(OUT)/TLA $(TLA_INC_FILES)
1.57 @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc
1.58
1.59 -TLA_Buffer: $(OUT)/TLA $(TLA_BUFFER_FILES)
1.60 +$(LOG)/TLA-Buffer.gz: $(OUT)/TLA $(TLA_BUFFER_FILES)
1.61 @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer
1.62
1.63 -TLA_Memory: $(OUT)/TLA $(TLA_MEMORY_FILES)
1.64 +$(LOG)/TLA-Memory.gz: $(OUT)/TLA $(TLA_MEMORY_FILES)
1.65 @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory
1.66
1.67
1.68 @@ -115,7 +116,7 @@
1.69 IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \
1.70 IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML
1.71
1.72 -IOA: $(OUT)/HOL $(IOA_FILES)
1.73 +$(LOG)/HOL-IOA.gz: $(OUT)/HOL $(IOA_FILES)
1.74 @$(ISATOOL) usedir $(OUT)/HOL IOA
1.75
1.76
1.77 @@ -128,7 +129,7 @@
1.78
1.79 AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
1.80
1.81 -Auth: $(OUT)/HOL $(AUTH_FILES)
1.82 +$(LOG)/HOL-Auth.gz: $(OUT)/HOL $(AUTH_FILES)
1.83 @$(ISATOOL) usedir $(OUT)/HOL Auth
1.84
1.85
1.86 @@ -138,7 +139,7 @@
1.87 Modelcheck/Example.thy Modelcheck/MCSyn.ML Modelcheck/MCSyn.thy \
1.88 Modelcheck/MuCalculus.ML Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML
1.89
1.90 -Modelcheck: $(OUT)/HOL $(MC_FILES)
1.91 +$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL $(MC_FILES)
1.92 @$(ISATOOL) usedir $(OUT)/HOL Modelcheck
1.93
1.94
1.95 @@ -149,7 +150,7 @@
1.96 SUBST_FILES = Subst/ROOT.ML \
1.97 $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
1.98
1.99 -Subst: $(OUT)/HOL $(SUBST_FILES)
1.100 +$(LOG)/HOL-Subst.gz: $(OUT)/HOL $(SUBST_FILES)
1.101 @$(ISATOOL) usedir $(OUT)/HOL Subst
1.102
1.103
1.104 @@ -160,7 +161,7 @@
1.105 LAMBDA_FILES = Lambda/ROOT.ML \
1.106 $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
1.107
1.108 -Lambda: $(OUT)/HOL $(LAMBDA_FILES)
1.109 +$(LOG)/HOL-Lambda.gz: $(OUT)/HOL $(LAMBDA_FILES)
1.110 @$(ISATOOL) usedir $(OUT)/HOL Lambda
1.111
1.112
1.113 @@ -171,7 +172,7 @@
1.114 W0_FILES = W0/ROOT.ML \
1.115 $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML)
1.116
1.117 -W0: $(OUT)/HOL $(W0_FILES)
1.118 +$(LOG)/HOL-W0.gz: $(OUT)/HOL $(W0_FILES)
1.119 @$(ISATOOL) usedir $(OUT)/HOL W0
1.120
1.121
1.122 @@ -182,7 +183,7 @@
1.123 MINIML_FILES = MiniML/ROOT.ML \
1.124 $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
1.125
1.126 -MiniML: $(OUT)/HOL $(MINIML_FILES)
1.127 +$(LOG)/HOL-MiniML.gz: $(OUT)/HOL $(MINIML_FILES)
1.128 @$(ISATOOL) usedir $(OUT)/HOL MiniML
1.129
1.130
1.131 @@ -193,7 +194,7 @@
1.132 LEX_FILES = Lex/ROOT.ML \
1.133 $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
1.134
1.135 -Lex: $(OUT)/HOL $(LEX_FILES)
1.136 +$(LOG)/HOL-Lex.gz: $(OUT)/HOL $(LEX_FILES)
1.137 @$(ISATOOL) usedir $(OUT)/HOL Lex
1.138
1.139
1.140 @@ -212,15 +213,19 @@
1.141 ProductInsts.thy ROOT.ML Semigroup.thy Semigroups.thy Sigs.thy \
1.142 Xor.ML Xor.thy
1.143
1.144 -AXCLASSES_FILES = AxClasses/ROOT.ML \
1.145 - $(AXC_GROUP_FILES:%=AxClasses/Group/%) \
1.146 - $(AXC_LATTICE_FILES:%=AxClasses/Lattice/%) \
1.147 - $(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%)
1.148 +$(LOG)/HOL-AxClasses.gz: AxClasses/ROOT.ML $(OUT)/HOL
1.149 + @$(ISATOOL) usedir $(OUT)/HOL AxClasses
1.150
1.151 -AxClasses: $(OUT)/HOL $(AXCLASSES_FILES)
1.152 - @$(ISATOOL) usedir $(OUT)/HOL AxClasses
1.153 +$(LOG)/HOL-AxClasses-Group.gz: $(LOG)/HOL-AxClasses.gz \
1.154 + $(AXC_GROUP_FILES:%=AxClasses/Group/%)
1.155 @$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
1.156 +
1.157 +$(LOG)/HOL-AxClasses-Lattice.gz: $(LOG)/HOL-AxClasses.gz \
1.158 + $(AXC_LATTICE_FILES:%=AxClasses/Lattice/%)
1.159 @$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice
1.160 +
1.161 +$(LOG)/HOL-AxClasses-Tutorial.gz: $(LOG)/HOL-AxClasses.gz \
1.162 + $(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%)
1.163 @$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial
1.164
1.165
1.166 @@ -229,7 +234,8 @@
1.167 QUOT_FILES = Quot/ROOT.ML Quot/PER0.thy Quot/PER0.ML Quot/PER.thy Quot/PER.ML \
1.168 Quot/HQUOT.thy Quot/HQUOT.ML Quot/NPAIR.thy Quot/NPAIR.ML \
1.169 Quot/FRACT.thy Quot/FRACT.ML
1.170 -Quot: $(OUT)/HOL $(QUOT_FILES)
1.171 +
1.172 +$(LOG)/HOL-Quot.gz: $(OUT)/HOL $(QUOT_FILES)
1.173 @$(ISATOOL) usedir $(OUT)/HOL Quot
1.174
1.175
1.176 @@ -240,16 +246,25 @@
1.177 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
1.178 ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
1.179
1.180 -ex: $(OUT)/HOL $(EX_FILES)
1.181 +$(LOG)/HOL-ex.gz: $(OUT)/HOL $(EX_FILES)
1.182 @$(ISATOOL) usedir $(OUT)/HOL ex
1.183
1.184
1.185 ## Full test
1.186
1.187 -test: $(OUT)/HOL \
1.188 - Subst Induct IMP Hoare Lex Integ Auth Modelcheck Lambda \
1.189 - W0 MiniML TLA TLA_Inc TLA_Buffer TLA_Memory IOA AxClasses Quot ex
1.190 - echo 'Test examples ran successfully' > test
1.191 +ALL_TARGETS = $(OUT)/HOL $(LOG)/HOL-Subst.gz $(LOG)/HOL-Induct.gz \
1.192 + $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz $(LOG)/HOL-Lex.gz \
1.193 + $(LOG)/HOL-Integ.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-Modelcheck.gz \
1.194 + $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
1.195 + $(OUT)/TLA $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
1.196 + $(LOG)/TLA-Memory.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
1.197 + $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \
1.198 + $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz $(LOG)/HOL-ex.gz
1.199 +
1.200 +test: $(ALL_TARGETS)
1.201 +
1.202 +clean:
1.203 + @rm -f $(ALL_TARGETS)
1.204
1.205
1.206 .PRECIOUS: $(OUT)/Pure $(OUT)/HOL