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