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