19 #Makes pure Isabelle (Pure) if this file is ABSENT -- but not |
19 #Makes pure Isabelle (Pure) if this file is ABSENT -- but not |
20 #if it is out of date, since this Makefile does not know its dependencies! |
20 #if it is out of date, since this Makefile does not know its dependencies! |
21 |
21 |
22 BIN = $(ISABELLEBIN) |
22 BIN = $(ISABELLEBIN) |
23 COMP = $(ISABELLECOMP) |
23 COMP = $(ISABELLECOMP) |
24 FILES = ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \ |
24 FILES = ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \ |
25 Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML |
25 Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML |
26 |
26 |
27 EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML |
27 EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML |
28 |
28 |
29 $(BIN)/CTT: $(BIN)/Pure $(FILES) |
29 $(BIN)/CTT: $(BIN)/Pure $(FILES) |
30 if [ -d $${ISABELLEBIN:?}/Pure ];\ |
30 if [ -d $${ISABELLEBIN:?}/Pure ];\ |
31 then echo Bad value for ISABELLEBIN: \ |
31 then echo Bad value for ISABELLEBIN: \ |
32 $(BIN) is the Isabelle source directory; \ |
32 $(BIN) is the Isabelle source directory; \ |
33 exit 1; \ |
33 exit 1; \ |
34 fi;\ |
34 fi;\ |
35 case "$(COMP)" in \ |
35 case "$(COMP)" in \ |
36 poly*) echo 'make_database"$(BIN)/CTT"; quit();' \ |
36 poly*) echo 'make_database"$(BIN)/CTT"; quit();' \ |
37 | $(COMP) $(BIN)/Pure;\ |
37 | $(COMP) $(BIN)/Pure;\ |
38 if [ "$${MAKE_HTML}" = "true" ]; \ |
38 if [ "$${MAKE_HTML}" = "true" ]; \ |
39 then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
39 then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
40 | $(COMP) $(BIN)/CTT;\ |
40 | $(COMP) $(BIN)/CTT;\ |
41 elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
41 elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
42 then echo 'open PolyML; make_html := true; exit_use_dir"."; make_html := false;' | $(COMP) $(BIN)/CTT;\ |
42 then echo 'open PolyML; make_html := true; exit_use_dir"."; make_html := false;' | $(COMP) $(BIN)/CTT;\ |
43 else echo 'open PolyML; exit_use_dir".";' \ |
43 else echo 'open PolyML; exit_use_dir".";' \ |
44 | $(COMP) $(BIN)/CTT;\ |
44 | $(COMP) $(BIN)/CTT;\ |
45 fi;\ |
45 fi;\ |
46 discgarb -c $(BIN)/CTT;;\ |
46 discgarb -c $(BIN)/CTT;;\ |
47 sml*) if [ "$${MAKE_HTML}" = "true" ]; \ |
47 sml*) if [ "$${MAKE_HTML}" = "true" ]; \ |
48 then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\ |
48 then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\ |
49 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
49 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
50 then echo 'make_html := true; exit_use_dir"."; make_html := false; xML"$(BIN)/CTT" banner;' \ |
50 then echo 'make_html := true; exit_use_dir"."; make_html := false; xML"$(BIN)/CTT" banner;' \ |
51 | $(BIN)/Pure;\ |
51 | $(BIN)/Pure;\ |
52 else echo 'exit_use_dir"."; xML"$(BIN)/CTT" banner;' \ |
52 else echo 'exit_use_dir"."; xML"$(BIN)/CTT" banner;' \ |
53 | $(BIN)/Pure;\ |
53 | $(BIN)/Pure;\ |
54 fi;;\ |
54 fi;;\ |
55 *) echo Bad value for ISABELLECOMP: \ |
55 *) echo Bad value for ISABELLECOMP: \ |
56 $(COMP) is not poly or sml;;\ |
56 $(COMP) is not poly or sml;;\ |
57 esac |
57 esac |
58 |
58 |
59 $(BIN)/Pure: |
59 $(BIN)/Pure: |
60 cd ../Pure; $(MAKE) |
60 cd ../Pure; $(MAKE) |
61 |
61 |
62 test: ex/ROOT.ML $(BIN)/CTT $(EX_FILES) |
62 test: ex/ROOT.ML $(BIN)/CTT $(EX_FILES) |
63 case "$(COMP)" in \ |
63 case "$(COMP)" in \ |
64 poly*) echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\ |
64 poly*) echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\ |
65 sml*) echo 'exit_use"ex/ROOT.ML";' | $(BIN)/CTT;;\ |
65 sml*) echo 'exit_use"ex/ROOT.ML";' | $(BIN)/CTT;;\ |
66 *) echo Bad value for ISABELLECOMP: \ |
66 *) echo Bad value for ISABELLECOMP: \ |
67 $(COMP) is not poly or sml;;\ |
67 $(COMP) is not poly or sml;;\ |
68 esac |
68 esac |
69 |
69 |
70 .PRECIOUS: $(BIN)/Pure $(BIN)/CTT |
70 .PRECIOUS: $(BIN)/Pure $(BIN)/CTT |