Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Makefile improvements by Thomas Santen and Stephan Herrmann
authorpaulson
Wed, 27 Nov 1996 10:31:05 +0100
changeset 2235 866dbb04816c
parent 2234 041bf27011b1
child 2236 c7869a443b14
Makefile improvements by Thomas Santen and Stephan Herrmann Should be more portable across different versions of make
src/CCL/Makefile file | annotate | diff | comparison | revisions
src/CTT/Makefile file | annotate | diff | comparison | revisions
src/Cube/Makefile file | annotate | diff | comparison | revisions
src/FOL/Makefile file | annotate | diff | comparison | revisions
src/FOLP/Makefile file | annotate | diff | comparison | revisions
src/HOL/Makefile file | annotate | diff | comparison | revisions
src/HOLCF/Makefile file | annotate | diff | comparison | revisions
src/LCF/Makefile file | annotate | diff | comparison | revisions
src/Pure/Makefile file | annotate | diff | comparison | revisions
src/Sequents/Makefile file | annotate | diff | comparison | revisions
src/ZF/Makefile file | annotate | diff | comparison | revisions 
--- a/src/CCL/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/CCL/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -34,7 +34,7 @@
 
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/CCL:   $(BIN)/FOL  $(SET_FILES)	$(CCL_FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	cp $(BIN)/FOL $(BIN)/CCL;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
@@ -61,7 +61,7 @@
 	cd ../FOL;  $(MAKE)
 
 test:	ex/ROOT.ML  $(BIN)/CCL	$(EX_FILES)
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
 		       | $(COMP) $(BIN)/CCL;\
--- a/src/CTT/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/CTT/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -32,7 +32,7 @@
 			$(BIN) is the Isabelle source directory; \
 			exit 1; \
 	fi
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo 'make_database"$(BIN)/CTT"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -60,7 +60,7 @@
 	cd ../Pure;  $(MAKE)
 
 test:	ex/ROOT.ML $(BIN)/CTT  $(EX_FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\
 	sml*)	echo 'exit_use"ex/ROOT.ML";' | $(BIN)/CTT;;\
 	*)	echo Bad value for ISABELLECOMP: \
--- a/src/Cube/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/Cube/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -25,7 +25,7 @@
 FILES =		ROOT.ML	 Cube.thy  Cube.ML
 
 $(BIN)/Cube:   $(BIN)/Pure  $(FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo 'make_database"$(BIN)/Cube"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -53,7 +53,7 @@
 	cd ../Pure;  $(MAKE)
 
 test:	ex.ML $(BIN)/Cube
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo 'exit_use"ex.ML"; quit();' | $(COMP) $(BIN)/Cube ;;\
 	sml*)	echo 'exit_use"ex.ML";' | $(BIN)/Cube;;\
 	*)	echo Bad value for ISABELLECOMP: \
