src/HOL/IsaMakefile
author wenzelm
Tue Jan 07 09:01:18 1997 +0100 (1997-01-07)
changeset 2473 3eb12c85846c
parent 2448 61337170db84
child 2527 0ba3755ce398
permissions -rw-r--r--
minor tuning;
added Auth/Recur;
     1 #
     2 # $Id$
     3 #
     4 # IsaMakefile for HOL
     5 #
     6 
     7 #### Base system
     8 
     9 OUT = $(ISABELLE_OUTPUT_DIR)
    10 
    11 NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF \
    12 	mono Lfp Gfp Nat intr_elim indrule Inductive Finite Arith \
    13 	Sexp Univ List RelPow Option
    14 
    15 FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
    16 	ind_syntax.ML cladata.ML simpdata.ML \
    17 	typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML \
    18 	../Provers/hypsubst.ML ../Provers/classical.ML \
    19 	../Provers/simplifier.ML ../Provers/splitter.ML \
    20 	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
    21 
    22 $(OUT)/HOL: $(OUT)/Pure $(FILES)
    23 	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu $(OUT)/Pure HOL
    24 	@chmod -w $@
    25 
    26 $(OUT)/Pure:
    27 	@cd ../Pure; $(ISATOOL) make
    28 
    29 
    30 ## TFL (requires integration into HOL proper)
    31 
    32 TFL_NAMES = mask tfl thms thry usyntax utils
    33 TFL_FILES = ../TFL/ROOT.ML ../TFL/sys.sml \
    34             $(TFL_NAMES:%=../TFL/%.sig) $(TFL_NAMES:%=../TFL/%.sml)
    35 
    36 TFL:	$(OUT)/HOL $(TFL_FILES)
    37 	@$(ISABELLE) -e 'exit_use_dir"../TFL"; quit();' HOL
    38 
    39 
    40 
    41 #### Tests and examples
    42 
    43 ## IMP-semantics example
    44 
    45 IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
    46 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    47 
    48 IMP:	$(OUT)/HOL $(IMP_FILES)
    49 	@$(ISATOOL) testdir $(OUT)/HOL IMP
    50 
    51 
    52 ## Hoare logic
    53 
    54 Hoare_NAMES = Hoare Arith2 Examples
    55 Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
    56 	      $(Hoare_NAMES:%=Hoare/%.ML)
    57 
    58 Hoare:	$(OUT)/HOL $(Hoare_FILES)
    59 	@$(ISATOOL) testdir $(OUT)/HOL Hoare
    60 
    61 
    62 ## The integers in HOL
    63 
    64 INTEG_NAMES = Equiv Integ Group Ring Lagrange IntRingDefs IntRing
    65 
    66 INTEG_FILES = Integ/ROOT.ML \
    67 	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
    68 
    69 Integ:	$(OUT)/HOL $(INTEG_FILES)
    70 	@$(ISATOOL) testdir $(OUT)/HOL Integ
    71 
    72 
    73 ## I/O Automata
    74 
    75 IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet \
    76 		Receiver Sender
    77 IOA_ABP_NAMES = Action Correctness Lemmas
    78 IOA_MT_NAMES = Asig IOA Solve
    79 
    80 IOA_FILES = IOA/NTP/ROOT.ML IOA/ABP/ROOT.ML IOA/NTP/Spec.thy \
    81  $(IOA_NTP_NAMES:%=IOA/NTP/%.thy) $(IOA_NTP_NAMES:%=IOA/NTP/%.ML) \
    82  IOA/ABP/Abschannel.thy IOA/ABP/Abschannel_finite.thy IOA/ABP/Env.thy \
    83  IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy IOA/ABP/Packet.thy \
    84  IOA/ABP/Receiver.thy IOA/ABP/Sender.thy IOA/ABP/Spec.thy \
    85  $(IOA_ABP_NAMES:%=IOA/ABP/%.thy) $(IOA_ABP_NAMES:%=IOA/ABP/%.ML) \
    86  $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
    87 
    88 IOA:	$(OUT)/HOL $(IOA_FILES)
    89 	@$(ISATOOL) testdir $(OUT)/HOL IOA/NTP
    90 	@$(ISATOOL) testdir $(OUT)/HOL IOA/ABP
    91 
    92 
    93 ## Authentication & Security Protocols
    94 
    95 Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \
    96 	     Recur WooLam Yahalom Yahalom2 Public NS_Public_Bad NS_Public
    97 
    98 AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
    99 
   100 Auth:	$(OUT)/HOL $(AUTH_FILES)
   101 	@$(ISATOOL) testdir $(OUT)/HOL Auth
   102 
   103 
   104 ## Properties of substitutions
   105 
   106 SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
   107 
   108 SUBST_FILES = Subst/ROOT.ML \
   109 	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
   110 
   111 Subst:	$(OUT)/HOL $(SUBST_FILES)
   112 	@$(ISATOOL) testdir $(OUT)/HOL Subst
   113 
   114 
   115 ## Confluence of Lambda-calculus
   116 
   117 LAMBDA_NAMES = Lambda ParRed Commutation Eta
   118 
   119 LAMBDA_FILES = Lambda/ROOT.ML \
   120 	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
   121 
   122 Lambda:	 $(OUT)/HOL $(LAMBDA_FILES)
   123 	@$(ISATOOL) testdir $(OUT)/HOL Lambda
   124 
   125 
   126 ## Type inference for MiniML
   127 
   128 MINIML_NAMES = I Maybe MiniML Type W
   129 
   130 MINIML_FILES = MiniML/ROOT.ML \
   131 	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
   132 
   133 MiniML: $(OUT)/HOL $(MINIML_FILES)
   134 	@$(ISATOOL) testdir $(OUT)/HOL MiniML
   135 
   136 
   137 ## Lexical analysis
   138 
   139 LEX_FILES = Auto AutoChopper Chopper Prefix
   140 
   141 LEX_FILES = Lex/ROOT.ML \
   142 	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
   143 
   144 Lex:	$(OUT)/HOL $(LEX_FILES)
   145 	@$(ISATOOL) testdir $(OUT)/HOL Lex
   146 
   147 
   148 ## Miscellaneous examples
   149 
   150 EX_NAMES = String BT Perm Comb InSort Qsort LexProd \
   151 	   Puzzle Mutil Primes NatSum SList LList Acc PropLog Term Simult MT
   152 
   153 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
   154 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   155 
   156 ex:	$(OUT)/HOL $(EX_FILES)
   157 	@$(ISATOOL) testdir $(OUT)/HOL ex
   158 
   159 
   160 ## Full test
   161 
   162 test:	$(OUT)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda MiniML IOA ex
   163 	echo 'Test examples ran successfully' > test
   164 
   165 
   166 .PRECIOUS: $(OUT)/Pure $(OUT)/HOL