IsaMakefile for HOL;
authorwenzelm
Wed Dec 18 15:56:58 1996 +0100 (1996-12-18)
changeset 244861337170db84
parent 2447 e86a6111cd8b
child 2449 d30ad12b1397
IsaMakefile for HOL;
src/HOL/IsaMakefile
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IsaMakefile	Wed Dec 18 15:56:58 1996 +0100
     1.3 @@ -0,0 +1,169 @@
     1.4 +#
     1.5 +# $Id$
     1.6 +#
     1.7 +# IsaMakefile for HOL
     1.8 +#
     1.9 +
    1.10 +#### Base system
    1.11 +
    1.12 +OUT = $(ISABELLE_OUTPUT_DIR)
    1.13 +
    1.14 +NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF \
    1.15 +	mono Lfp Gfp Nat intr_elim indrule Inductive Finite Arith \
    1.16 +	Sexp Univ List RelPow Option
    1.17 +
    1.18 +FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
    1.19 +	ind_syntax.ML cladata.ML simpdata.ML \
    1.20 +	typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML \
    1.21 +	../Provers/hypsubst.ML ../Provers/classical.ML \
    1.22 +	../Provers/simplifier.ML ../Provers/splitter.ML \
    1.23 +	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
    1.24 +
    1.25 +$(OUT)/HOL: $(OUT)/Pure $(FILES)
    1.26 +	@$(ISABELLE_HOME)/bin/isabelle -e "make_html := $(ISABELLE_HTML);" -qu Pure HOL
    1.27 +	@chmod -w $@
    1.28 +
    1.29 +$(OUT)/Pure:
    1.30 +	@cd ../Pure; $(ISABELLE_HOME)/bin/isatool make
    1.31 +
    1.32 +
    1.33 +
    1.34 +#### Tests and examples
    1.35 +
    1.36 +ISABELLE=$(ISABELLE_HOME)/bin/isabelle -e "make_html := $(ISABELLE_HTML);" -rq
    1.37 +
    1.38 +
    1.39 +## TFL (requires integration into HOL proper)
    1.40 +
    1.41 +TFL_NAMES = mask tfl thms thry usyntax utils
    1.42 +TFL_FILES = ../TFL/ROOT.ML ../TFL/sys.sml \
    1.43 +            $(TFL_NAMES:%=../TFL/%.sig) $(TFL_NAMES:%=../TFL/%.sml)
    1.44 +
    1.45 +TFL:	$(OUT)/HOL $(TFL_FILES)
    1.46 +	$(ISABELLE) -e 'exit_use_dir"../TFL"; quit();' HOL
    1.47 +
    1.48 +
    1.49 +## IMP-semantics example
    1.50 +
    1.51 +IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
    1.52 +IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    1.53 +
    1.54 +IMP:	$(OUT)/HOL $(IMP_FILES)
    1.55 +	$(ISABELLE) -e 'exit_use_dir"IMP"; quit();' HOL
    1.56 +
    1.57 +
    1.58 +## Hoare logic
    1.59 +
    1.60 +Hoare_NAMES = Hoare Arith2 Examples
    1.61 +Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
    1.62 +	      $(Hoare_NAMES:%=Hoare/%.ML)
    1.63 +
    1.64 +Hoare:	$(OUT)/HOL $(Hoare_FILES)
    1.65 +	$(ISABELLE) -e 'exit_use_dir"Hoare"; quit();' HOL
    1.66 +
    1.67 +
    1.68 +## The integers in HOL
    1.69 +
    1.70 +INTEG_NAMES = Equiv Integ Group Ring Lagrange IntRingDefs IntRing
    1.71 +
    1.72 +INTEG_FILES = Integ/ROOT.ML \
    1.73 +	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
    1.74 +
    1.75 +Integ:	$(OUT)/HOL $(INTEG_FILES)
    1.76 +	$(ISABELLE) -e 'exit_use_dir"Integ"; quit();' HOL
    1.77 +
    1.78 +
    1.79 +## I/O Automata
    1.80 +
    1.81 +IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet \
    1.82 +		Receiver Sender
    1.83 +IOA_ABP_NAMES = Action Correctness Lemmas
    1.84 +IOA_MT_NAMES = Asig IOA Solve
    1.85 +
    1.86 +IOA_FILES = IOA/NTP/ROOT.ML IOA/ABP/ROOT.ML IOA/NTP/Spec.thy \
    1.87 + $(IOA_NTP_NAMES:%=IOA/NTP/%.thy) $(IOA_NTP_NAMES:%=IOA/NTP/%.ML) \
    1.88 + IOA/ABP/Abschannel.thy IOA/ABP/Abschannel_finite.thy IOA/ABP/Env.thy \
    1.89 + IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy IOA/ABP/Packet.thy \
    1.90 + IOA/ABP/Receiver.thy IOA/ABP/Sender.thy IOA/ABP/Spec.thy \
    1.91 + $(IOA_ABP_NAMES:%=IOA/ABP/%.thy) $(IOA_ABP_NAMES:%=IOA/ABP/%.ML) \
    1.92 + $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
    1.93 +
    1.94 +IOA:	$(OUT)/HOL $(IOA_FILES)
    1.95 +	$(ISABELLE) -e 'exit_use_dir"IOA/NTP"; quit();' HOL
    1.96 +	$(ISABELLE) -e 'exit_use_dir"IOA/ABP"; quit();' HOL
    1.97 +
    1.98 +
    1.99 +## Authentication & Security Protocols
   1.100 +
   1.101 +Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \
   1.102 +	     WooLam Yahalom Yahalom2 Public NS_Public_Bad NS_Public
   1.103 +
   1.104 +AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
   1.105 +
   1.106 +Auth:	$(OUT)/HOL $(AUTH_FILES)
   1.107 +	$(ISABELLE) -e 'exit_use_dir"Auth"; quit();' HOL
   1.108 +
   1.109 +
   1.110 +## Properties of substitutions
   1.111 +
   1.112 +SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
   1.113 +
   1.114 +SUBST_FILES = Subst/ROOT.ML \
   1.115 +	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
   1.116 +
   1.117 +Subst:	$(OUT)/HOL $(SUBST_FILES)
   1.118 +	$(ISABELLE) -e 'exit_use_dir"Subst"; quit();' HOL
   1.119 +
   1.120 +
   1.121 +## Confluence of Lambda-calculus
   1.122 +
   1.123 +LAMBDA_NAMES = Lambda ParRed Commutation Eta
   1.124 +
   1.125 +LAMBDA_FILES = Lambda/ROOT.ML \
   1.126 +	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
   1.127 +
   1.128 +Lambda:	 $(OUT)/HOL $(LAMBDA_FILES)
   1.129 +	$(ISABELLE) -e 'exit_use_dir"Lambda"; quit();' HOL
   1.130 +
   1.131 +
   1.132 +## Type inference for MiniML
   1.133 +
   1.134 +MINIML_NAMES = I Maybe MiniML Type W
   1.135 +
   1.136 +MINIML_FILES = MiniML/ROOT.ML \
   1.137 +	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
   1.138 +
   1.139 +MiniML: $(OUT)/HOL $(MINIML_FILES)
   1.140 +	$(ISABELLE) -e 'exit_use_dir"MiniML"; quit();' HOL
   1.141 +
   1.142 +
   1.143 +## Lexical analysis
   1.144 +
   1.145 +LEX_FILES = Auto AutoChopper Chopper Prefix
   1.146 +
   1.147 +LEX_FILES = Lex/ROOT.ML \
   1.148 +	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
   1.149 +
   1.150 +Lex:	$(OUT)/HOL $(LEX_FILES)
   1.151 +	$(ISABELLE) -e 'exit_use_dir"Lex"; quit();' HOL
   1.152 +
   1.153 +
   1.154 +## Miscellaneous examples
   1.155 +
   1.156 +EX_NAMES = String BT Perm Comb InSort Qsort LexProd \
   1.157 +	   Puzzle Mutil Primes NatSum SList LList Acc PropLog Term Simult MT
   1.158 +
   1.159 +EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
   1.160 +	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   1.161 +
   1.162 +ex:	$(OUT)/HOL $(EX_FILES)
   1.163 +	$(ISABELLE) -e 'exit_use_dir"ex"; quit();' HOL
   1.164 +
   1.165 +
   1.166 +## Full test
   1.167 +
   1.168 +test:	$(OUT)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda MiniML IOA ex
   1.169 +	echo 'Test examples ran successfully' > test
   1.170 +
   1.171 +
   1.172 +.PRECIOUS: $(OUT)/Pure $(OUT)/HOL