|
1 # $Id$ |
|
2 ######################################################################### |
|
3 # # |
|
4 # Makefile for Isabelle (Sequents) # |
|
5 # # |
|
6 ######################################################################### |
|
7 |
|
8 #To make the system, cd to this directory and type |
|
9 # make |
|
10 #To make the system and test it on standard examples, type |
|
11 # make test |
|
12 #To generate HTML files for every theory, set the environment variable |
|
13 #MAKE_HTML or add the parameter "MAKE_HTML=". |
|
14 |
|
15 #Environment variable ISABELLECOMP specifies the compiler. |
|
16 #Environment variable ISABELLEBIN specifies the destination directory. |
|
17 #For Poly/ML, ISABELLEBIN must begin with a / |
|
18 |
|
19 #Makes Pure if this file is ABSENT -- but not |
|
20 #if it is out of date, since this Makefile does not know its dependencies! |
|
21 |
|
22 BIN = $(ISABELLEBIN) |
|
23 COMP = $(ISABELLECOMP) |
|
24 NAMES = ILL LK S4 S43 T |
|
25 FILES = ROOT.ML Sequents.thy prover.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML) |
|
26 |
|
27 ILL_NAMES = ILL_predlog washing |
|
28 EX_FILES = ex/ROOT.ML \ |
|
29 ex/LK/ROOT.ML ex/LK/hardquant.ML ex/LK/prop.ML ex/LK/quant.ML \ |
|
30 ex/Modal/ROOT.ML ex/Modal/S43thms.ML ex/Modal/S4thms.ML ex/Modal/Tthms.ML \ |
|
31 ex/ILL/ILL_kleene_lemmas.ML \ |
|
32 $(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML) |
|
33 |
|
34 $(BIN)/Sequents: $(BIN)/Pure $(FILES) |
|
35 case "$(COMP)" in \ |
|
36 poly*) echo 'make_database"$(BIN)/Sequents"; quit();' \ |
|
37 | $(COMP) $(BIN)/Pure;\ |
|
38 if [ "$${MAKE_HTML}" = "true" ]; \ |
|
39 then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
|
40 | $(COMP) $(BIN)/Sequents;\ |
|
41 elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
|
42 then echo 'open PolyML; make_html := true; exit_use_dir"."; make_html := false;' | $(COMP) $(BIN)/Sequents;\ |
|
43 else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/Sequents;\ |
|
44 fi;\ |
|
45 discgarb -c $(BIN)/Sequents;;\ |
|
46 sml*) if [ "$${MAKE_HTML}" = "true" ]; \ |
|
47 then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/Sequents" banner;' | $(BIN)/Pure;\ |
|
48 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
|
49 then echo 'make_html := true; exit_use_dir"."; make_html := false; xML"$(BIN)/Sequents" banner;' \ |
|
50 | $(BIN)/Pure;\ |
|
51 else echo 'exit_use_dir"."; xML"$(BIN)/Sequents" banner;' \ |
|
52 | $(BIN)/Pure;\ |
|
53 fi;;\ |
|
54 *) echo Bad value for ISABELLECOMP: \ |
|
55 $(COMP) is not poly or sml;;\ |
|
56 esac |
|
57 |
|
58 $(BIN)/Pure: |
|
59 cd ../Pure; $(MAKE) |
|
60 |
|
61 test: $(BIN)/Sequents $(EX_FILES) |
|
62 case "$(COMP)" in \ |
|
63 poly*) echo 'exit_use"ex/ROOT.ML";quit();' | $(COMP) $(BIN)/Sequents;;\ |
|
64 sml*) echo 'exit_use"ex/ROOT.ML";' | $(BIN)/Sequents;;\ |
|
65 *) echo Bad value for ISABELLECOMP: \ |
|
66 $(COMP) is not poly or sml;;\ |
|
67 esac |
|
68 |
|
69 |
|
70 |
|
71 |
|
72 .PRECIOUS: $(BIN)/Pure $(BIN)/Sequents |