minor tuning;
authorwenzelm
Tue Jan 07 09:01:18 1997 +0100 (1997-01-07)
changeset 24733eb12c85846c
parent 2472 e5b407ff3100
child 2474 9990f088d7ac
minor tuning;
added Auth/Recur;
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Tue Jan 07 09:00:26 1997 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jan 07 09:01:18 1997 +0100
     1.3 @@ -20,17 +20,11 @@
     1.4  	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
     1.5  
     1.6  $(OUT)/HOL: $(OUT)/Pure $(FILES)
     1.7 -	@$(ISABELLE_HOME)/bin/isabelle -e "make_html := $(ISABELLE_HTML);" -qu Pure HOL
     1.8 +	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu $(OUT)/Pure HOL
     1.9  	@chmod -w $@
    1.10  
    1.11  $(OUT)/Pure:
    1.12 -	@cd ../Pure; $(ISABELLE_HOME)/bin/isatool make
    1.13 -
    1.14 -
    1.15 -
    1.16 -#### Tests and examples
    1.17 -
    1.18 -ISABELLE=$(ISABELLE_HOME)/bin/isabelle -e "make_html := $(ISABELLE_HTML);" -rq
    1.19 +	@cd ../Pure; $(ISATOOL) make
    1.20  
    1.21  
    1.22  ## TFL (requires integration into HOL proper)
    1.23 @@ -40,16 +34,19 @@
    1.24              $(TFL_NAMES:%=../TFL/%.sig) $(TFL_NAMES:%=../TFL/%.sml)
    1.25  
    1.26  TFL:	$(OUT)/HOL $(TFL_FILES)
    1.27 -	$(ISABELLE) -e 'exit_use_dir"../TFL"; quit();' HOL
    1.28 +	@$(ISABELLE) -e 'exit_use_dir"../TFL"; quit();' HOL
    1.29 +
    1.30  
    1.31  
    1.32 +#### Tests and examples
    1.33 +
    1.34  ## IMP-semantics example
    1.35  
    1.36  IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
    1.37  IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    1.38  
    1.39  IMP:	$(OUT)/HOL $(IMP_FILES)
    1.40 -	$(ISABELLE) -e 'exit_use_dir"IMP"; quit();' HOL
    1.41 +	@$(ISATOOL) testdir $(OUT)/HOL IMP
    1.42  
    1.43  
    1.44  ## Hoare logic
    1.45 @@ -59,7 +56,7 @@
    1.46  	      $(Hoare_NAMES:%=Hoare/%.ML)
    1.47  
    1.48  Hoare:	$(OUT)/HOL $(Hoare_FILES)
    1.49 -	$(ISABELLE) -e 'exit_use_dir"Hoare"; quit();' HOL
    1.50 +	@$(ISATOOL) testdir $(OUT)/HOL Hoare
    1.51  
    1.52  
    1.53  ## The integers in HOL
    1.54 @@ -70,7 +67,7 @@
    1.55  	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
    1.56  
    1.57  Integ:	$(OUT)/HOL $(INTEG_FILES)
    1.58 -	$(ISABELLE) -e 'exit_use_dir"Integ"; quit();' HOL
    1.59 +	@$(ISATOOL) testdir $(OUT)/HOL Integ
    1.60  
    1.61  
    1.62  ## I/O Automata
    1.63 @@ -89,19 +86,19 @@
    1.64   $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
    1.65  
    1.66  IOA:	$(OUT)/HOL $(IOA_FILES)
    1.67 -	$(ISABELLE) -e 'exit_use_dir"IOA/NTP"; quit();' HOL
    1.68 -	$(ISABELLE) -e 'exit_use_dir"IOA/ABP"; quit();' HOL
    1.69 +	@$(ISATOOL) testdir $(OUT)/HOL IOA/NTP
    1.70 +	@$(ISATOOL) testdir $(OUT)/HOL IOA/ABP
    1.71  
    1.72  
    1.73  ## Authentication & Security Protocols
    1.74  
    1.75  Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \
    1.76 -	     WooLam Yahalom Yahalom2 Public NS_Public_Bad NS_Public
    1.77 +	     Recur WooLam Yahalom Yahalom2 Public NS_Public_Bad NS_Public
    1.78  
    1.79  AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
    1.80  
    1.81  Auth:	$(OUT)/HOL $(AUTH_FILES)
    1.82 -	$(ISABELLE) -e 'exit_use_dir"Auth"; quit();' HOL
    1.83 +	@$(ISATOOL) testdir $(OUT)/HOL Auth
    1.84  
    1.85  
    1.86  ## Properties of substitutions
    1.87 @@ -112,7 +109,7 @@
    1.88  	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
    1.89  
    1.90  Subst:	$(OUT)/HOL $(SUBST_FILES)
    1.91 -	$(ISABELLE) -e 'exit_use_dir"Subst"; quit();' HOL
    1.92 +	@$(ISATOOL) testdir $(OUT)/HOL Subst
    1.93  
    1.94  
    1.95  ## Confluence of Lambda-calculus
    1.96 @@ -123,7 +120,7 @@
    1.97  	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
    1.98  
    1.99  Lambda:	 $(OUT)/HOL $(LAMBDA_FILES)
   1.100 -	$(ISABELLE) -e 'exit_use_dir"Lambda"; quit();' HOL
   1.101 +	@$(ISATOOL) testdir $(OUT)/HOL Lambda
   1.102  
   1.103  
   1.104  ## Type inference for MiniML
   1.105 @@ -134,7 +131,7 @@
   1.106  	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
   1.107  
   1.108  MiniML: $(OUT)/HOL $(MINIML_FILES)
   1.109 -	$(ISABELLE) -e 'exit_use_dir"MiniML"; quit();' HOL
   1.110 +	@$(ISATOOL) testdir $(OUT)/HOL MiniML
   1.111  
   1.112  
   1.113  ## Lexical analysis
   1.114 @@ -145,7 +142,7 @@
   1.115  	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
   1.116  
   1.117  Lex:	$(OUT)/HOL $(LEX_FILES)
   1.118 -	$(ISABELLE) -e 'exit_use_dir"Lex"; quit();' HOL
   1.119 +	@$(ISATOOL) testdir $(OUT)/HOL Lex
   1.120  
   1.121  
   1.122  ## Miscellaneous examples
   1.123 @@ -157,7 +154,7 @@
   1.124  	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   1.125  
   1.126  ex:	$(OUT)/HOL $(EX_FILES)
   1.127 -	$(ISABELLE) -e 'exit_use_dir"ex"; quit();' HOL
   1.128 +	@$(ISATOOL) testdir $(OUT)/HOL ex
   1.129  
   1.130  
   1.131  ## Full test