author | paulson |
Wed, 27 Nov 1996 10:31:05 +0100 | |
changeset 2235 | 866dbb04816c |
parent 2117 | 292df12bace5 |
child 2822 | 50bac845de6f |
permissions | -rw-r--r-- |
1294 | 1 |
# $Id$ |
0 | 2 |
######################################################################### |
3 |
# # |
|
2094 | 4 |
# Makefile for Isabelle (CTT) # |
0 | 5 |
# # |
6 |
######################################################################### |
|
7 |
||
8 |
#To make the system, cd to this directory and type |
|
1294 | 9 |
# make |
0 | 10 |
#To make the system and test it on standard examples, type |
1294 | 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) |
|
2094 | 24 |
FILES = ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \ |
335 | 25 |
Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML |
0 | 26 |
|
101 | 27 |
EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML |
28 |
||
0 | 29 |
$(BIN)/CTT: $(BIN)/Pure $(FILES) |
2117 | 30 |
@if [ -d $${ISABELLEBIN:?}/Pure ];\ |
2094 | 31 |
then echo Bad value for ISABELLEBIN: \ |
32 |
$(BIN) is the Isabelle source directory; \ |
|
33 |
exit 1; \ |
|
2117 | 34 |
fi |
2235
866dbb04816c
Makefile improvements by Thomas Santen and Stephan Herrmann
paulson
parents:
2117
diff
changeset
|
35 |
@case `basename "$(COMP)"` in \ |
0 | 36 |
poly*) echo 'make_database"$(BIN)/CTT"; quit();' \ |
37 |
| $(COMP) $(BIN)/Pure;\ |
|
2094 | 38 |
if [ "$${MAKE_HTML}" = "true" ]; \ |
39 |
then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
|
40 |
| $(COMP) $(BIN)/CTT;\ |
|
1491 | 41 |
elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
2094 | 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".";' \ |
|
44 |
| $(COMP) $(BIN)/CTT;\ |
|
45 |
fi;\ |
|
2023
aa25f20c5d8b
Calls discgarb -c to realize dramatic space savings!
paulson
parents:
1491
diff
changeset
|
46 |
discgarb -c $(BIN)/CTT;;\ |
1491 | 47 |
sml*) if [ "$${MAKE_HTML}" = "true" ]; \ |
2094 | 48 |
then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\ |
49 |
elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
|
50 |
then echo 'make_html := true; exit_use_dir"."; make_html := false; xML"$(BIN)/CTT" banner;' \ |
|
51 |
| $(BIN)/Pure;\ |
|
52 |
else echo 'exit_use_dir"."; xML"$(BIN)/CTT" banner;' \ |
|
53 |
| $(BIN)/Pure;\ |
|
54 |
fi;;\ |
|
409 | 55 |
*) echo Bad value for ISABELLECOMP: \ |
2117 | 56 |
\"$(COMP)\" is not poly or sml;;\ |
0 | 57 |
esac |
58 |
||
59 |
$(BIN)/Pure: |
|
60 |
cd ../Pure; $(MAKE) |
|
61 |
||
2094 | 62 |
test: ex/ROOT.ML $(BIN)/CTT $(EX_FILES) |
2235
866dbb04816c
Makefile improvements by Thomas Santen and Stephan Herrmann
paulson
parents:
2117
diff
changeset
|
63 |
@case `basename "$(COMP)"` in \ |
953
17d7fad9c9a2
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
409
diff
changeset
|
64 |
poly*) echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\ |
17d7fad9c9a2
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
409
diff
changeset
|
65 |
sml*) echo 'exit_use"ex/ROOT.ML";' | $(BIN)/CTT;;\ |
409 | 66 |
*) echo Bad value for ISABELLECOMP: \ |
2117 | 67 |
\"$(COMP)\" is not poly or sml;;\ |
0 | 68 |
esac |
69 |
||
2094 | 70 |
.PRECIOUS: $(BIN)/Pure $(BIN)/CTT |