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