src/HOL/Makefile
changeset 2094 2061df98aab5
parent 2091 644104f85d14
child 2117 292df12bace5
     1.1 --- a/src/HOL/Makefile	Mon Oct 14 11:08:54 1996 +0200
     1.2 +++ b/src/HOL/Makefile	Tue Oct 15 10:46:42 1996 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  # $Id$
     1.5  #########################################################################
     1.6  #									#
     1.7 -# 			Makefile for Isabelle (HOL)			#
     1.8 +#			Makefile for Isabelle (HOL)			#
     1.9  #									#
    1.10  #########################################################################
    1.11  
    1.12 @@ -22,44 +22,44 @@
    1.13  BIN = $(ISABELLEBIN)
    1.14  COMP = $(ISABELLECOMP)
    1.15  NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF \
    1.16 -        mono Lfp Gfp Nat intr_elim indrule Inductive Finite Arith \
    1.17 -        Sexp Univ List RelPow Option
    1.18 +	mono Lfp Gfp Nat intr_elim indrule Inductive Finite Arith \
    1.19 +	Sexp Univ List RelPow Option
    1.20  
    1.21  FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML\
    1.22  	ind_syntax.ML cladata.ML simpdata.ML\
    1.23  	typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML\
    1.24  	../Provers/hypsubst.ML ../Provers/classical.ML\
    1.25 -        ../Provers/simplifier.ML ../Provers/splitter.ML\
    1.26 - 	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
    1.27 +	../Provers/simplifier.ML ../Provers/splitter.ML\
    1.28 +	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
    1.29  
    1.30  $(BIN)/HOL:   $(BIN)/Pure  $(FILES) 
    1.31  	if [ -d $${ISABELLEBIN:?}/Pure ];\
    1.32 -           	then echo Bad value for ISABELLEBIN: \
    1.33 -                	$(BIN) is the Isabelle source directory; \
    1.34 -                	exit 1; \
    1.35 -           	fi;\
    1.36 +		then echo Bad value for ISABELLEBIN: \
    1.37 +			$(BIN) is the Isabelle source directory; \
    1.38 +			exit 1; \
    1.39 +		fi;\
    1.40  	case "$(COMP)" in \
    1.41  	poly*)	echo 'make_database"$(BIN)/HOL"; quit();'  \
    1.42  		  | $(COMP) $(BIN)/Pure;\
    1.43 -                if [ "$${MAKE_HTML}" = "true" ]; \
    1.44 -                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    1.45 -                       | $(COMP) $(BIN)/HOL;\
    1.46 +		if [ "$${MAKE_HTML}" = "true" ]; \
    1.47 +		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    1.48 +		       | $(COMP) $(BIN)/HOL;\
    1.49  		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.50 -                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/HOL;\
    1.51 -                else echo 'open PolyML; exit_use_dir".";' \
    1.52 -                       | $(COMP) $(BIN)/HOL;\
    1.53 -                fi;\
    1.54 +		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/HOL;\
    1.55 +		else echo 'open PolyML; exit_use_dir".";' \
    1.56 +		       | $(COMP) $(BIN)/HOL;\
    1.57 +		fi;\
    1.58  		discgarb -c $(BIN)/HOL;;\
    1.59  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    1.60 -                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\
    1.61 -                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    1.62 -                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/HOL" banner;' \
    1.63 -                       | $(BIN)/Pure;\
    1.64 -                else echo 'exit_use_dir"."; xML"$(BIN)/HOL" banner;' \
    1.65 -                       | $(BIN)/Pure;\
    1.66 -                fi;;\
    1.67 +		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\
    1.68 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    1.69 +		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/HOL" banner;' \
    1.70 +		       | $(BIN)/Pure;\
    1.71 +		else echo 'exit_use_dir"."; xML"$(BIN)/HOL" banner;' \
    1.72 +		       | $(BIN)/Pure;\
    1.73 +		fi;;\
    1.74  	*)	echo Bad value for ISABELLECOMP: \
    1.75 -                	$(COMP) is not poly or sml; exit 1;;\
    1.76 +			$(COMP) is not poly or sml; exit 1;;\
    1.77  	esac
    1.78  
    1.79  $(BIN)/Pure:
    1.80 @@ -72,45 +72,45 @@
    1.81  	poly*)	echo "$ISABELLECOMP $ISABELLEBIN/HOL" ;;\
    1.82  	sml*)	echo "$ISABELLEBIN/HOL" ;;\
    1.83  	*)	echo "echo Bad value for ISABELLECOMP: \
    1.84 -                	$ISABELLEBIN is not poly or sml; exit 1" ;;\
    1.85 +			$ISABELLEBIN is not poly or sml; exit 1" ;;\
    1.86  	esac
    1.87  
    1.88  ##IMP-semantics example
    1.89  IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
    1.90  IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    1.91  
    1.92 -IMP:    $(BIN)/HOL  $(IMP_FILES)
    1.93 +IMP:	$(BIN)/HOL  $(IMP_FILES)
    1.94  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.95 -        then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \
    1.96 -        else echo 'exit_use_dir"IMP";quit();' | $(LOGIC); \
    1.97 -        fi
    1.98 +	then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \
    1.99 +	else echo 'exit_use_dir"IMP";quit();' | $(LOGIC); \
   1.100 +	fi
   1.101  
   1.102  ##Hoare logic
   1.103  Hoare_NAMES = Hoare Arith2 Examples
   1.104  Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
   1.105 -              $(Hoare_NAMES:%=Hoare/%.ML)
   1.106 +	      $(Hoare_NAMES:%=Hoare/%.ML)
   1.107  
   1.108 -Hoare:  $(BIN)/HOL  $(Hoare_FILES)
   1.109 +Hoare:	$(BIN)/HOL  $(Hoare_FILES)
   1.110  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.111 -        then echo 'make_html := true; exit_use_dir"Hoare";quit();' | $(LOGIC);\
   1.112 -        else echo 'exit_use_dir"Hoare";quit();' | $(LOGIC); \
   1.113 -        fi
   1.114 +	then echo 'make_html := true; exit_use_dir"Hoare";quit();' | $(LOGIC);\
   1.115 +	else echo 'exit_use_dir"Hoare";quit();' | $(LOGIC); \
   1.116 +	fi
   1.117  
   1.118  ##The integers in HOL
   1.119  INTEG_NAMES = Equiv Integ 
   1.120  
   1.121  INTEG_FILES = Integ/ROOT.ML \
   1.122 -              $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
   1.123 +	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
   1.124  
   1.125 -Integ:  $(BIN)/HOL  $(INTEG_FILES)
   1.126 +Integ:	$(BIN)/HOL  $(INTEG_FILES)
   1.127  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.128 -        then echo 'make_html := true; exit_use_dir"Integ";quit();' | $(LOGIC);\
   1.129 -        else echo 'exit_use_dir"Integ";quit();' | $(LOGIC); \
   1.130 -        fi
   1.131 +	then echo 'make_html := true; exit_use_dir"Integ";quit();' | $(LOGIC);\
   1.132 +	else echo 'exit_use_dir"Integ";quit();' | $(LOGIC); \
   1.133 +	fi
   1.134  
   1.135  ##I/O Automata
   1.136  IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet\
   1.137 -                Receiver Sender
   1.138 +		Receiver Sender
   1.139  IOA_ABP_NAMES = Action Correctness Lemmas
   1.140  IOA_MT_NAMES = Asig IOA Solve
   1.141  
   1.142 @@ -122,15 +122,15 @@
   1.143   $(IOA_ABP_NAMES:%=IOA/ABP/%.thy) $(IOA_ABP_NAMES:%=IOA/ABP/%.ML)\
   1.144   $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
   1.145  
   1.146 -IOA:    $(BIN)/HOL  $(IOA_FILES)
   1.147 +IOA:	$(BIN)/HOL  $(IOA_FILES)
   1.148  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.149 -        then echo 'make_html := true; exit_use_dir"IOA/NTP";quit();' \
   1.150 -               | $(LOGIC);\
   1.151 -             echo 'make_html := true; exit_use_dir"IOA/ABP";quit();' \
   1.152 -               | $(LOGIC);\
   1.153 -        else echo 'exit_use_dir"IOA/NTP";quit();' | $(LOGIC); \
   1.154 +	then echo 'make_html := true; exit_use_dir"IOA/NTP";quit();' \
   1.155 +	       | $(LOGIC);\
   1.156 +	     echo 'make_html := true; exit_use_dir"IOA/ABP";quit();' \
   1.157 +	       | $(LOGIC);\
   1.158 +	else echo 'exit_use_dir"IOA/NTP";quit();' | $(LOGIC); \
   1.159  	     echo 'exit_use_dir"IOA/ABP";quit();' | $(LOGIC); \
   1.160 -        fi
   1.161 +	fi
   1.162  
   1.163  
   1.164  ##Authentication & Security Protocols
   1.165 @@ -138,78 +138,78 @@
   1.166  
   1.167  AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
   1.168  
   1.169 -Auth:   $(BIN)/HOL  $(AUTH_FILES)
   1.170 +Auth:	$(BIN)/HOL  $(AUTH_FILES)
   1.171  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.172 -        then echo 'make_html := true; exit_use_dir"Auth";quit();' | $(LOGIC);\
   1.173 -        else echo 'exit_use_dir"Auth";quit();' | $(LOGIC); \
   1.174 -        fi
   1.175 +	then echo 'make_html := true; exit_use_dir"Auth";quit();' | $(LOGIC);\
   1.176 +	else echo 'exit_use_dir"Auth";quit();' | $(LOGIC); \
   1.177 +	fi
   1.178  
   1.179  
   1.180  ##Properties of substitutions
   1.181  SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
   1.182  
   1.183  SUBST_FILES = Subst/ROOT.ML \
   1.184 -              $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
   1.185 +	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
   1.186  
   1.187 -Subst:  $(BIN)/HOL  $(SUBST_FILES)
   1.188 +Subst:	$(BIN)/HOL  $(SUBST_FILES)
   1.189  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.190 -        then echo 'make_html := true; exit_use_dir"Subst";quit();' | $(LOGIC);\
   1.191 -        else echo 'exit_use_dir"Subst";quit();' | $(LOGIC); \
   1.192 -        fi
   1.193 +	then echo 'make_html := true; exit_use_dir"Subst";quit();' | $(LOGIC);\
   1.194 +	else echo 'exit_use_dir"Subst";quit();' | $(LOGIC); \
   1.195 +	fi
   1.196  
   1.197  ##Confluence of Lambda-calculus
   1.198  LAMBDA_NAMES = Lambda ParRed Commutation Eta
   1.199  
   1.200  LAMBDA_FILES = Lambda/ROOT.ML \
   1.201 -              $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
   1.202 +	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
   1.203  
   1.204 -Lambda:  $(BIN)/HOL $(LAMBDA_FILES)
   1.205 +Lambda:	 $(BIN)/HOL $(LAMBDA_FILES)
   1.206  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.207 -        then echo 'make_html := true; exit_use_dir"Lambda";quit();' \
   1.208 -               | $(LOGIC);\
   1.209 -        else echo 'exit_use_dir"Lambda";quit();' | $(LOGIC); \
   1.210 -        fi
   1.211 +	then echo 'make_html := true; exit_use_dir"Lambda";quit();' \
   1.212 +	       | $(LOGIC);\
   1.213 +	else echo 'exit_use_dir"Lambda";quit();' | $(LOGIC); \
   1.214 +	fi
   1.215  
   1.216  ##Type inference for MiniML
   1.217  MINIML_NAMES = I Maybe MiniML Type W
   1.218  
   1.219  MINIML_FILES = MiniML/ROOT.ML \
   1.220 -              $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
   1.221 +	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
   1.222  
   1.223  MiniML: $(BIN)/HOL  $(MINIML_FILES)
   1.224  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.225 -        then echo 'make_html := true; exit_use_dir"MiniML";quit();' \
   1.226 -               | $(LOGIC);\
   1.227 -        else echo 'exit_use_dir"MiniML";quit();' | $(LOGIC); \
   1.228 -        fi
   1.229 +	then echo 'make_html := true; exit_use_dir"MiniML";quit();' \
   1.230 +	       | $(LOGIC);\
   1.231 +	else echo 'exit_use_dir"MiniML";quit();' | $(LOGIC); \
   1.232 +	fi
   1.233  
   1.234  ##Lexical analysis
   1.235  LEX_FILES = Auto AutoChopper Chopper Prefix
   1.236  
   1.237  LEX_FILES = Lex/ROOT.ML \
   1.238 -            $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
   1.239 +	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
   1.240  
   1.241  Lex:	$(BIN)/HOL  $(LEX_FILES)
   1.242  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.243 -        then echo 'make_html := true; exit_use_dir"Lex";quit();' | $(LOGIC);\
   1.244 -        else echo 'exit_use_dir"Lex";quit();' | $(LOGIC); \
   1.245 -        fi
   1.246 +	then echo 'make_html := true; exit_use_dir"Lex";quit();' | $(LOGIC);\
   1.247 +	else echo 'exit_use_dir"Lex";quit();' | $(LOGIC); \
   1.248 +	fi
   1.249  
   1.250  ##Miscellaneous examples
   1.251  EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
   1.252 -            Primes NatSum SList LList Acc PropLog Term Simult MT	    
   1.253 +	    Primes NatSum SList LList Acc PropLog Term Simult MT	    
   1.254  
   1.255  EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
   1.256 -           ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   1.257 +	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   1.258  
   1.259 -ex:     $(BIN)/HOL  $(EX_FILES)
   1.260 +ex:	$(BIN)/HOL  $(EX_FILES)
   1.261  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   1.262 -        then echo 'make_html := true; exit_use_dir"ex";quit();' | $(LOGIC);\
   1.263 -        else echo 'exit_use_dir"ex";quit();' | $(LOGIC); \
   1.264 -        fi
   1.265 +	then echo 'make_html := true; exit_use_dir"ex";quit();' | $(LOGIC);\
   1.266 +	else echo 'exit_use_dir"ex";quit();' | $(LOGIC); \
   1.267 +	fi
   1.268  
   1.269  #Full test.
   1.270 -test:   $(BIN)/HOL IMP Hoare Lex Integ Auth Subst Lambda MiniML IOA ex
   1.271 +test:	$(BIN)/HOL IMP Hoare Lex Integ Auth Subst Lambda MiniML IOA ex
   1.272  	echo 'Test examples ran successfully' > test
   1.273  
   1.274  .PRECIOUS:  $(BIN)/Pure $(BIN)/HOL