# HG changeset patch
# User lcp
# Date 793965037 -3600
# Node ID bd26f536e1feaf78adeaf18082325efcab8fb4bc
# Parent  d03bb9f50b3b5319b32422709bba724d0f8e2683
Re-organised to perform the tests independently.  Now test
is defined in terms of separate targets IMP, ex, etc.  If ISABELLECOMP is set
wrongly then "exit 1" causes the Make to fail.  Defines the macro "LOGIC" to
refer to the right command for running the object-logic.  Uses "suffix
substitution" to shorten macro definitions.

diff -r d03bb9f50b3b -r bd26f536e1fe src/ZF/Makefile
--- a/src/ZF/Makefile	Tue Feb 28 10:33:52 1995 +0100
+++ b/src/ZF/Makefile	Tue Feb 28 10:50:37 1995 +0100
@@ -18,40 +18,18 @@
 
 BIN = $(ISABELLEBIN)
 COMP = $(ISABELLECOMP)
-FILES = ROOT.ML ZF.thy ZF.ML upair.thy upair.ML subset.thy subset.ML \
-	thy_syntax.ML pair.thy pair.ML domrange.thy domrange.ML \
-	func.thy func.ML AC.thy AC.ML simpdata.thy simpdata.ML\
-	equalities.thy equalities.ML Bool.thy Bool.ML \
-	Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \
-	../Pure/section_utils.ML ind_syntax.thy ind_syntax.ML \
-         add_ind_def.thy add_ind_def.ML \
-	intr_elim.thy intr_elim.ML indrule.thy indrule.ML \
-	Inductive.thy Inductive.ML \
-	Perm.thy Perm.ML Rel.thy Rel.ML EquivClass.ML EquivClass.thy \
-	Trancl.thy Trancl.ML \
-	WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \
-	Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \
-	QUniv.thy QUniv.ML constructor.ML Datatype.thy Datatype.ML  \
-	OrderArith.thy OrderArith.ML OrderType.thy OrderType.ML \
-	Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \
-	Cardinal_AC.thy Cardinal_AC.ML InfDatatype.thy InfDatatype.ML \
-	Zorn.thy Zorn.ML Nat.thy Nat.ML Finite.thy Finite.ML \
-	List.thy List.ML
+THYS = ZF.thy upair.thy subset.thy pair.thy domrange.thy \
+       func.thy AC.thy simpdata.thy equalities.thy Bool.thy \
+       Sum.thy QPair.thy mono.thy Fixedpt.thy ind_syntax.thy add_ind_def.thy \
+       constructor.thy intr_elim.thy indrule.thy Inductive.thy \
+       Perm.thy Rel.thy EquivClass.thy Trancl.thy \
+       WF.thy Order.thy Ordinal.thy Epsilon.thy Arith.thy Univ.thy \
+       QUniv.thy Datatype.thy OrderArith.thy OrderType.thy \
+       Cardinal.thy CardinalArith.thy Cardinal_AC.thy InfDatatype.thy \
+       Zorn.thy Nat.thy Finite.thy List.thy 
 
