src/HOL/IsaMakefile
changeset 4447 b7ee449eb345
parent 4289 5c1bfefd39b7
child 4455 c0a6ad614fa0
     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 +$(LOG)/HOL-AxClasses-Group.gz: $(LOG)/HOL-AxClasses.gz \
   1.152 +  $(AXC_GROUP_FILES:%=AxClasses/Group/%)
   1.153 +	@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
   1.154  
   1.155 -AxClasses: $(OUT)/HOL $(AXCLASSES_FILES)
   1.156 -	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
   1.157 -	@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
   1.158 +$(LOG)/HOL-AxClasses-Lattice.gz: $(LOG)/HOL-AxClasses.gz \
   1.159 +  $(AXC_LATTICE_FILES:%=AxClasses/Lattice/%)
   1.160  	@$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice
   1.161 +
   1.162 +$(LOG)/HOL-AxClasses-Tutorial.gz: $(LOG)/HOL-AxClasses.gz \
   1.163 +  $(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%)
   1.164  	@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial
   1.165  
   1.166  
   1.167 @@ -229,7 +234,8 @@
   1.168  QUOT_FILES = Quot/ROOT.ML Quot/PER0.thy Quot/PER0.ML Quot/PER.thy Quot/PER.ML \
   1.169  	Quot/HQUOT.thy Quot/HQUOT.ML Quot/NPAIR.thy Quot/NPAIR.ML \
   1.170  	Quot/FRACT.thy Quot/FRACT.ML
   1.171 -Quot:	$(OUT)/HOL $(QUOT_FILES)
   1.172 +
   1.173 +$(LOG)/HOL-Quot.gz: $(OUT)/HOL $(QUOT_FILES)
   1.174  	@$(ISATOOL) usedir $(OUT)/HOL Quot
   1.175  
   1.176  
   1.177 @@ -240,16 +246,25 @@
   1.178  EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
   1.179  	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   1.180  
   1.181 -ex:	$(OUT)/HOL $(EX_FILES)
   1.182 +$(LOG)/HOL-ex.gz: $(OUT)/HOL $(EX_FILES)
   1.183  	@$(ISATOOL) usedir $(OUT)/HOL ex
   1.184  
   1.185  
   1.186  ## Full test
   1.187  
   1.188 -test:	$(OUT)/HOL \
   1.189 -	  Subst Induct IMP Hoare Lex Integ Auth Modelcheck Lambda  \
   1.190 -	  W0 MiniML TLA TLA_Inc TLA_Buffer TLA_Memory IOA AxClasses Quot ex
   1.191 -	echo 'Test examples ran successfully' > test
   1.192 +ALL_TARGETS = $(OUT)/HOL $(LOG)/HOL-Subst.gz $(LOG)/HOL-Induct.gz \
   1.193 +  $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz $(LOG)/HOL-Lex.gz \
   1.194 +  $(LOG)/HOL-Integ.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-Modelcheck.gz \
   1.195 +  $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
   1.196 +  $(OUT)/TLA $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
   1.197 +  $(LOG)/TLA-Memory.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
   1.198 +  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \
   1.199 +  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz $(LOG)/HOL-ex.gz
   1.200 +
   1.201 +test: $(ALL_TARGETS)
   1.202 +
   1.203 +clean:
   1.204 +	@rm -f $(ALL_TARGETS)
   1.205  
   1.206  
   1.207  .PRECIOUS: $(OUT)/Pure $(OUT)/HOL