Target "test" now depends on examples files
authorlcp
Tue, 09 Nov 1993 16:09:34 +0100
changeset 101d4730dd72226
parent 100 e95b98536b3d
child 102 e04cb6295a3f
Target "test" now depends on examples files
src/CCL/Makefile
src/CTT/Makefile
src/Cube/Makefile
src/FOL/Makefile
src/FOLP/Makefile
     1.1 --- a/src/CCL/Makefile	Tue Nov 09 14:24:45 1993 +0100
     1.2 +++ b/src/CCL/Makefile	Tue Nov 09 16:09:34 1993 +0100
     1.3 @@ -26,6 +26,9 @@
     1.4              coinduction.ML hered.thy hered.ML trancl.thy trancl.ML\
     1.5              wfd.thy wfd.ML genrec.ML typecheck.ML eval.ML fix.thy fix.ML
     1.6  
     1.7 +EX_FILES = ex/ROOT.ML ex/flag.ML ex/flag.thy ex/list.ML ex/list.thy\
     1.8 +	   ex/nat.ML ex/nat.thy ex/stream.ML ex/stream.thy
     1.9 +
    1.10  #Uses cp rather than make_database because Poly/ML allows only 3 levels
    1.11  $(BIN)/CCL:   $(BIN)/FOL  $(SET_FILES)  $(CCL_FILES) 
    1.12  	case "$(COMP)" in \
    1.13 @@ -38,7 +41,7 @@
    1.14  $(BIN)/FOL:
    1.15  	cd ../FOL;  $(MAKE)
    1.16  
    1.17 -test:   ex/ROOT.ML  $(BIN)/CCL
    1.18 +test:   ex/ROOT.ML  $(BIN)/CCL  $(EX_FILES)
    1.19  	case "$(COMP)" in \
    1.20  	poly*)	echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CCL ;;\
    1.21  	sml*)	echo 'use"ex/ROOT.ML";' | $(BIN)/CCL;;\
     2.1 --- a/src/CTT/Makefile	Tue Nov 09 14:24:45 1993 +0100
     2.2 +++ b/src/CTT/Makefile	Tue Nov 09 16:09:34 1993 +0100
     2.3 @@ -21,6 +21,8 @@
     2.4  FILES = 	ROOT.ML ctt.thy ctt.ML bool.thy bool.ML \
     2.5  		arith.thy arith.ML rew.ML ../Provers/typedsimp.ML
     2.6  
     2.7 +EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML
     2.8 +
     2.9  $(BIN)/CTT:   $(BIN)/Pure  $(FILES) 
    2.10  	case "$(COMP)" in \
    2.11  	poly*)	echo 'make_database"$(BIN)/CTT"; quit();'  \
    2.12 @@ -33,7 +35,7 @@
    2.13  $(BIN)/Pure:
    2.14  	cd ../Pure;  $(MAKE)
    2.15  
    2.16 -test:   ex/ROOT.ML $(BIN)/CTT
    2.17 +test:   ex/ROOT.ML $(BIN)/CTT  $(EX_FILES) 
    2.18  	case "$(COMP)" in \
    2.19  	poly*)	echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\
    2.20  	sml*)	echo 'use"ex/ROOT.ML";' | $(BIN)/CTT;;\
     3.1 --- a/src/Cube/Makefile	Tue Nov 09 14:24:45 1993 +0100
     3.2 +++ b/src/Cube/Makefile	Tue Nov 09 16:09:34 1993 +0100
     3.3 @@ -19,7 +19,7 @@
     3.4  
     3.5  BIN = $(ISABELLEBIN)
     3.6  COMP = $(ISABELLECOMP)
     3.7 -FILES = 	ROOT.ML  cube.thy  cube.ML  ex.ML
     3.8 +FILES = 	ROOT.ML  cube.thy  cube.ML
     3.9  
    3.10  $(BIN)/Cube:   $(BIN)/Pure  $(FILES) 
    3.11  	case "$(COMP)" in \
     4.1 --- a/src/FOL/Makefile	Tue Nov 09 14:24:45 1993 +0100
     4.2 +++ b/src/FOL/Makefile	Tue Nov 09 16:09:34 1993 +0100
     4.3 @@ -21,6 +21,11 @@
     4.4  FILES =  ROOT.ML ifol.thy ifol.ML fol.thy fol.ML intprover.ML simpdata.ML \
     4.5  	../Provers/classical.ML ../Provers/simplifier.ML ../Provers/ind.ML
     4.6  
     4.7 +EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/if.ML ex/if.thy ex/int.ML\
     4.8 +	   ex/intro.ML ex/list.ML ex/list.thy ex/nat.ML ex/nat.thy\
     4.9 +	   ex/nat2.ML ex/nat2.thy ex/prolog.ML ex/prolog.thy ex/prop.ML\
    4.10 +	   ex/quant.ML
    4.11 +
    4.12  $(BIN)/FOL:   $(BIN)/Pure  $(FILES) 
    4.13  	case "$(COMP)" in \
    4.14  	poly*)	echo 'make_database"$(BIN)/FOL"; quit();'  \
    4.15 @@ -33,7 +38,7 @@
    4.16  $(BIN)/Pure:
    4.17  	cd ../Pure;  $(MAKE)
    4.18  
    4.19 -test:   ex/ROOT.ML  $(BIN)/FOL
    4.20 +test:   ex/ROOT.ML  $(BIN)/FOL  $(EX_FILES) 
    4.21  	case "$(COMP)" in \
    4.22  	poly*)	echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/FOL ;;\
    4.23  	sml*)	echo 'use"ex/ROOT.ML";' | $(BIN)/FOL;;\
     5.1 --- a/src/FOLP/Makefile	Tue Nov 09 14:24:45 1993 +0100
     5.2 +++ b/src/FOLP/Makefile	Tue Nov 09 16:09:34 1993 +0100
     5.3 @@ -21,6 +21,10 @@
     5.4  FILES =  ROOT.ML ifolp.thy ifolp.ML folp.thy folp.ML intprover.ML simpdata.ML\
     5.5  	 classical.ML ../Provers/simp.ML ../Provers/ind.ML
     5.6  
     5.7 +EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/if.ML ex/if.thy ex/int.ML\
     5.8 +	   ex/intro.ML ex/nat.ML ex/nat.thy ex/prolog.ML ex/prolog.thy\
     5.9 +	   ex/prop.ML ex/quant.ML
    5.10 +
    5.11  $(BIN)/FOLP:   $(BIN)/Pure  $(FILES) 
    5.12  	case "$(COMP)" in \
    5.13  	poly*)	echo 'make_database"$(BIN)/FOLP"; quit();'  \
    5.14 @@ -33,7 +37,7 @@
    5.15  $(BIN)/Pure:
    5.16  	cd ../Pure;  $(MAKE)
    5.17  
    5.18 -test:   ex/ROOT.ML  $(BIN)/FOLP
    5.19 +test:   ex/ROOT.ML  $(BIN)/FOLP  $(EX_FILES) 
    5.20  	case "$(COMP)" in \
    5.21  	poly*)	echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/FOLP ;;\
    5.22  	sml*)	echo 'use"ex/ROOT.ML";' | $(BIN)/FOLP;;\