author | wenzelm |
Sat, 08 Dec 2001 17:34:46 +0100 | |
changeset 12427 | 37cfec8dfe8e |
parent 11576 | c418146c4763 |
child 12721 | 226fc0e2e7e3 |
permissions | -rwxr-xr-x |
10082 | 1 |
#!/bin/bash |
2 |
# |
|
3 |
# $Id$ |
|
4 |
# |
|
5 |
# makebin -- make Isabelle logic images for current platform. |
|
6 |
||
7 |
||
8 |
## global settings |
|
9 |
||
10090 | 10 |
FAKE_BUILD="" |
10082 | 11 |
DISTBASE=~/tmp/isadist |
12427
37cfec8dfe8e
use /var/tmp (which happens to be more spacious on atbroy37);
wenzelm
parents:
11576
diff
changeset
|
12 |
TMP="/var/tmp/isabelle-makebin$$" |
10082 | 13 |
|
14 |
TAR=tar |
|
15 |
type -path gtar >/dev/null && TAR=gtar |
|
16 |
||
10097 | 17 |
export THIS_IS_ISABELLE_BUILD=true |
18 |
||
10082 | 19 |
|
20 |
## diagnostics |
|
21 |
||
22 |
PRG=$(basename "$0") |
|
23 |
||
24 |
function usage() |
|
25 |
{ |
|
26 |
echo |
|
27 |
echo "Usage: $PRG ARCHIVE" |
|
28 |
echo |
|
29 |
echo " Make Isabelle logic images for current platform." |
|
30 |
echo |
|
31 |
exit 1 |
|
32 |
} |
|
33 |
||
34 |
function fail() |
|
35 |
{ |
|
36 |
echo "$1" >&2 |
|
37 |
exit 2 |
|
38 |
} |
|
39 |
||
40 |
||
41 |
## process command line |
|
42 |
||
43 |
[ "$#" -gt 1 ] && usage |
|
44 |
||
45 |
ARCHIVE="$1"; shift |
|
46 |
||
47 |
||
48 |
## main |
|
49 |
||
50 |
[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE" |
|
51 |
ARCHIVE_BASE=$(basename "$ARCHIVE") |
|
52 |
ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo "$PWD") |
|
53 |
ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE" |
|
54 |
||
55 |
ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz) |
|
56 |
ISABELLE_HOME="$TMP/$ISABELLE_NAME" |
|
57 |
||
58 |
||
59 |
# build logics |
|
60 |
||
61 |
mkdir "$TMP" || fail "Cannot create directory $TMP" |
|
62 |
||
63 |
cd "$TMP" |
|
10087 | 64 |
"$TAR" xzf "$ARCHIVE_FULL" |
10082 | 65 |
cd "$ISABELLE_NAME" |
66 |
||
11576
c418146c4763
activate default ISABELLE_USEDIR_OPTIONS for precompiled distribution;
wenzelm
parents:
10307
diff
changeset
|
67 |
#activate default for precompiled distribution ... |
c418146c4763
activate default ISABELLE_USEDIR_OPTIONS for precompiled distribution;
wenzelm
parents:
10307
diff
changeset
|
68 |
perl -pi -e 's/#ISABELLE_USEDIR_OPTIONS/ISABELLE_USEDIR_OPTIONS/' etc/settings |
c418146c4763
activate default ISABELLE_USEDIR_OPTIONS for precompiled distribution;
wenzelm
parents:
10307
diff
changeset
|
69 |
|
10082 | 70 |
ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER) |
71 |
[ -f "$ISABELLE_HOME_USER/etc/settings" ] && \ |
|
72 |
echo "### WARNING! Personal Isabelle settings present. " >&2 |
|
73 |
||
74 |
COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER) |
|
75 |
PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM) |
|
76 |
||
77 |
if [ -n "$FAKE_BUILD" ]; then |
|
78 |
mkdir -p "heaps/$COMPILER" |
|
79 |
touch "heaps/$COMPILER/HOL" |
|
80 |
touch "heaps/$COMPILER/HOL-Real" |
|
81 |
touch "heaps/$COMPILER/ZF" |
|
82 |
else |
|
83 |
./build -b -m HOL-Real HOL |
|
84 |
./build -b ZF |
|
85 |
rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL" |
|
86 |
fi |
|
87 |
||
88 |
||
89 |
# prepare result |
|
90 |
||
91 |
cd "$TMP" |
|
92 |
||
93 |
chmod -R g=o "$TMP" |
|
94 |
chgrp -R isabelle "$TMP" |
|
95 |
||
96 |
for IMG in HOL HOL-Real ZF |
|
97 |
do |
|
10113 | 98 |
"$TAR" cf "${IMG}_$PLATFORM.tar" \ |
99 |
"$ISABELLE_NAME/heaps/$COMPILER/$IMG" \ |
|
100 |
"$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz" |
|
10082 | 101 |
gzip "${IMG}_$PLATFORM.tar" |
10087 | 102 |
cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR" |
10082 | 103 |
done |
104 |
||
105 |
||
106 |
# clean up |
|
107 |
cd /tmp |
|
108 |
rm -rf "$TMP" |