-IMP_FILES = IMP/ROOT.ML IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\
-            IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy
-
-EX_FILES = ex/ROOT.ML ex/misc.ML ex/Ramsey.ML ex/Ramsey.thy\
-	   ex/Integ.ML ex/Integ.thy\
-           ex/twos_compl.thy ex/twos_compl.ML ex/Bin.thy ex/Bin.ML\
-	   ex/BT.thy ex/BT.ML ex/Term.thy ex/Term.ML \
-	   ex/TF.thy ex/TF.ML ex/Ntree.thy ex/Ntree.ML \
-           ex/Brouwer.thy ex/Brouwer.ML \
-	   ex/Data.thy ex/Data.ML ex/Enum.thy ex/Enum.ML \
-	   ex/Rmap.thy ex/Rmap.ML ex/PropLog.ML ex/PropLog.thy \
-	   ex/ListN.thy ex/ListN.ML ex/Acc.thy ex/Acc.ML\
-	   ex/Comb.thy ex/Comb.ML ex/Primrec.thy ex/Primrec.ML\
-           ex/LList.thy ex/LList.ML ex/CoUnit.thy ex/CoUnit.ML
+FILES = ROOT.ML thy_syntax.ML ../Pure/section_utils.ML $(THYS) $(THYS:.thy=.ML)
+	
 
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/ZF:   $(BIN)/FOL  $(FILES) 
@@ -60,21 +38,54 @@
 		echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/ZF ;;\
 	sml*)	echo 'use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\
 	*)	echo Bad value for ISABELLECOMP: \
-                	$(COMP) is not poly or sml;;\
+                	$(COMP) is not poly or sml; exit 1;;\
 	esac
 
 $(BIN)/FOL:
 	cd ../FOL;  $(MAKE)
 
-#Directory IMP also tests the system
-#Load ex/ROOT.ML last since it creates the file "test"
-test:   $(BIN)/ZF  $(IMP_FILES) $(EX_FILES)
-	case "$(COMP)" in \
-	poly*)	echo '(use"IMP/ROOT.ML"; use"ex/ROOT.ML"); quit();' | \
-			$(COMP) $(BIN)/ZF ;;\
-	sml*)	echo '(use"IMP/ROOT.ML"; use"ex/ROOT.ML");' | $(BIN)/ZF;;\
-	*)	echo Bad value for ISABELLECOMP: \
-                	$(COMP) is not poly or sml;;\
+#### Testing of ZF
+
+#A macro referring to the object-logic (depends on ML compiler)
+LOGIC:sh=case $ISABELLECOMP in \
+	poly*)	echo "$ISABELLECOMP $ISABELLEBIN/ZF" ;;\
+	sml*)	echo "$ISABELLEBIN/ZF" ;;\
+	*)	echo "echo Bad value for ISABELLECOMP: \
+                	$ISABELLEBIN is not poly or sml; exit 1" ;;\
 	esac
 
+##IMP-semantics example
+IMP_THYS = IMP/Com.thy IMP/Denotation.thy IMP/Equiv.thy
+IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
+
+IMP:   $(BIN)/ZF  $(IMP_FILES)
+	echo 'use"IMP/ROOT.ML";quit();' | $(LOGIC)
+
+##Coinduction example
+COIND_THYS = Coind/ECR.thy Coind/Language.thy\
+	     Coind/MT.thy Coind/Map.thy Coind/Static.thy \
+	     Coind/Types.thy Coind/Values.thy 
+
+COIND_FILES = Coind/ROOT.ML Coind/BCR.thy  Coind/Dynamic.thy \
+              $(COIND_THYS) $(COIND_THYS:.thy=.ML)
+
+Coind:  $(BIN)/ZF  $(COIND_FILES)
+	echo 'use"Coind/ROOT.ML";quit();' | $(LOGIC)
+
+##Miscellaneous examples
+EX_THYS = ex/Ramsey.thy ex/Integ.thy ex/twos_compl.thy ex/Bin.thy \
+	  ex/BT.thy ex/Term.thy  ex/TF.thy ex/Ntree.thy \
+	  ex/Brouwer.thy ex/Data.thy ex/Enum.thy \
+	  ex/Rmap.thy ex/PropLog.thy ex/ListN.thy ex/Acc.thy \
+	  ex/Comb.thy ex/Primrec.thy ex/LList.thy ex/CoUnit.thy 
+EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
+
+#Test ZF by loading the examples in directory ex
+ex:     $(BIN)/ZF  $(EX_FILES)
+	echo 'use"ex/ROOT.ML";quit();' | $(LOGIC)
+
+#Full test.
+test:   $(BIN)/ZF IMP Coind ex
+	echo 'Test examples ran successfully' > test
+
 .PRECIOUS:  $(BIN)/FOL $(BIN)/ZF