--- a/src/FOL/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/FOL/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -35,7 +35,7 @@
 			$(BIN) is the Isabelle source directory; \
 			exit 1; \
 	fi
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo 'make_database"$(BIN)/FOL"; quit();' \
 		  | $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -63,7 +63,7 @@
 	cd ../Pure;  $(MAKE)
 
 test:	ex/ROOT.ML  $(BIN)/FOL	$(EX_FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
 		       | $(COMP) $(BIN)/FOL;\
--- a/src/FOLP/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/FOLP/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -29,7 +29,7 @@
 	   ex/prop.ML ex/quant.ML
 
 $(BIN)/FOLP:   $(BIN)/Pure  $(FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo 'make_database"$(BIN)/FOLP"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -57,7 +57,7 @@
 	cd ../Pure;  $(MAKE)
 
 test:	ex/ROOT.ML  $(BIN)/FOLP	 $(EX_FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
 		       | $(COMP) $(BIN)/FOLP;\
--- a/src/HOL/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/HOL/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -38,7 +38,7 @@
 			$(BIN) is the Isabelle source directory; \
 			exit 1; \
 	fi
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo 'make_database"$(BIN)/HOL"; quit();'  \
 		  | $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -68,12 +68,13 @@
 #### Testing of HOL
 
 #A macro referring to the object-logic (depends on ML compiler)
-LOGIC:sh=case `expr "//$ISABELLECOMP" : '[^ ]*/\(.*\)'` in \
-	poly*)	echo "$ISABELLECOMP $ISABELLEBIN/HOL" ;;\
-	sml*)	echo "$ISABELLEBIN/HOL" ;;\
+#	[Thanks to Thomas Santen and Stephan Herrmann from GMD First]
+LOGIC=`case \`basename "$(ISABELLECOMP)"\` in \
+	poly*)	echo "$(ISABELLECOMP) $(ISABELLEBIN)/HOL" ;;\
+	sml*)	echo "$(ISABELLEBIN)/HOL" ;;\
 	*)	echo "echo; echo Bad value for ISABELLECOMP: \
-			$ISABELLECOMP is not poly or sml; exit 1" ;;\
-	esac
+			$(ISABELLECOMP) is not poly or sml; exit 1" ;;\
+	esac`
 
 ##IMP-semantics example
 IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
@@ -197,8 +198,8 @@
 	fi
 
 ##Miscellaneous examples
-EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
-	    Primes NatSum SList LList Acc PropLog Term Simult MT	    
+EX_NAMES = String BT Perm Comb InSort Qsort LexProd Group Ring Lagrange \
+	   Puzzle Mutil Primes NatSum SList LList Acc PropLog Term Simult MT
 
 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
--- a/src/HOLCF/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/HOLCF/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -34,7 +34,7 @@
 
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/HOLCF:	$(BIN)/HOL  $(FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	cp $(BIN)/HOL $(BIN)/HOLCF; chmod u+w $(BIN)/HOLCF;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
@@ -66,7 +66,7 @@
 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
 
 test:	ex/ROOT.ML  $(BIN)/HOLCF  $(EX_FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
 		       | $(COMP) $(BIN)/HOLCF;\
@@ -90,7 +90,7 @@
 			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
 
 test2:	explicit_domains/ROOT.ML  $(BIN)/HOLCF	$(EXPLICIT_DOMAINS_FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 		then echo 'make_html := true; exit_use_dir"explicit_domains";				  quit();' | $(COMP) $(BIN)/HOLCF;\
 		else echo 'exit_use_dir"explicit_domains"; quit();' \
--- a/src/LCF/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/LCF/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -25,7 +25,7 @@
 
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/LCF:   $(BIN)/FOL  $(FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	cp $(BIN)/FOL $(BIN)/LCF;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
@@ -52,7 +52,7 @@
 	cd ../FOL;  $(MAKE)
 
 test:	ex.ML  $(BIN)/LCF
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo 'exit_use"ex.ML"; quit();' | $(COMP) $(BIN)/LCF ;;\
 	sml*)	echo 'exit_use"ex.ML";' | $(BIN)/LCF;;\
 	*)	echo Bad value for ISABELLECOMP: \
--- a/src/Pure/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/Pure/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -21,7 +21,8 @@
 
 BIN = $(ISABELLEBIN)
 COMP = $(ISABELLECOMP)
-FILES =	POLY.ML NJ.ML ROOT.ML library.ML term.ML symtab.ML type.ML sign.ML\
+FILES =	POLY.ML NJ.ML NJ093.ML NJ1xx.ML ROOT.ML basis.ML library.ML\
+	term.ML symtab.ML type.ML sign.ML\
 	sequence.ML envir.ML pattern.ML unify.ML logic.ML theory.ML thm.ML\
 	net.ML display.ML deriv.ML drule.ML tctical.ML search.ML tactic.ML\
 	goals.ML axclass.ML install_pp.ML\
@@ -37,7 +38,7 @@
 
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/Pure:   $(FILES)	 $(SYNTAX_FILES)  $(THY_FILES)	$(ML_DBASE)
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
 		cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
 		echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' \
@@ -49,8 +50,8 @@
 			exit 1; \
 		fi;\
 		echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1;				     xML"$(BIN)/Pure" banner;' | $(COMP);;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
+	*)	echo Bad value for ISABELLECOMP: $(COMP); \
+		echo "   " \"`basename "$(COMP)"`\" is not poly or sml;;\
 	esac
 
 
--- a/src/Sequents/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/Sequents/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -32,7 +32,7 @@
     $(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML)
 
 $(BIN)/Sequents:   $(BIN)/Pure	$(FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo 'make_database"$(BIN)/Sequents"; quit();'	\
 			| $(COMP) $(BIN)/Pure;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
@@ -59,7 +59,7 @@
 	cd ../Pure;  $(MAKE)
 
 test:	$(BIN)/Sequents	 $(EX_FILES)
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	echo 'exit_use"ex/ROOT.ML";quit();' | $(COMP) $(BIN)/Sequents;;\
 	sml*)	echo 'exit_use"ex/ROOT.ML";' | $(BIN)/Sequents;;\
 	*)	echo Bad value for ISABELLECOMP: \
--- a/src/ZF/Makefile	Tue Nov 26 17:49:25 1996 +0100
+++ b/src/ZF/Makefile	Wed Nov 27 10:31:05 1996 +0100
@@ -35,7 +35,7 @@
 
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/ZF:   $(BIN)/FOL	 $(FILES) 
-	@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \
+	@case `basename "$(COMP)"` in \
 	poly*)	cp $(BIN)/FOL $(BIN)/ZF;\
 		if [ "$${MAKE_HTML}" = "true" ]; \
 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
@@ -64,12 +64,13 @@
 #### Testing of ZF
 
 #A macro referring to the object-logic (depends on ML compiler)
-LOGIC:sh=case `expr "//$ISABELLECOMP" : '[^ ]*/\(.*\)'` in \
-	poly*)	echo "$ISABELLECOMP $ISABELLEBIN/ZF" ;;\
-	sml*)	echo "$ISABELLEBIN/ZF" ;;\
+#	[Thanks to Thomas Santen and Stephan Herrmann from GMD First]
+LOGIC=`case \`basename "$(ISABELLECOMP)"\` in \
+	poly*)	echo "$(ISABELLECOMP) $(ISABELLEBIN)/ZF" ;;\
+	sml*)	echo "$(ISABELLEBIN)/ZF" ;;\
 	*)	echo "echo; echo Bad value for ISABELLECOMP: \
-			$ISABELLECOMP is not poly or sml; exit 1" ;;\
-	esac
+			$(ISABELLECOMP) is not poly or sml; exit 1" ;;\
+	esac`
 
 ##IMP-semantics example
 IMP_NAMES = Com Denotation Equiv
isabelle