author | wenzelm |
Sat, 11 Jun 2005 23:17:28 +0200 | |
changeset 16374 | f4b7cf8975af |
parent 16285 | 75954ae8b247 |
child 16392 | 7212040b71f2 |
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 |
|
10206 | 31 |
ML_DBASE_PREFIX="" |
16374 | 32 |
ML_DBASE_SUFFIX="" |
33 |
CYGPATH="" |
|
34 |
||
35 |
case "$ML_PLATFORM" in |
|
36 |
*-cygwin) |
|
37 |
ML_DBASE_SUFFIX=".pmd" |
|
38 |
POLY="$ML_HOME/PolyML.exe" |
|
39 |
CYGPATH="cygpath -m" |
|
40 |
;; |
|
41 |
*) |
|
42 |
POLY="$ML_HOME/poly" |
|
43 |
;; |
|
44 |
esac |
|
45 |
||
10206 | 46 |
check_file "$POLY" |
2301 | 47 |
|
9765 | 48 |
case "$ML_SYSTEM" in |
49 |
polyml-4.*) |
|
10206 | 50 |
if [ -z "$ML_DBASE" ]; then |
51 |
if [ -z "$COPYDB" ]; then |
|
52 |
ML_DBASE_PREFIX="$ML_HOME/" |
|
16374 | 53 |
ML_DBASE="ML_dbase${ML_DBASE_SUFFIX}" |
10206 | 54 |
else |
16374 | 55 |
ML_DBASE="$ML_HOME/ML_dbase${ML_DBASE_SUFFIX}" |
10206 | 56 |
fi |
57 |
POLYPATH="$ML_HOME" |
|
58 |
else |
|
16374 | 59 |
POLYPATH="$(dirname "$ML_DBASE")" |
10206 | 60 |
fi |
61 |
export POLYPATH |
|
62 |
||
63 |
DISCGARB="$POLY" |
|
64 |
DISCGARB_OPTIONS="-d -c" |
|
65 |
||
9765 | 66 |
EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" |
67 |
;; |
|
68 |
*) |
|
10206 | 69 |
if [ -z "$ML_DBASE" ]; then |
70 |
ML_DBASE="$ML_HOME/ML_dbase" |
|
71 |
fi |
|
72 |
||
73 |
DISCGARB="$ML_HOME/discgarb" |
|
74 |
DISCGARB_OPTIONS="-c" |
|
75 |
check_file "$DISCGARB" |
|
76 |
||
9765 | 77 |
EXIT="val exit = PolyML.exit;" |
78 |
;; |
|
79 |
esac |
|
80 |
||
81 |
||
2301 | 82 |
## prepare databases |
83 |
||
84 |
if [ -z "$INFILE" ]; then |
|
10206 | 85 |
check_file "$ML_DBASE_PREFIX$ML_DBASE" |
86 |
INFILE="$ML_DBASE" |
|
9765 | 87 |
MLTEXT="val use = PolyML.use; $EXIT $MLTEXT" |
16285 | 88 |
case "$ML_SYSTEM" in |
89 |
polyml-4.1.[12]) |
|
90 |
DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180" |
|
91 |
;; |
|
92 |
polyml-4.1.*) |
|
93 |
DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max" |
|
94 |
;; |
|
95 |
esac |
|
10105 | 96 |
else |
97 |
COPYDB=true |
|
2301 | 98 |
fi |
99 |
||
100 |
if [ -z "$OUTFILE" ]; then |
|
101 |
DB="$INFILE" |
|
15850
30e878979457
no longer need feeder to run normal interactive sessions;
wenzelm
parents:
14981
diff
changeset
|
102 |
ML_OPTIONS="-r $ML_OPTIONS" |
2349 | 103 |
elif [ "$INFILE" -ef "$OUTFILE" ]; then |
2301 | 104 |
DB="$INFILE" |
105 |
elif [ -n "$COPYDB" ]; then |
|
2936
bd33e7aae062
fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents:
2605
diff
changeset
|
106 |
[ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } |
2548 | 107 |
cp "$INFILE" "$OUTFILE" || fail_out |
2349 | 108 |
chmod +w "$OUTFILE" || fail_out |
2301 | 109 |
DB="$OUTFILE" |
110 |
else |
|
2936
bd33e7aae062
fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents:
2605
diff
changeset
|
111 |
[ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } |
16374 | 112 |
if [ -z "$CYGPATH" ]; then |
113 |
echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE" |
|
114 |
else |
|
115 |
OUTFILE_CYGWIN="$($CYGPATH "$OUTFILE")" |
|
116 |
INFILE_CYGWIN="$($CYGPATH "$INFILE")" |
|
117 |
echo "PolyML.make_database \"$OUTFILE_CYGWIN\"; PolyML.quit();" | "$POLY" -r "$INFILE_CYGWIN" |
|
118 |
fi |
|
2301 | 119 |
[ -f "$OUTFILE" ] || fail_out |
120 |
DB="$OUTFILE" |
|
121 |
fi |
|
122 |
||
123 |
||
124 |
## run it! |
|
125 |
||
16254
1b2683e18fd2
DISCGARB_OPTIONS: proper treatment of specific polyml versions;
wenzelm
parents:
15850
diff
changeset
|
126 |
if [ -z "$TERMINATE" ]; then |
1b2683e18fd2
DISCGARB_OPTIONS: proper treatment of specific polyml versions;
wenzelm
parents:
15850
diff
changeset
|
127 |
FEEDER_OPTS="" |
1b2683e18fd2
DISCGARB_OPTIONS: proper treatment of specific polyml versions;
wenzelm
parents:
15850
diff
changeset
|
128 |
else |
1b2683e18fd2
DISCGARB_OPTIONS: proper treatment of specific polyml versions;
wenzelm
parents:
15850
diff
changeset
|
129 |
FEEDER_OPTS="-q" |
1b2683e18fd2
DISCGARB_OPTIONS: proper treatment of specific polyml versions;
wenzelm
parents:
15850
diff
changeset
|
130 |
fi |
1b2683e18fd2
DISCGARB_OPTIONS: proper treatment of specific polyml versions;
wenzelm
parents:
15850
diff
changeset
|
131 |
|
15850
30e878979457
no longer need feeder to run normal interactive sessions;
wenzelm
parents:
14981
diff
changeset
|
132 |
DB_INFO=$(ls -l "$DB" 2>/dev/null) |
30e878979457
no longer need feeder to run normal interactive sessions;
wenzelm
parents:
14981
diff
changeset
|
133 |
|
16374 | 134 |
if [ -z "$CYGPATH" ]; then |
135 |
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \ |
|
136 |
{ read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
|
137 |
else |
|
138 |
DB_CYGWIN="$($CYGPATH "$DB")" |
|
139 |
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \ |
|
140 |
{ read FPID; "$POLY" $ML_OPTIONS "$DB_CYGWIN"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
|
141 |
fi |
|
9789 | 142 |
RC="$?" |
2301 | 143 |
|
10206 | 144 |
NEW_DB_INFO=$(ls -l "$DB" 2>/dev/null) |
145 |
[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \ |
|
146 |
"$DISCGARB" $DISCGARB_OPTIONS "$OUTFILE" |
|
4505 | 147 |
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
2301 | 148 |
|
9789 | 149 |
exit "$RC" |