author | aspinall |
Fri, 27 May 2005 13:51:32 +0200 | |
changeset 16101 | 37471d84d353 |
parent 15850 | 30e878979457 |
child 16254 | 1b2683e18fd2 |
permissions | -rwxr-xr-x |
10555 | 1 |
#!/usr/bin/env bash |
2301 | 2 |
# |
2314 | 3 |
# $Id$ |
9789 | 4 |
# Author: Markus Wenzel, TU Muenchen |
2314 | 5 |
# |
2301 | 6 |
# Poly/ML startup script. |
9977 | 7 |
|
10105 | 8 |
export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE |
2301 | 9 |
|
10 |
||
11 |
## diagnostics |
|
12 |
||
2349 | 13 |
function fail_out() |
2301 | 14 |
{ |
2349 | 15 |
echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
2301 | 16 |
exit 2 |
17 |
} |
|
18 |
||
10206 | 19 |
function check_file() |
5063 | 20 |
{ |
21 |
if [ ! -f "$1" ]; then |
|
22 |
echo "Unable to locate $1" >&2 |
|
10206 | 23 |
echo "Please check your ML system settings!" >&2 |
5063 | 24 |
exit 2 |
25 |
fi |
|
26 |
} |
|
27 |
||
2301 | 28 |
|
2400 | 29 |
## Poly/ML programs |
2301 | 30 |
|
15850
30e878979457
no longer need feeder to run normal interactive sessions;
wenzelm
parents:
14981
diff
changeset
|
31 |
FEEDER="" |
10206 | 32 |
ML_DBASE_PREFIX="" |
9789 | 33 |
POLY="$ML_HOME/poly" |
10206 | 34 |
check_file "$POLY" |
2301 | 35 |
|
9765 | 36 |
case "$ML_SYSTEM" in |
37 |
polyml-4.*) |
|
10206 | 38 |
if [ -z "$ML_DBASE" ]; then |
39 |
if [ -z "$COPYDB" ]; then |
|
40 |
ML_DBASE_PREFIX="$ML_HOME/" |
|
41 |
ML_DBASE="ML_dbase" |
|
42 |
else |
|
43 |
ML_DBASE="$ML_HOME/ML_dbase" |
|
44 |
fi |
|
45 |
POLYPATH="$ML_HOME" |
|
46 |
else |
|
47 |
POLYPATH=$(dirname "$ML_DBASE") |
|
48 |
fi |
|
49 |
export POLYPATH |
|
50 |
||
51 |
DISCGARB="$POLY" |
|
52 |
DISCGARB_OPTIONS="-d -c" |
|
53 |
||
9765 | 54 |
EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" |
55 |
;; |
|
56 |
*) |
|
15850
30e878979457
no longer need feeder to run normal interactive sessions;
wenzelm
parents:
14981
diff
changeset
|
57 |
FEEDER=true |
30e878979457
no longer need feeder to run normal interactive sessions;
wenzelm
parents:
14981
diff
changeset
|
58 |
|
10206 | 59 |
if [ -z "$ML_DBASE" ]; then |
60 |
ML_DBASE="$ML_HOME/ML_dbase" |
|
61 |
fi |
|
62 |
||
63 |
DISCGARB="$ML_HOME/discgarb" |
|
64 |
DISCGARB_OPTIONS="-c" |
|
65 |
check_file "$DISCGARB" |
|
66 |
||
9765 | 67 |
EXIT="val exit = PolyML.exit;" |
68 |
;; |
|
69 |
esac |
|
70 |
||
71 |
||
2301 | 72 |
## prepare databases |
73 |
||
74 |
if [ -z "$INFILE" ]; then |
|
15850
30e878979457
no longer need feeder to run normal interactive sessions;
wenzelm
parents:
14981
diff
changeset
|
75 |
FEEDER=true |
10206 | 76 |
check_file "$ML_DBASE_PREFIX$ML_DBASE" |
77 |
INFILE="$ML_DBASE" |
|
9765 | 78 |
MLTEXT="val use = PolyML.use; $EXIT $MLTEXT" |
13965
46ad7fd03a38
use -Smax with poly 4.1.3 for maximum database space (see poly release notes)
kleing
parents:
13002
diff
changeset
|
79 |
[ "$ML_SYSTEM" = polyml-4.1.3 ] && \ |
15850
30e878979457
no longer need feeder to run normal interactive sessions;
wenzelm
parents:
14981
diff
changeset
|
80 |
DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max" |
12810 | 81 |
[ "$ML_SYSTEM" = polyml-4.1.1 -o "$ML_SYSTEM" = polyml-4.1.2 ] && \ |
13002 | 82 |
DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180" |
10105 | 83 |
else |
84 |
COPYDB=true |
|
2301 | 85 |
fi |
86 |
||
87 |
if [ -z "$OUTFILE" ]; then |
|
88 |
DB="$INFILE" |
|
15850
30e878979457
no longer need feeder to run normal interactive sessions;
wenzelm
parents:
14981
diff
changeset
|
89 |
ML_OPTIONS="-r $ML_OPTIONS" |
2349 | 90 |
elif [ "$INFILE" -ef "$OUTFILE" ]; then |
2301 | 91 |
DB="$INFILE" |
92 |
elif [ -n "$COPYDB" ]; then |
|
2936
bd33e7aae062
fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents:
2605
diff
changeset
|
93 |
[ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } |
2548 | 94 |
cp "$INFILE" "$OUTFILE" || fail_out |
2349 | 95 |
chmod +w "$OUTFILE" || fail_out |
2301 | 96 |
DB="$OUTFILE" |
97 |
else |
|
2936
bd33e7aae062
fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents:
2605
diff
changeset
|
98 |
[ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } |
9789 | 99 |
echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE" |
2301 | 100 |
[ -f "$OUTFILE" ] || fail_out |
101 |
DB="$OUTFILE" |
|
102 |
fi |
|
103 |
||
104 |
||
105 |
## run it! |
|
106 |
||
15850
30e878979457
no longer need feeder to run normal interactive sessions;
wenzelm
parents:
14981
diff
changeset
|
107 |
DB_INFO=$(ls -l "$DB" 2>/dev/null) |
30e878979457
no longer need feeder to run normal interactive sessions;
wenzelm
parents:
14981
diff
changeset
|
108 |
|
30e878979457
no longer need feeder to run normal interactive sessions;
wenzelm
parents:
14981
diff
changeset
|
109 |
if [ -n "$TERMINATE" ]; then |
30e878979457
no longer need feeder to run normal interactive sessions;
wenzelm
parents:
14981
diff
changeset
|
110 |
echo "$MLTEXT" | "$POLY" $ML_OPTIONS "$DB" |
30e878979457
no longer need feeder to run normal interactive sessions;
wenzelm
parents:
14981
diff
changeset
|
111 |
elif [ -n "$FEEDER" ]; then |
30e878979457
no longer need feeder to run normal interactive sessions;
wenzelm
parents:
14981
diff
changeset
|
112 |
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" | \ |
30e878979457
no longer need feeder to run normal interactive sessions;
wenzelm
parents:
14981
diff
changeset
|
113 |
{ read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
4505 | 114 |
else |
15850
30e878979457
no longer need feeder to run normal interactive sessions;
wenzelm
parents:
14981
diff
changeset
|
115 |
"$POLY" $ML_OPTIONS "$DB" -- "$MLTEXT" |
4505 | 116 |
fi |
117 |
||
9789 | 118 |
RC="$?" |
2301 | 119 |
|
13965
46ad7fd03a38
use -Smax with poly 4.1.3 for maximum database space (see poly release notes)
kleing
parents:
13002
diff
changeset
|
120 |
|
10206 | 121 |
NEW_DB_INFO=$(ls -l "$DB" 2>/dev/null) |
122 |
[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \ |
|
123 |
"$DISCGARB" $DISCGARB_OPTIONS "$OUTFILE" |
|
4505 | 124 |
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
2301 | 125 |
|
9789 | 126 |
exit "$RC" |