author | berghofe |
Tue, 25 Mar 2003 09:47:05 +0100 | |
changeset 13876 | 68f4ed8311ac |
parent 13001 | 40ba2eee948e |
child 14024 | 213dcc39358f |
permissions | -rwxr-xr-x |
12721 | 1 |
#!/usr/bin/env bash |
10082 | 2 |
# |
3 |
# $Id$ |
|
4 |
# |
|
5 |
# makebin -- make Isabelle logic images for current platform. |
|
6 |
||
7 |
||
8 |
## global settings |
|
9 |
||
10 |
DISTBASE=~/tmp/isadist |
|
12427
37cfec8dfe8e
use /var/tmp (which happens to be more spacious on atbroy37);
wenzelm
parents:
11576
diff
changeset
|
11 |
TMP="/var/tmp/isabelle-makebin$$" |
10082 | 12 |
|
13 |
TAR=tar |
|
14 |
type -path gtar >/dev/null && TAR=gtar |
|
15 |
||
10097 | 16 |
export THIS_IS_ISABELLE_BUILD=true |
12985 | 17 |
export THIS_IS_ISABELLE_ADMIN=true |
10097 | 18 |
|
10082 | 19 |
|
20 |
## diagnostics |
|
21 |
||
22 |
PRG=$(basename "$0") |
|
23 |
||
24 |
function usage() |
|
25 |
{ |
|
26 |
echo |
|
12827 | 27 |
echo "Usage: $PRG [OPTIONS] ARCHIVE" |
10082 | 28 |
echo |
12827 | 29 |
echo " Options are:" |
13001 | 30 |
echo " -l produce library" |
31 |
echo " -n dry run" |
|
12827 | 32 |
echo |
33 |
echo " Precompile Isabelle for the current platform." |
|
10082 | 34 |
echo |
35 |
exit 1 |
|
36 |
} |
|
37 |
||
38 |
function fail() |
|
39 |
{ |
|
40 |
echo "$1" >&2 |
|
41 |
exit 2 |
|
42 |
} |
|
43 |
||
44 |
||
45 |
## process command line |
|
46 |
||
12827 | 47 |
# options |
48 |
||
49 |
DO_LIBRARY="" |
|
13001 | 50 |
DRY_RUN="" |
12827 | 51 |
|
13001 | 52 |
while getopts "ln" OPT |
12827 | 53 |
do |
54 |
case "$OPT" in |
|
55 |
l) |
|
56 |
DO_LIBRARY=true |
|
57 |
;; |
|
13001 | 58 |
n) |
59 |
DRY_RUN=true |
|
12827 | 60 |
;; |
61 |
\?) |
|
62 |
usage |
|
63 |
;; |
|
64 |
esac |
|
65 |
done |
|
66 |
||
67 |
shift $(($OPTIND - 1)) |
|
68 |
||
69 |
||
70 |
# args |
|
71 |
||
10082 | 72 |
[ "$#" -gt 1 ] && usage |
73 |
||
74 |
ARCHIVE="$1"; shift |
|
75 |
||
76 |
||
77 |
## main |
|
78 |
||
79 |
[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE" |
|
80 |
ARCHIVE_BASE=$(basename "$ARCHIVE") |
|
81 |
ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo "$PWD") |
|
82 |
ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE" |
|
83 |
||
84 |
ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz) |
|
85 |
ISABELLE_HOME="$TMP/$ISABELLE_NAME" |
|
86 |
||
87 |
||
88 |
# build logics |
|
89 |
||
90 |
mkdir "$TMP" || fail "Cannot create directory $TMP" |
|
91 |
||
92 |
cd "$TMP" |
|
10087 | 93 |
"$TAR" xzf "$ARCHIVE_FULL" |
10082 | 94 |
cd "$ISABELLE_NAME" |
95 |
||
13001 | 96 |
if [ -n "$DO_LIBRARY" ]; then |
97 |
perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-i true -d pdf"/' \ |
|
98 |
etc/settings |
|
99 |
else |
|
100 |
perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-p 2"/' \ |
|
101 |
etc/settings |
|
102 |
fi |
|
11576
c418146c4763
activate default ISABELLE_USEDIR_OPTIONS for precompiled distribution;
wenzelm
parents:
10307
diff
changeset
|
103 |
|
10082 | 104 |
ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER) |
105 |
[ -f "$ISABELLE_HOME_USER/etc/settings" ] && \ |
|
106 |
echo "### WARNING! Personal Isabelle settings present. " >&2 |
|
107 |
||
108 |
COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER) |
|
109 |
PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM) |
|
110 |
||
13001 | 111 |
if [ -n "$DRY_RUN" ]; then |
12827 | 112 |
mkdir -p "heaps/$COMPILER/log" |
10082 | 113 |
touch "heaps/$COMPILER/HOL" |
12827 | 114 |
touch "heaps/$COMPILER/log/HOL.gz" |
10082 | 115 |
touch "heaps/$COMPILER/HOL-Real" |
12827 | 116 |
touch "heaps/$COMPILER/log/HOL-Real.gz" |
10082 | 117 |
touch "heaps/$COMPILER/ZF" |
12827 | 118 |
touch "heaps/$COMPILER/log/ZF.gz" |
119 |
mkdir browser_info |
|
13001 | 120 |
elif [ -n "$DO_LIBRARY" ]; then |
121 |
./build -bait |
|
10082 | 122 |
else |
123 |
./build -b -m HOL-Real HOL |
|
124 |
./build -b ZF |
|
125 |
rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL" |
|
126 |
fi |
|
127 |
||
128 |
||
129 |
# prepare result |
|
130 |
||
131 |
cd "$TMP" |
|
132 |
||
133 |
chmod -R g=o "$TMP" |
|
134 |
chgrp -R isabelle "$TMP" |
|
135 |
||
13001 | 136 |
if [ -n "$DO_LIBRARY" ]; then |
137 |
"$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \ |
|
138 |
gzip -f "${ISABELLE_NAME}_library.tar" |
|
139 |
cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR" |
|
140 |
else |
|
141 |
for IMG in HOL HOL-Real ZF |
|
142 |
do |
|
143 |
"$TAR" cf "${IMG}_$PLATFORM.tar" \ |
|
144 |
"$ISABELLE_NAME/heaps/$COMPILER/$IMG" \ |
|
145 |
"$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz" |
|
146 |
gzip -f "${IMG}_$PLATFORM.tar" |
|
147 |
cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR" |
|
148 |
done |
|
149 |
fi |
|
10082 | 150 |
|
151 |
||
152 |
# clean up |
|
153 |
cd /tmp |
|
154 |
rm -rf "$TMP" |