src/HOL/IsaMakefile
changeset 34205 f69cd974bc4e
parent 34126 8a2c5d7aff51
child 34228 bc0cea4cae52
     1.1 --- a/src/HOL/IsaMakefile	Mon Dec 28 23:34:36 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Dec 29 16:20:39 2009 +0100
     1.3 @@ -17,6 +17,7 @@
     1.4    HOL-NSA \
     1.5    HOL-Nominal \
     1.6    HOL-Plain \
     1.7 +  HOL-Proofs \
     1.8    HOL-SMT \
     1.9    HOL-Word \
    1.10    HOL4 \
    1.11 @@ -30,7 +31,6 @@
    1.12    HOL-Bali \
    1.13    HOL-Boogie-Examples \
    1.14    HOL-Decision_Procs \
    1.15 -  HOL-Extraction \
    1.16    HOL-Hahn_Banach \
    1.17    HOL-Hoare \
    1.18    HOL-Hoare_Parallel \
    1.19 @@ -41,7 +41,6 @@
    1.20    HOL-Import \
    1.21    HOL-Induct \
    1.22    HOL-Isar_Examples \
    1.23 -  HOL-Lambda \
    1.24    HOL-Lattice \
    1.25    HOL-Matrix \
    1.26    HOL-Metis_Examples \
    1.27 @@ -55,6 +54,8 @@
    1.28    HOL-Old_Number_Theory \
    1.29    HOL-Probability \
    1.30    HOL-Prolog \
    1.31 +  HOL-Proofs-Extraction \
    1.32 +  HOL-Proofs-Lambda \
    1.33    HOL-SET_Protocol \
    1.34    HOL-SMT-Examples \
    1.35    HOL-Statespace \
    1.36 @@ -69,8 +70,6 @@
    1.37    HOL-ZF
    1.38      # ^ this is the sort position
    1.39  
    1.40 -proofterms: HOL HOL-Extraction HOL-Lambda
    1.41 -
    1.42  all: test images
    1.43  
    1.44  
    1.45 @@ -91,6 +90,8 @@
    1.46  
    1.47  HOL-Main: Pure $(OUT)/HOL-Main
    1.48  
    1.49 +HOL-Proofs: Pure $(OUT)/HOL-Proofs
    1.50 +
    1.51  Pure:
    1.52  	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
    1.53  
    1.54 @@ -324,7 +325,7 @@
    1.55  $(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
    1.56  	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
    1.57  
    1.58 -$(OUT)/HOL: ROOT.ML $(MAIN_DEPENDENCIES) \
    1.59 +HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
    1.60    Archimedean_Field.thy \
    1.61    Complex.thy \
    1.62    Complex_Main.thy \
    1.63 @@ -357,7 +358,13 @@
    1.64    Tools/Qelim/ferrante_rackoff.ML \
    1.65    Tools/Qelim/langford_data.ML \
    1.66    Tools/Qelim/langford.ML
    1.67 -	@$(ISABELLE_TOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
    1.68 +
    1.69 +$(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES)
    1.70 +	@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL
    1.71 +
    1.72 +$(OUT)/HOL-Proofs: ROOT.ML $(HOL_DEPENDENCIES)
    1.73 +	@$(ISABELLE_TOOL) usedir -b -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs
    1.74 +
    1.75  
    1.76  
    1.77  ## HOL-Library
    1.78 @@ -800,17 +807,17 @@
    1.79  	@$(ISABELLE_TOOL) usedir -D generated $(OUT)/HOL Docs
    1.80  
    1.81  
    1.82 -## HOL-Lambda
    1.83 +## HOL-Proofs-Lambda
    1.84  
    1.85 -HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
    1.86 +HOL-Proofs-Lambda: HOL-Proofs $(LOG)/HOL-Proofs-Lambda.gz
    1.87  
    1.88 -$(LOG)/HOL-Lambda.gz: $(OUT)/HOL Lambda/Commutation.thy Lambda/Eta.thy	\
    1.89 -  Lambda/InductTermi.thy Lambda/Lambda.thy Lambda/ListApplication.thy	\
    1.90 -  Lambda/ListBeta.thy Lambda/ListOrder.thy Lambda/NormalForm.thy	\
    1.91 -  Lambda/ParRed.thy Lambda/Standardization.thy Lambda/StrongNorm.thy	\
    1.92 -  Lambda/Type.thy Lambda/WeakNorm.thy Lambda/ROOT.ML			\
    1.93 -  Lambda/document/root.bib Lambda/document/root.tex
    1.94 -	@$(ISABELLE_TOOL) usedir -g true -m no_brackets $(OUT)/HOL Lambda
    1.95 +$(LOG)/HOL-Proofs-Lambda.gz: $(OUT)/HOL-Proofs Lambda/Commutation.thy	\
    1.96 +  Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy		\
    1.97 +  Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy	\
    1.98 +  Lambda/NormalForm.thy Lambda/ParRed.thy Lambda/Standardization.thy	\
    1.99 +  Lambda/StrongNorm.thy Lambda/Type.thy Lambda/WeakNorm.thy		\
   1.100 +  Lambda/ROOT.ML Lambda/document/root.bib Lambda/document/root.tex
   1.101 +	@$(ISABELLE_TOOL) usedir -g true -m no_brackets $(OUT)/HOL-Proofs Lambda
   1.102  
   1.103  
   1.104  ## HOL-Prolog
   1.105 @@ -893,17 +900,17 @@
   1.106  	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
   1.107  
   1.108  
   1.109 -## HOL-Extraction
   1.110 +## HOL-Proofs-Extraction
   1.111  
   1.112 -HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
   1.113 +HOL-Proofs-Extraction: HOL-Proofs $(LOG)/HOL-Proofs-Extraction.gz
   1.114  
   1.115 -$(LOG)/HOL-Extraction.gz: $(OUT)/HOL Library/Efficient_Nat.thy	\
   1.116 -  Extraction/Euclid.thy Extraction/Greatest_Common_Divisor.thy	\
   1.117 -  Extraction/Higman.thy Extraction/Pigeonhole.thy		\
   1.118 -  Extraction/QuotRem.thy Extraction/ROOT.ML Extraction/Util.thy	\
   1.119 -  Extraction/Warshall.thy Extraction/document/root.tex		\
   1.120 -  Extraction/document/root.bib
   1.121 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Extraction
   1.122 +$(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs			\
   1.123 +  Library/Efficient_Nat.thy Extraction/Euclid.thy			\
   1.124 +  Extraction/Greatest_Common_Divisor.thy Extraction/Higman.thy		\
   1.125 +  Extraction/Pigeonhole.thy Extraction/QuotRem.thy Extraction/ROOT.ML	\
   1.126 +  Extraction/Util.thy Extraction/Warshall.thy				\
   1.127 +  Extraction/document/root.tex Extraction/document/root.bib
   1.128 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL-Proofs Extraction
   1.129  
   1.130  
   1.131  ## HOL-IOA
   1.132 @@ -1417,18 +1424,17 @@
   1.133  	@rm -f $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz			\
   1.134  		$(LOG)/HOL-Bali.gz $(LOG)/HOL-Base.gz			\
   1.135  		$(LOG)/HOL-Boogie-Examples.gz $(LOG)/HOL-Boogie.gz	\
   1.136 -		$(LOG)/HOL-Decision_Procs.gz $(LOG)/HOL-Extraction.gz	\
   1.137 -		$(LOG)/HOL-Hahn_Banach.gz $(LOG)/HOL-Hoare.gz		\
   1.138 -		$(LOG)/HOL-Hoare_Parallel.gz $(LOG)/HOL-IMP.gz		\
   1.139 -		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz			\
   1.140 +		$(LOG)/HOL-Decision_Procs.gz $(LOG)/HOL-Hahn_Banach.gz	\
   1.141 +		$(LOG)/HOL-Hoare.gz $(LOG)/HOL-Hoare_Parallel.gz	\
   1.142 +		$(LOG)/HOL-IMP.gz $(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz	\
   1.143  		$(LOG)/HOL-Imperative_HOL.gz $(LOG)/HOL-Import.gz	\
   1.144  		$(LOG)/HOL-Induct.gz $(LOG)/HOL-Isar_Examples.gz	\
   1.145 -		$(LOG)/HOL-Lambda.gz $(LOG)/HOL-Lattice			\
   1.146 -		$(LOG)/HOL-Lattice.gz $(LOG)/HOL-Lex.gz			\
   1.147 -		$(LOG)/HOL-Library.gz $(LOG)/HOL-Main.gz		\
   1.148 -		$(LOG)/HOL-Matrix $(LOG)/HOL-Matrix.gz			\
   1.149 -		$(LOG)/HOL-Metis_Examples.gz $(LOG)/HOL-MicroJava.gz	\
   1.150 -		$(LOG)/HOL-Mirabelle.gz $(LOG)/HOL-Modelcheck.gz	\
   1.151 +		$(LOG)/HOL-Lattice $(LOG)/HOL-Lattice.gz		\
   1.152 +		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Library.gz			\
   1.153 +		$(LOG)/HOL-Main.gz $(LOG)/HOL-Matrix			\
   1.154 +		$(LOG)/HOL-Matrix.gz $(LOG)/HOL-Metis_Examples.gz	\
   1.155 +		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-Mirabelle.gz		\
   1.156 +		$(LOG)/HOL-Modelcheck.gz				\
   1.157  		$(LOG)/HOL-Multivariate_Analysis.gz			\
   1.158  		$(LOG)/HOL-NSA-Examples.gz $(LOG)/HOL-NSA.gz		\
   1.159  		$(LOG)/HOL-NanoJava.gz $(LOG)/HOL-Nitpick_Examples.gz	\
   1.160 @@ -1436,8 +1442,9 @@
   1.161  		$(LOG)/HOL-Number_Theory.gz				\
   1.162  		$(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz	\
   1.163  		$(LOG)/HOL-Probability.gz $(LOG)/HOL-Prolog.gz		\
   1.164 -		$(LOG)/HOL-SET_Protocol.gz $(LOG)/HOL-SMT-Examples.gz	\
   1.165 -		$(LOG)/HOL-SMT.gz					\
   1.166 +		$(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-Extraction.gz	\
   1.167 +		$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz	\
   1.168 +		$(LOG)/HOL-SMT-Examples.gz $(LOG)/HOL-SMT.gz		\
   1.169  		$(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz		\
   1.170  		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz			\
   1.171  		$(LOG)/HOL-W0.gz $(LOG)/HOL-Word-Examples.gz		\
   1.172 @@ -1447,5 +1454,5 @@
   1.173  		$(OUT)/HOL $(OUT)/HOL-Algebra $(OUT)/HOL-Base		\
   1.174  		$(OUT)/HOL-Boogie $(OUT)/HOL-Main			\
   1.175  		$(OUT)/HOL-Multivariate_Analysis $(OUT)/HOL-NSA		\
   1.176 -		$(OUT)/HOL-Nominal $(OUT)/HOL-Plain $(OUT)/HOL-SMT	\
   1.177 -		$(OUT)/HOL-Word $(OUT)/HOL4 $(OUT)/TLA
   1.178 +		$(OUT)/HOL-Nominal $(OUT)/HOL-Plain $(OUT)/HOL-Proofs	\
   1.179 +		$(OUT)/HOL-SMT $(OUT)/HOL-Word $(OUT)/HOL4 $(OUT)/TLA