src/HOL/IsaMakefile
author wenzelm
Fri Dec 19 10:18:58 1997 +0100 (1997-12-19)
changeset 4447 b7ee449eb345
parent 4289 5c1bfefd39b7
child 4455 c0a6ad614fa0
permissions -rw-r--r--
log files;
'clean' target;
     1 #
     2 # $Id$
     3 #
     4 # IsaMakefile for HOL
     5 #
     6 
     7 #### Base system
     8 
     9 OUT = $(ISABELLE_OUTPUT)
    10 LOG = $(OUT)/log
    11 
    12 NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \
    13 	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
    14 	Divides Power Sexp Univ List RelPow Option Map
    15 
    16 PROVERS = hypsubst.ML classical.ML blast.ML \
    17 	simplifier.ML splitter.ML Arith/nat_transitive.ML Arith/cancel_sums.ML
    18 
    19 TFL   = dcterm.sml post.sml rules.new.sml rules.sig \
    20 	sys.sml tfl.sig tfl.sml thms.sig thms.sml thry.sig thry.sml   \
    21 	usyntax.sig usyntax.sml utils.sig utils.sml
    22 
    23 FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
    24 	ind_syntax.ML cladata.ML simpdata.ML arith_data.ML \
    25 	typedef.ML thy_syntax.ML thy_data.ML $(ISABELLE_HOME)/src/Pure/section_utils.ML \
    26 	$(NAMES:%=%.thy) $(NAMES:%=%.ML) $(TFL:%=../TFL/%) \
    27 	$(PROVERS:%=$(ISABELLE_HOME)/src/Provers/%)
    28 
    29 $(OUT)/HOL: $(OUT)/Pure $(FILES)
    30 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    31 
    32 $(OUT)/Pure:
    33 	@cd ../Pure; $(ISATOOL) make
    34 
    35 
    36 #### Tests and examples
    37 
    38 ## Inductive definitions: simple examples
    39 
    40 INDUCT_FILES = Perm Comb Mutil SList LList LFilter Acc PropLog Term Simult Com Exp
    41 
    42 INDUCT_FILES = Induct/ROOT.ML \
    43 	    $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML)
    44 
    45 $(LOG)/HOL-Induct.gz: $(OUT)/HOL $(INDUCT_FILES)
    46 	@$(ISATOOL) usedir $(OUT)/HOL Induct
    47 
    48 
    49 ## IMP-semantics example
    50 
    51 IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
    52 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    53 
    54 $(LOG)/HOL-IMP.gz: $(OUT)/HOL $(IMP_FILES)
    55 	@$(ISATOOL) usedir $(OUT)/HOL IMP
    56 
    57 
    58 ## Hoare logic
    59 
    60 Hoare_NAMES = Hoare Arith2 Examples
    61 Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
    62 	      $(Hoare_NAMES:%=Hoare/%.ML)
    63 
    64 $(LOG)/HOL-Hoare.gz: $(OUT)/HOL $(Hoare_FILES)
    65 	@$(ISATOOL) usedir $(OUT)/HOL Hoare
    66 
    67 
    68 ## The integers in HOL
    69 
    70 INTEG_NAMES = Equiv Integ Group Ring Lagrange IntRingDefs IntRing
    71 
    72 INTEG_FILES = Integ/ROOT.ML \
    73 	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
    74 
    75 $(LOG)/HOL-Integ.gz: $(OUT)/HOL $(INTEG_FILES)
    76 	@$(ISATOOL) usedir $(OUT)/HOL Integ
    77 
    78 
    79 ## TLA -- Temporal Logic of Actions
    80 
    81 TLA_FILES = TLA/Action.ML TLA/Action.thy TLA/IntLemmas.ML \
    82 	TLA/Intensional.ML TLA/Intensional.thy TLA/ROOT.ML TLA/Stfun.ML \
    83 	TLA/Stfun.thy TLA/TLA.ML TLA/TLA.thy TLA/cladata.ML TLA/hypsubst.ML
    84 
    85 TLA_INC_FILES = TLA/Inc/Inc.thy TLA/Inc/Inc.ML TLA/Inc/Pcount.thy
    86 
    87 TLA_BUFFER_FILES = TLA/Buffer/Buffer.thy TLA/Buffer/Buffer.ML \
    88 	TLA/Buffer/DBuffer.thy TLA/Buffer/DBuffer.ML
    89 
    90 TLA_MEMORY_FILES = TLA/Memory/MIParameters.thy TLA/Memory/MIlive.ML \
    91 	TLA/Memory/MIsafe.ML TLA/Memory/MemClerk.ML TLA/Memory/MemClerk.thy \
    92 	TLA/Memory/MemClerkParameters.ML TLA/Memory/MemClerkParameters.thy \
    93 	TLA/Memory/Memory.ML TLA/Memory/Memory.thy \
    94 	TLA/Memory/MemoryImplementation.ML TLA/Memory/MemoryImplementation.thy \
    95 	TLA/Memory/MemoryParameters.ML TLA/Memory/MemoryParameters.thy \
    96 	TLA/Memory/ProcedureInterface.ML TLA/Memory/ProcedureInterface.thy \
    97 	TLA/Memory/RPC.ML TLA/Memory/RPC.thy TLA/Memory/RPCMemoryParams.thy \
    98 	TLA/Memory/RPCParameters.ML TLA/Memory/RPCParameters.thy
    99 
   100 
   101 $(OUT)/TLA: $(OUT)/HOL $(TLA_FILES)
   102 	@cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA
   103 
   104 $(LOG)/TLA-Inc.gz: $(OUT)/TLA $(TLA_INC_FILES)
   105 	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc
   106 
   107 $(LOG)/TLA-Buffer.gz: $(OUT)/TLA $(TLA_BUFFER_FILES)
   108 	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer
   109 
   110 $(LOG)/TLA-Memory.gz: $(OUT)/TLA $(TLA_MEMORY_FILES)
   111 	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory
   112 
   113 
   114 ## I/O Automata (meta theory only)
   115 
   116 IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \
   117   IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML
   118 
   119 $(LOG)/HOL-IOA.gz: $(OUT)/HOL $(IOA_FILES)
   120 	@$(ISATOOL) usedir $(OUT)/HOL IOA
   121 
   122 
   123 ## Authentication & Security Protocols
   124 
   125 AUTH_NAMES = Message Event Shared NS_Shared \
   126 	     OtwayRees OtwayRees_AN OtwayRees_Bad \
   127 	     Recur WooLam Yahalom Yahalom2 \
   128 	     Public NS_Public_Bad NS_Public TLS
   129 
   130 AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
   131 
   132 $(LOG)/HOL-Auth.gz: $(OUT)/HOL $(AUTH_FILES)
   133 	@$(ISATOOL) usedir $(OUT)/HOL Auth
   134 
   135 
   136 ## Modelchecker invocation
   137 
   138 MC_FILES = Modelcheck/CTL.thy Modelcheck/Example.ML \
   139   Modelcheck/Example.thy Modelcheck/MCSyn.ML Modelcheck/MCSyn.thy \
   140   Modelcheck/MuCalculus.ML Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML
   141 
   142 $(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL $(MC_FILES)
   143 	@$(ISATOOL) usedir $(OUT)/HOL Modelcheck
   144 
   145 
   146 ## Properties of substitutions
   147 
   148 SUBST_NAMES = AList Subst Unifier UTerm Unify
   149 
   150 SUBST_FILES = Subst/ROOT.ML \
   151 	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
   152 
   153 $(LOG)/HOL-Subst.gz: $(OUT)/HOL $(SUBST_FILES)
   154 	@$(ISATOOL) usedir $(OUT)/HOL Subst
   155 
   156 
   157 ## Confluence of Lambda-calculus
   158 
   159 LAMBDA_NAMES = Lambda ParRed Commutation Eta
   160 
   161 LAMBDA_FILES = Lambda/ROOT.ML \
   162 	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
   163 
   164 $(LOG)/HOL-Lambda.gz: $(OUT)/HOL $(LAMBDA_FILES)
   165 	@$(ISATOOL) usedir $(OUT)/HOL Lambda
   166 
   167 
   168 ## Type inference without let
   169 
   170 W0_NAMES = I Maybe MiniML Type W
   171 
   172 W0_FILES = W0/ROOT.ML \
   173 	      $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML)
   174 
   175 $(LOG)/HOL-W0.gz: $(OUT)/HOL $(W0_FILES)
   176 	@$(ISATOOL) usedir $(OUT)/HOL W0
   177 
   178 
   179 ## Type inference with let
   180 
   181 MINIML_NAMES = Generalize Instance Maybe MiniML Type W
   182 
   183 MINIML_FILES = MiniML/ROOT.ML \
   184 	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
   185 
   186 $(LOG)/HOL-MiniML.gz: $(OUT)/HOL $(MINIML_FILES)
   187 	@$(ISATOOL) usedir $(OUT)/HOL MiniML
   188 
   189 
   190 ## Lexical analysis
   191 
   192 LEX_FILES = Auto AutoChopper Chopper Prefix
   193 
   194 LEX_FILES = Lex/ROOT.ML \
   195 	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
   196 
   197 $(LOG)/HOL-Lex.gz: $(OUT)/HOL $(LEX_FILES)
   198 	@$(ISATOOL) usedir $(OUT)/HOL Lex
   199 
   200 
   201 ## Axiomatic type classes examples
   202 
   203 AXC_GROUP_FILES = Group.ML Group.thy GroupDefs.ML GroupDefs.thy \
   204 	GroupInsts.thy Monoid.thy MonoidGroupInsts.thy ROOT.ML Sigs.thy
   205 
   206 AXC_LATTICE_FILES = CLattice.ML CLattice.thy LatInsts.ML LatInsts.thy \
   207 	LatMorph.ML LatMorph.thy LatPreInsts.ML LatPreInsts.thy \
   208 	Lattice.ML Lattice.thy OrdDefs.ML OrdDefs.thy OrdInsts.thy \
   209 	Order.ML Order.thy ROOT.ML tools.ML
   210 
   211 AXC_TUTORIAL_FILES = BoolGroupInsts.thy Group.ML Group.thy Monoid.thy \
   212 	MonoidGroupInsts.thy ProdGroupInsts.thy Product.thy \
   213 	ProductInsts.thy ROOT.ML Semigroup.thy Semigroups.thy Sigs.thy \
   214 	Xor.ML Xor.thy
   215 
   216 $(LOG)/HOL-AxClasses.gz: AxClasses/ROOT.ML $(OUT)/HOL
   217 	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
   218 
   219 $(LOG)/HOL-AxClasses-Group.gz: $(LOG)/HOL-AxClasses.gz \
   220   $(AXC_GROUP_FILES:%=AxClasses/Group/%)
   221 	@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
   222 
   223 $(LOG)/HOL-AxClasses-Lattice.gz: $(LOG)/HOL-AxClasses.gz \
   224   $(AXC_LATTICE_FILES:%=AxClasses/Lattice/%)
   225 	@$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice
   226 
   227 $(LOG)/HOL-AxClasses-Tutorial.gz: $(LOG)/HOL-AxClasses.gz \
   228   $(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%)
   229 	@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial
   230 
   231 
   232 ## Higher-order quotients and example fractionals
   233 
   234 QUOT_FILES = Quot/ROOT.ML Quot/PER0.thy Quot/PER0.ML Quot/PER.thy Quot/PER.ML \
   235 	Quot/HQUOT.thy Quot/HQUOT.ML Quot/NPAIR.thy Quot/NPAIR.ML \
   236 	Quot/FRACT.thy Quot/FRACT.ML
   237 
   238 $(LOG)/HOL-Quot.gz: $(OUT)/HOL $(QUOT_FILES)
   239 	@$(ISATOOL) usedir $(OUT)/HOL Quot
   240 
   241 
   242 ## Miscellaneous examples
   243 
   244 EX_NAMES = Recdef Fib Primes Primrec NatSum String BT InSort Qsort Puzzle MT
   245 
   246 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
   247 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   248 
   249 $(LOG)/HOL-ex.gz: $(OUT)/HOL $(EX_FILES)
   250 	@$(ISATOOL) usedir $(OUT)/HOL ex
   251 
   252 
   253 ## Full test
   254 
   255 ALL_TARGETS = $(OUT)/HOL $(LOG)/HOL-Subst.gz $(LOG)/HOL-Induct.gz \
   256   $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz $(LOG)/HOL-Lex.gz \
   257   $(LOG)/HOL-Integ.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-Modelcheck.gz \
   258   $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
   259   $(OUT)/TLA $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
   260   $(LOG)/TLA-Memory.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
   261   $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \
   262   $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz $(LOG)/HOL-ex.gz
   263 
   264 test: $(ALL_TARGETS)
   265 
   266 clean:
   267 	@rm -f $(ALL_TARGETS)
   268 
   269 
   270 .PRECIOUS: $(OUT)/Pure $(OUT)/HOL