author | paulson |
Wed, 21 Aug 1996 13:22:23 +0200 | |
changeset 1933 | 8b24773de6db |
parent 1550 | f945e3a96b35 |
child 2023 | aa25f20c5d8b |
permissions | -rw-r--r-- |
1296 | 1 |
# $Id$ |
0 | 2 |
######################################################################### |
3 |
# # |
|
4 |
# Makefile for Isabelle (FOL) # |
|
5 |
# # |
|
6 |
######################################################################### |
|
7 |
||
8 |
#To make the system, cd to this directory and type |
|
1296 | 9 |
# make |
0 | 10 |
#To make the system and test it on standard examples, type |
1296 | 11 |
# make test |
12 |
#To generate HTML files for every theory, set the environment variable |
|
13 |
#MAKE_HTML or add the parameter "MAKE_HTML=". |
|
0 | 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 Isabelle (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) |
|
336 | 24 |
FILES = ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \ |
953
17d7fad9c9a2
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
940
diff
changeset
|
25 |
../Provers/hypsubst.ML ../Provers/classical.ML \ |
17d7fad9c9a2
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
940
diff
changeset
|
26 |
../Provers/simplifier.ML ../Provers/splitter.ML ../Provers/ind.ML |
0 | 27 |
|
1550
f945e3a96b35
EX_FILES includes new oracle examples, and uses the
paulson
parents:
1491
diff
changeset
|
28 |
EX_NAMES = If List Nat Nat2 Prolog declIffOracle IffOracle |
f945e3a96b35
EX_FILES includes new oracle examples, and uses the
paulson
parents:
1491
diff
changeset
|
29 |
EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/int.ML ex/intro.ML\ |
f945e3a96b35
EX_FILES includes new oracle examples, and uses the
paulson
parents:
1491
diff
changeset
|
30 |
ex/prop.ML ex/quant.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
101 | 31 |
|
0 | 32 |
$(BIN)/FOL: $(BIN)/Pure $(FILES) |
409 | 33 |
if [ -d $${ISABELLEBIN:?}/Pure ];\ |
34 |
then echo Bad value for ISABELLEBIN: \ |
|
35 |
$(BIN) is the Isabelle source directory; \ |
|
36 |
exit 1; \ |
|
37 |
fi;\ |
|
0 | 38 |
case "$(COMP)" in \ |
1296 | 39 |
poly*) echo 'make_database"$(BIN)/FOL"; quit();' \ |
40 |
| $(COMP) $(BIN)/Pure;\ |
|
1491 | 41 |
if [ "$${MAKE_HTML}" = "true" ]; \ |
1356 | 42 |
then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
1296 | 43 |
| $(COMP) $(BIN)/FOL;\ |
1491 | 44 |
elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
45 |
then echo 'open PolyML; make_html := true; exit_use_dir"."; make_html := false;' | $(COMP) $(BIN)/FOL;\ |
|
46 |
else echo 'open PolyML; exit_use_dir".";' \ |
|
1356 | 47 |
| $(COMP) $(BIN)/FOL;\ |
1296 | 48 |
fi;;\ |
1491 | 49 |
sml*) if [ "$${MAKE_HTML}" = "true" ]; \ |
1356 | 50 |
then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;\ |
1491 | 51 |
elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
52 |
then echo 'make_html := true; exit_use_dir"."; make_html := false; xML"$(BIN)/FOL" banner;' \ |
|
53 |
| $(BIN)/Pure;\ |
|
1356 | 54 |
else echo 'exit_use_dir"."; xML"$(BIN)/FOL" banner;' \ |
1296 | 55 |
| $(BIN)/Pure;\ |
56 |
fi;;\ |
|
409 | 57 |
*) echo Bad value for ISABELLECOMP: \ |
58 |
$(COMP) is not poly or sml;;\ |
|
0 | 59 |
esac |
60 |
||
61 |
$(BIN)/Pure: |
|
62 |
cd ../Pure; $(MAKE) |
|
63 |
||
101 | 64 |
test: ex/ROOT.ML $(BIN)/FOL $(EX_FILES) |
0 | 65 |
case "$(COMP)" in \ |
1491 | 66 |
poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
67 |
then echo 'make_html := true; exit_use_dir"ex"; quit();' \ |
|
68 |
| $(COMP) $(BIN)/FOL;\ |
|
69 |
else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOL;\ |
|
70 |
fi;;\ |
|
71 |
sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
|
72 |
then echo 'make_html := true; exit_use_dir"ex";' \ |
|
73 |
| $(BIN)/FOL;\ |
|
74 |
else echo 'exit_use_dir"ex";' | $(BIN)/FOL;\ |
|
75 |
fi;;\ |
|
409 | 76 |
*) echo Bad value for ISABELLECOMP: \ |
77 |
$(COMP) is not poly or sml;;\ |
|
0 | 78 |
esac |
79 |
||
80 |
.PRECIOUS: $(BIN)/Pure $(BIN)/FOL |