22 Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML |
22 Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML |
23 |
23 |
24 EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML |
24 EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML |
25 |
25 |
26 $(BIN)/CTT: $(BIN)/Pure $(FILES) |
26 $(BIN)/CTT: $(BIN)/Pure $(FILES) |
|
27 if [ -d $${ISABELLEBIN:?}/Pure ];\ |
|
28 then echo Bad value for ISABELLEBIN: \ |
|
29 $(BIN) is the Isabelle source directory; \ |
|
30 exit 1; \ |
|
31 fi;\ |
27 case "$(COMP)" in \ |
32 case "$(COMP)" in \ |
28 poly*) echo 'make_database"$(BIN)/CTT"; quit();' \ |
33 poly*) echo 'make_database"$(BIN)/CTT"; quit();' \ |
29 | $(COMP) $(BIN)/Pure;\ |
34 | $(COMP) $(BIN)/Pure;\ |
30 echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/CTT ;;\ |
35 echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/CTT ;;\ |
31 sml*) echo 'use"ROOT.ML"; xML"$(BIN)/CTT" banner;' | $(BIN)/Pure ;;\ |
36 sml*) echo 'use"ROOT.ML"; xML"$(BIN)/CTT" banner;' | $(BIN)/Pure ;;\ |
32 *) echo Bad value for ISABELLECOMP;;\ |
37 *) echo Bad value for ISABELLECOMP: \ |
|
38 $(COMP) is not poly or sml;;\ |
33 esac |
39 esac |
34 |
40 |
35 $(BIN)/Pure: |
41 $(BIN)/Pure: |
36 cd ../Pure; $(MAKE) |
42 cd ../Pure; $(MAKE) |
37 |
43 |
38 test: ex/ROOT.ML $(BIN)/CTT $(EX_FILES) |
44 test: ex/ROOT.ML $(BIN)/CTT $(EX_FILES) |
39 case "$(COMP)" in \ |
45 case "$(COMP)" in \ |
40 poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\ |
46 poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\ |
41 sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/CTT;;\ |
47 sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/CTT;;\ |
42 *) echo Bad value for ISABELLECOMP;;\ |
48 *) echo Bad value for ISABELLECOMP: \ |
|
49 $(COMP) is not poly or sml;;\ |
43 esac |
50 esac |
44 |
51 |
45 .PRECIOUS: $(BIN)/Pure $(BIN)/CTT |
52 .PRECIOUS: $(BIN)/Pure $(BIN)/CTT |