author | paulson |
Thu, 26 Sep 1996 12:50:48 +0200 | |
changeset 2032 | 1bbf1bdcaf56 |
parent 2023 | aa25f20c5d8b |
child 2091 | 644104f85d14 |
permissions | -rw-r--r-- |
1935
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
1 |
# $Id$ |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
2 |
# This Makefile allows the common theory for security logics to be |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
3 |
# built separately. |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
4 |
# |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
5 |
BIN = $(ISABELLEBIN) |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
6 |
COMP = $(ISABELLECOMP) |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
7 |
NAMES = Message Shared |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
8 |
|
1970
2818289768e9
Now uses DB-ROOT.ML, which is separate from ROOT.ML
paulson
parents:
1935
diff
changeset
|
9 |
FILES = DB-ROOT.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML) |
1935
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
10 |
|
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
11 |
$(BIN)/Auth: $(BIN)/HOL $(FILES) |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
12 |
if [ -d $${ISABELLEBIN:?}/Pure ];\ |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
13 |
then echo Bad value for ISABELLEBIN: \ |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
14 |
$(BIN) is the Isabelle source directory; \ |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
15 |
exit 1; \ |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
16 |
fi;\ |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
17 |
case "$(COMP)" in \ |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
18 |
poly*) echo 'make_database"$(BIN)/Auth"; quit();' \ |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
19 |
| $(COMP) $(BIN)/HOL;\ |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
20 |
if [ "$${MAKE_HTML}" = "true" ]; \ |
2016 | 21 |
then echo 'open PolyML; init_html(); exit_use"DB-ROOT.ML";' \ |
1935
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
22 |
| $(COMP) $(BIN)/Auth;\ |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
23 |
elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
2016 | 24 |
then echo 'open PolyML; init_html(); exit_use"DB-ROOT.ML"; make_html := false;' | $(COMP) $(BIN)/Auth;\ |
1970
2818289768e9
Now uses DB-ROOT.ML, which is separate from ROOT.ML
paulson
parents:
1935
diff
changeset
|
25 |
else echo 'open PolyML; exit_use"DB-ROOT.ML";' \ |
1935
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
26 |
| $(COMP) $(BIN)/Auth;\ |
2023
aa25f20c5d8b
Calls discgarb -c to realize dramatic space savings!
paulson
parents:
2016
diff
changeset
|
27 |
fi;\ |
aa25f20c5d8b
Calls discgarb -c to realize dramatic space savings!
paulson
parents:
2016
diff
changeset
|
28 |
discgarb -c $(BIN)/Auth;;\ |
1935
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
29 |
sml*) if [ "$${MAKE_HTML}" = "true" ]; \ |
2016 | 30 |
then echo 'init_html(); exit_use"DB-ROOT.ML"; xML"$(BIN)/Auth" banner;' | $(BIN)/HOL;\ |
1935
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
31 |
elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
2016 | 32 |
then echo 'init_html(); exit_use"DB-ROOT.ML"; make_html := false; xML"$(BIN)/Auth" banner;' \ |
1935
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
33 |
| $(BIN)/HOL;\ |
1970
2818289768e9
Now uses DB-ROOT.ML, which is separate from ROOT.ML
paulson
parents:
1935
diff
changeset
|
34 |
else echo 'exit_use"DB-ROOT.ML"; xML"$(BIN)/Auth" banner;' \ |
1935
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
35 |
| $(BIN)/HOL;\ |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
36 |
fi;;\ |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
37 |
*) echo Bad value for ISABELLECOMP: \ |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
38 |
$(COMP) is not poly or sml; exit 1;;\ |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
39 |
esac |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
40 |
|
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
41 |
$(BIN)/HOL: |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
42 |
cd ..; $(MAKE) |
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
43 |
|
ec67a0507c2a
For building the security theory as a separate database
paulson
parents:
diff
changeset
|
44 |
.PRECIOUS: $(BIN)/HOL $(BIN)/Auth |