# HG changeset patch # User wenzelm # Date 852624078 -3600 # Node ID 3eb12c85846c8e7b6b289f8352f7753c65b8a914 # Parent e5b407ff3100da335c4cc3fecfbd3d7813ffd38a minor tuning; added Auth/Recur; diff -r e5b407ff3100 -r 3eb12c85846c src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Jan 07 09:00:26 1997 +0100 +++ b/src/HOL/IsaMakefile Tue Jan 07 09:01:18 1997 +0100 @@ -20,17 +20,11 @@ $(NAMES:%=%.thy) $(NAMES:%=%.ML) $(OUT)/HOL: $(OUT)/Pure $(FILES) - @$(ISABELLE_HOME)/bin/isabelle -e "make_html := $(ISABELLE_HTML);" -qu Pure HOL + @$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu $(OUT)/Pure HOL @chmod -w $@ $(OUT)/Pure: - @cd ../Pure; $(ISABELLE_HOME)/bin/isatool make - - - -#### Tests and examples - -ISABELLE=$(ISABELLE_HOME)/bin/isabelle -e "make_html := $(ISABELLE_HTML);" -rq + @cd ../Pure; $(ISATOOL) make ## TFL (requires integration into HOL proper) @@ -40,16 +34,19 @@ $(TFL_NAMES:%=../TFL/%.sig) $(TFL_NAMES:%=../TFL/%.sml) TFL: $(OUT)/HOL $(TFL_FILES) - $(ISABELLE) -e 'exit_use_dir"../TFL"; quit();' HOL + @$(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) - $(ISABELLE) -e 'exit_use_dir"IMP"; quit();' HOL + @$(ISATOOL) testdir $(OUT)/HOL IMP ## Hoare logic @@ -59,7 +56,7 @@ $(Hoare_NAMES:%=Hoare/%.ML) Hoare: $(OUT)/HOL $(Hoare_FILES) - $(ISABELLE) -e 'exit_use_dir"Hoare"; quit();' HOL + @$(ISATOOL) testdir $(OUT)/HOL Hoare ## The integers in HOL @@ -70,7 +67,7 @@ $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML) Integ: $(OUT)/HOL $(INTEG_FILES) - $(ISABELLE) -e 'exit_use_dir"Integ"; quit();' HOL + @$(ISATOOL) testdir $(OUT)/HOL Integ ## I/O Automata @@ -89,19 +86,19 @@ $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML) IOA: $(OUT)/HOL $(IOA_FILES) - $(ISABELLE) -e 'exit_use_dir"IOA/NTP"; quit();' HOL - $(ISABELLE) -e 'exit_use_dir"IOA/ABP"; quit();' HOL + @$(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 \ - WooLam Yahalom Yahalom2 Public NS_Public_Bad NS_Public + 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) - $(ISABELLE) -e 'exit_use_dir"Auth"; quit();' HOL + @$(ISATOOL) testdir $(OUT)/HOL Auth ## Properties of substitutions @@ -112,7 +109,7 @@ $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML) Subst: $(OUT)/HOL $(SUBST_FILES) - $(ISABELLE) -e 'exit_use_dir"Subst"; quit();' HOL + @$(ISATOOL) testdir $(OUT)/HOL Subst ## Confluence of Lambda-calculus @@ -123,7 +120,7 @@ $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML) Lambda: $(OUT)/HOL $(LAMBDA_FILES) - $(ISABELLE) -e 'exit_use_dir"Lambda"; quit();' HOL + @$(ISATOOL) testdir $(OUT)/HOL Lambda ## Type inference for MiniML @@ -134,7 +131,7 @@ $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML) MiniML: $(OUT)/HOL $(MINIML_FILES) - $(ISABELLE) -e 'exit_use_dir"MiniML"; quit();' HOL + @$(ISATOOL) testdir $(OUT)/HOL MiniML ## Lexical analysis @@ -145,7 +142,7 @@ $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML) Lex: $(OUT)/HOL $(LEX_FILES) - $(ISABELLE) -e 'exit_use_dir"Lex"; quit();' HOL + @$(ISATOOL) testdir $(OUT)/HOL Lex ## Miscellaneous examples @@ -157,7 +154,7 @@ ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) ex: $(OUT)/HOL $(EX_FILES) - $(ISABELLE) -e 'exit_use_dir"ex"; quit();' HOL + @$(ISATOOL) testdir $(OUT)/HOL ex ## Full test