# # $Id$ # # IsaMakefile for HOL # #### Base system OUT = $(ISABELLE_OUTPUT_DIR) NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF \ mono Lfp Gfp Nat intr_elim indrule Inductive Finite Arith \ Sexp Univ List RelPow Option FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \ ind_syntax.ML cladata.ML simpdata.ML \ typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML \ ../Provers/hypsubst.ML ../Provers/classical.ML \ ../Provers/simplifier.ML ../Provers/splitter.ML \ $(NAMES:%=%.thy) $(NAMES:%=%.ML) $(OUT)/HOL: $(OUT)/Pure $(FILES) @$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu $(OUT)/Pure HOL @chmod -w $@ $(OUT)/Pure: @cd ../Pure; $(ISATOOL) make ## TFL (requires integration into HOL proper) TFL_NAMES = mask tfl thms thry usyntax utils TFL_FILES = ../TFL/ROOT.ML ../TFL/sys.sml \ $(TFL_NAMES:%=../TFL/%.sig) $(TFL_NAMES:%=../TFL/%.sml) TFL: $(OUT)/HOL $(TFL_FILES) @$(ISABELLE) -e 'exit_use_dir"../TFL"; quit();' HOL #### Tests and examples ## IMP-semantics example IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML) IMP: $(OUT)/HOL $(IMP_FILES) @$(ISATOOL) testdir $(OUT)/HOL IMP ## Hoare logic Hoare_NAMES = Hoare Arith2 Examples Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \ $(Hoare_NAMES:%=Hoare/%.ML) Hoare: $(OUT)/HOL $(Hoare_FILES) @$(ISATOOL) testdir $(OUT)/HOL Hoare ## The integers in HOL INTEG_NAMES = Equiv Integ Group Ring Lagrange IntRingDefs IntRing INTEG_FILES = Integ/ROOT.ML \ $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML) Integ: $(OUT)/HOL $(INTEG_FILES) @$(ISATOOL) testdir $(OUT)/HOL Integ ## I/O Automata IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet \ Receiver Sender IOA_ABP_NAMES = Action Correctness Lemmas IOA_MT_NAMES = Asig IOA Solve IOA_FILES = IOA/NTP/ROOT.ML IOA/ABP/ROOT.ML IOA/NTP/Spec.thy \ $(IOA_NTP_NAMES:%=IOA/NTP/%.thy) $(IOA_NTP_NAMES:%=IOA/NTP/%.ML) \ IOA/ABP/Abschannel.thy IOA/ABP/Abschannel_finite.thy IOA/ABP/Env.thy \ IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy IOA/ABP/Packet.thy \ IOA/ABP/Receiver.thy IOA/ABP/Sender.thy IOA/ABP/Spec.thy \ $(IOA_ABP_NAMES:%=IOA/ABP/%.thy) $(IOA_ABP_NAMES:%=IOA/ABP/%.ML) \ $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML) IOA: $(OUT)/HOL $(IOA_FILES) @$(ISATOOL) testdir $(OUT)/HOL IOA/NTP @$(ISATOOL) testdir $(OUT)/HOL IOA/ABP ## Authentication & Security Protocols Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \ Recur WooLam Yahalom Yahalom2 Public NS_Public_Bad NS_Public AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML) Auth: $(OUT)/HOL $(AUTH_FILES) @$(ISATOOL) testdir $(OUT)/HOL Auth ## Properties of substitutions SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas SUBST_FILES = Subst/ROOT.ML \ $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML) Subst: $(OUT)/HOL $(SUBST_FILES) @$(ISATOOL) testdir $(OUT)/HOL Subst ## Confluence of Lambda-calculus LAMBDA_NAMES = Lambda ParRed Commutation Eta LAMBDA_FILES = Lambda/ROOT.ML \ $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML) Lambda: $(OUT)/HOL $(LAMBDA_FILES) @$(ISATOOL) testdir $(OUT)/HOL Lambda ## Type inference without let W0_NAMES = I Maybe MiniML Type W W0_FILES = W0/ROOT.ML \ $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML) W0: $(OUT)/HOL $(W0_FILES) @$(ISATOOL) testdir $(OUT)/HOL W0 ## Type inference with let MINIML_NAMES = Generalize Instance Maybe MiniML Type W MINIML_FILES = MiniML/ROOT.ML \ $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML) MiniML: $(OUT)/HOL $(MINIML_FILES) @$(ISATOOL) testdir $(OUT)/HOL MiniML ## Lexical analysis LEX_FILES = Auto AutoChopper Chopper Prefix LEX_FILES = Lex/ROOT.ML \ $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML) Lex: $(OUT)/HOL $(LEX_FILES) @$(ISATOOL) testdir $(OUT)/HOL Lex ## Axiomatic type classes examples AXC_GROUP_FILES = Group.ML Group.thy GroupDefs.ML GroupDefs.thy \ GroupInsts.thy Monoid.thy MonoidGroupInsts.thy ROOT.ML Sigs.thy AXC_LATTICE_FILES = CLattice.ML CLattice.thy LatInsts.ML LatInsts.thy \ LatMorph.ML LatMorph.thy LatPreInsts.ML LatPreInsts.thy \ Lattice.ML Lattice.thy OrdDefs.ML OrdDefs.thy OrdInsts.thy \ Order.ML Order.thy ROOT.ML tools.ML AXC_TUTORIAL_FILES = BoolGroupInsts.thy Group.ML Group.thy Monoid.thy \ MonoidGroupInsts.thy ProdGroupInsts.thy Product.thy \ ProductInsts.thy ROOT.ML Semigroup.thy Semigroups.thy Sigs.thy \ Xor.ML Xor.thy AXCLASSES_FILES = AxClasses/ROOT.ML \ $(AXC_GROUP_FILES:%=AxClasses/Group/%) \ $(AXC_LATTICE_FILES:%=AxClasses/Lattice/%) \ $(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%) AxClasses: $(OUT)/HOL $(AXCLASSES_FILES) @$(ISATOOL) testdir $(OUT)/HOL AxClasses @$(ISATOOL) testdir $(OUT)/HOL AxClasses/Group @$(ISATOOL) testdir $(OUT)/HOL AxClasses/Lattice @$(ISATOOL) testdir $(OUT)/HOL AxClasses/Tutorial ## Miscellaneous examples EX_NAMES = String BT Perm Comb InSort Qsort LexProd \ Puzzle Mutil Primes NatSum SList LList Acc PropLog Term Simult MT EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \ ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) ex: $(OUT)/HOL $(EX_FILES) @$(ISATOOL) testdir $(OUT)/HOL ex ## Full test test: $(OUT)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda W0 MiniML \ IOA AxClasses ex echo 'Test examples ran successfully' > test .PRECIOUS: $(OUT)/Pure $(OUT)/HOL