src/FOLP/Makefile
changeset 101 d4730dd72226
parent 98 329b5ac27f6e
child 337 bd39933d107b
equal deleted inserted replaced
100:e95b98536b3d 101:d4730dd72226
    19 BIN = $(ISABELLEBIN)
    19 BIN = $(ISABELLEBIN)
    20 COMP = $(ISABELLECOMP)
    20 COMP = $(ISABELLECOMP)
    21 FILES =  ROOT.ML ifolp.thy ifolp.ML folp.thy folp.ML intprover.ML simpdata.ML\
    21 FILES =  ROOT.ML ifolp.thy ifolp.ML folp.thy folp.ML intprover.ML simpdata.ML\
    22 	 classical.ML ../Provers/simp.ML ../Provers/ind.ML
    22 	 classical.ML ../Provers/simp.ML ../Provers/ind.ML
    23 
    23 
       
    24 EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/if.ML ex/if.thy ex/int.ML\
       
    25 	   ex/intro.ML ex/nat.ML ex/nat.thy ex/prolog.ML ex/prolog.thy\
       
    26 	   ex/prop.ML ex/quant.ML
       
    27 
    24 $(BIN)/FOLP:   $(BIN)/Pure  $(FILES) 
    28 $(BIN)/FOLP:   $(BIN)/Pure  $(FILES) 
    25 	case "$(COMP)" in \
    29 	case "$(COMP)" in \
    26 	poly*)	echo 'make_database"$(BIN)/FOLP"; quit();'  \
    30 	poly*)	echo 'make_database"$(BIN)/FOLP"; quit();'  \
    27 			| $(COMP) $(BIN)/Pure;\
    31 			| $(COMP) $(BIN)/Pure;\
    28 		echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/FOLP;;\
    32 		echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/FOLP;;\
    31 	esac
    35 	esac
    32 
    36 
    33 $(BIN)/Pure:
    37 $(BIN)/Pure:
    34 	cd ../Pure;  $(MAKE)
    38 	cd ../Pure;  $(MAKE)
    35 
    39 
    36 test:   ex/ROOT.ML  $(BIN)/FOLP
    40 test:   ex/ROOT.ML  $(BIN)/FOLP  $(EX_FILES) 
    37 	case "$(COMP)" in \
    41 	case "$(COMP)" in \
    38 	poly*)	echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/FOLP ;;\
    42 	poly*)	echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/FOLP ;;\
    39 	sml*)	echo 'use"ex/ROOT.ML";' | $(BIN)/FOLP;;\
    43 	sml*)	echo 'use"ex/ROOT.ML";' | $(BIN)/FOLP;;\
    40 	*)	echo Bad value for ISABELLECOMP;;\
    44 	*)	echo Bad value for ISABELLECOMP;;\
    41 	esac
    45 	esac