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 IFOLP.thy IFOLP.ML FOLP.thy FOLP.ML intprover.ML simpdata.ML\ |
24 FILES = ROOT.ML IFOLP.thy IFOLP.ML FOLP.thy FOLP.ML intprover.ML simpdata.ML\ |
25 hypsubst.ML classical.ML simp.ML |
25 hypsubst.ML classical.ML simp.ML |
26 |
26 |
27 EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/If.ML ex/If.thy ex/int.ML\ |
27 EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/If.ML ex/If.thy ex/int.ML\ |
28 ex/intro.ML ex/Nat.ML ex/Nat.thy ex/Prolog.ML ex/Prolog.thy\ |
28 ex/intro.ML ex/Nat.ML ex/Nat.thy ex/Prolog.ML ex/Prolog.thy\ |
29 ex/prop.ML ex/quant.ML |
29 ex/prop.ML ex/quant.ML |
30 |
30 |
31 $(BIN)/FOLP: $(BIN)/Pure $(FILES) |
31 $(BIN)/FOLP: $(BIN)/Pure $(FILES) |
32 case "$(COMP)" in \ |
32 case "$(COMP)" in \ |
33 poly*) echo 'make_database"$(BIN)/FOLP"; quit();' \ |
33 poly*) echo 'make_database"$(BIN)/FOLP"; quit();' \ |
34 | $(COMP) $(BIN)/Pure;\ |
34 | $(COMP) $(BIN)/Pure;\ |
35 if [ "$${MAKE_HTML}" = "true" ]; \ |
35 if [ "$${MAKE_HTML}" = "true" ]; \ |
36 then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
36 then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
37 | $(COMP) $(BIN)/FOLP;\ |
37 | $(COMP) $(BIN)/FOLP;\ |
38 elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
38 elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
39 then echo 'open PolyML; make_html := true; exit_use_dir"."; make_html := false;' | $(COMP) $(BIN)/FOLP;\ |
39 then echo 'open PolyML; make_html := true; exit_use_dir"."; make_html := false;' | $(COMP) $(BIN)/FOLP;\ |
40 else echo 'open PolyML; exit_use_dir".";' \ |
40 else echo 'open PolyML; exit_use_dir".";' \ |
41 | $(COMP) $(BIN)/FOLP;\ |
41 | $(COMP) $(BIN)/FOLP;\ |
42 fi;\ |
42 fi;\ |
43 discgarb -c $(BIN)/FOLP;;\ |
43 discgarb -c $(BIN)/FOLP;;\ |
44 sml*) if [ "$${MAKE_HTML}" = "true" ]; \ |
44 sml*) if [ "$${MAKE_HTML}" = "true" ]; \ |
45 then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;\ |
45 then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;\ |
46 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
46 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
47 then echo 'make_html := true; exit_use_dir"."; make_html := false; xML"$(BIN)/FOLP" banner;' \ |
47 then echo 'make_html := true; exit_use_dir"."; make_html := false; xML"$(BIN)/FOLP" banner;' \ |
48 | $(BIN)/Pure;\ |
48 | $(BIN)/Pure;\ |
49 else echo 'exit_use_dir"."; xML"$(BIN)/FOLP" banner;' \ |
49 else echo 'exit_use_dir"."; xML"$(BIN)/FOLP" banner;' \ |
50 | $(BIN)/Pure;\ |
50 | $(BIN)/Pure;\ |
51 fi;;\ |
51 fi;;\ |
52 *) echo Bad value for ISABELLECOMP: \ |
52 *) echo Bad value for ISABELLECOMP: \ |
53 $(COMP) is not poly or sml;;\ |
53 $(COMP) is not poly or sml;;\ |
54 esac |
54 esac |
55 |
55 |
56 $(BIN)/Pure: |
56 $(BIN)/Pure: |
57 cd ../Pure; $(MAKE) |
57 cd ../Pure; $(MAKE) |
58 |
58 |
59 test: ex/ROOT.ML $(BIN)/FOLP $(EX_FILES) |
59 test: ex/ROOT.ML $(BIN)/FOLP $(EX_FILES) |
60 case "$(COMP)" in \ |
60 case "$(COMP)" in \ |
61 poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
61 poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
62 then echo 'make_html := true; exit_use_dir"ex"; quit();' \ |
62 then echo 'make_html := true; exit_use_dir"ex"; quit();' \ |
63 | $(COMP) $(BIN)/FOLP;\ |
63 | $(COMP) $(BIN)/FOLP;\ |
64 else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOLP;\ |
64 else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOLP;\ |
65 fi;;\ |
65 fi;;\ |
66 sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
66 sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
67 then echo 'make_html := true; exit_use_dir"ex";' \ |
67 then echo 'make_html := true; exit_use_dir"ex";' \ |
68 | $(BIN)/FOLP;\ |
68 | $(BIN)/FOLP;\ |
69 else echo 'exit_use_dir"ex";' | $(BIN)/FOLP;\ |
69 else echo 'exit_use_dir"ex";' | $(BIN)/FOLP;\ |
70 fi;;\ |
70 fi;;\ |
71 *) echo Bad value for ISABELLECOMP: \ |
71 *) echo Bad value for ISABELLECOMP: \ |
72 $(COMP) is not poly or sml;;\ |
72 $(COMP) is not poly or sml;;\ |
73 esac |
73 esac |
74 |
74 |
75 .PRECIOUS: $(BIN)/Pure $(BIN)/FOLP |
75 .PRECIOUS: $(BIN)/Pure $(BIN)/FOLP |