author | wenzelm |
Sat, 20 Dec 2008 11:55:34 +0100 | |
changeset 29145 | b1c6f4563df7 |
parent 26215 | 94d32a7cd0fb |
permissions | -rwxr-xr-x |
wenzelm@26215 | 1 |
#!/usr/bin/env bash |
wenzelm@26215 | 2 |
# |
wenzelm@26215 | 3 |
# Author: Markus Wenzel, TU Muenchen |
wenzelm@26215 | 4 |
# |
wenzelm@26215 | 5 |
# Poly/ML 4.x startup script. |
wenzelm@26215 | 6 |
|
wenzelm@26215 | 7 |
export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE |
wenzelm@26215 | 8 |
|
wenzelm@26215 | 9 |
|
wenzelm@26215 | 10 |
## diagnostics |
wenzelm@26215 | 11 |
|
wenzelm@26215 | 12 |
function fail_out() |
wenzelm@26215 | 13 |
{ |
wenzelm@26215 | 14 |
echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
wenzelm@26215 | 15 |
exit 2 |
wenzelm@26215 | 16 |
} |
wenzelm@26215 | 17 |
|
wenzelm@26215 | 18 |
function check_file() |
wenzelm@26215 | 19 |
{ |
wenzelm@26215 | 20 |
if [ ! -f "$1" ]; then |
wenzelm@26215 | 21 |
echo "Unable to locate $1" >&2 |
wenzelm@26215 | 22 |
echo "Please check your ML system settings!" >&2 |
wenzelm@26215 | 23 |
exit 2 |
wenzelm@26215 | 24 |
fi |
wenzelm@26215 | 25 |
} |
wenzelm@26215 | 26 |
|
wenzelm@26215 | 27 |
|
wenzelm@26215 | 28 |
## Poly/ML executable and database |
wenzelm@26215 | 29 |
|
wenzelm@26215 | 30 |
ML_DBASE_PREFIX="" |
wenzelm@26215 | 31 |
|
wenzelm@26215 | 32 |
POLY="$ML_HOME/poly" |
wenzelm@26215 | 33 |
check_file "$POLY" |
wenzelm@26215 | 34 |
|
wenzelm@26215 | 35 |
if [ -z "$ML_DBASE" ]; then |
wenzelm@26215 | 36 |
if [ ! -e "$ML_HOME/ML_dbase" -a "$(basename "$ML_HOME")" = bin ]; then |
wenzelm@26215 | 37 |
ML_DBASE_HOME="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib/poly; pwd)" |
wenzelm@26215 | 38 |
else |
wenzelm@26215 | 39 |
ML_DBASE_HOME="$ML_HOME" |
wenzelm@26215 | 40 |
fi |
wenzelm@26215 | 41 |
if [ -z "$COPYDB" ]; then |
wenzelm@26215 | 42 |
ML_DBASE_PREFIX="$ML_DBASE_HOME/" |
wenzelm@26215 | 43 |
ML_DBASE="ML_dbase" |
wenzelm@26215 | 44 |
else |
wenzelm@26215 | 45 |
ML_DBASE="$ML_DBASE_HOME/ML_dbase" |
wenzelm@26215 | 46 |
fi |
wenzelm@26215 | 47 |
export POLYPATH="$ML_DBASE_HOME" |
wenzelm@26215 | 48 |
else |
wenzelm@26215 | 49 |
export POLYPATH="$(dirname "$ML_DBASE")" |
wenzelm@26215 | 50 |
fi |
wenzelm@26215 | 51 |
|
wenzelm@26215 | 52 |
DISCGARB_OPTIONS="-d -c" |
wenzelm@26215 | 53 |
|
wenzelm@26215 | 54 |
EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" |
wenzelm@26215 | 55 |
|
wenzelm@26215 | 56 |
|
wenzelm@26215 | 57 |
## prepare databases |
wenzelm@26215 | 58 |
|
wenzelm@26215 | 59 |
if [ -z "$INFILE" ]; then |
wenzelm@26215 | 60 |
check_file "$ML_DBASE_PREFIX$ML_DBASE" |
wenzelm@26215 | 61 |
INFILE="$ML_DBASE" |
wenzelm@26215 | 62 |
MLTEXT="val use = PolyML.use; $EXIT $MLTEXT" |
wenzelm@26215 | 63 |
DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max" |
wenzelm@26215 | 64 |
else |
wenzelm@26215 | 65 |
COPYDB=true |
wenzelm@26215 | 66 |
fi |
wenzelm@26215 | 67 |
|
wenzelm@26215 | 68 |
if [ -z "$OUTFILE" ]; then |
wenzelm@26215 | 69 |
DB="$INFILE" |
wenzelm@26215 | 70 |
ML_OPTIONS="-r $ML_OPTIONS" |
wenzelm@26215 | 71 |
elif [ "$INFILE" -ef "$OUTFILE" ]; then |
wenzelm@26215 | 72 |
DB="$INFILE" |
wenzelm@26215 | 73 |
elif [ -n "$COPYDB" ]; then |
wenzelm@26215 | 74 |
[ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } |
wenzelm@26215 | 75 |
cp "$INFILE" "$OUTFILE" || fail_out |
wenzelm@26215 | 76 |
chmod +w "$OUTFILE" || fail_out |
wenzelm@26215 | 77 |
DB="$OUTFILE" |
wenzelm@26215 | 78 |
else |
wenzelm@26215 | 79 |
[ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } |
wenzelm@26215 | 80 |
echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE" |
wenzelm@26215 | 81 |
[ -f "$OUTFILE" ] || fail_out |
wenzelm@26215 | 82 |
DB="$OUTFILE" |
wenzelm@26215 | 83 |
fi |
wenzelm@26215 | 84 |
|
wenzelm@26215 | 85 |
|
wenzelm@26215 | 86 |
## run it! |
wenzelm@26215 | 87 |
|
wenzelm@26215 | 88 |
if [ -z "$TERMINATE" ]; then |
wenzelm@26215 | 89 |
FEEDER_OPTS="" |
wenzelm@26215 | 90 |
else |
wenzelm@26215 | 91 |
FEEDER_OPTS="-q" |
wenzelm@26215 | 92 |
fi |
wenzelm@26215 | 93 |
|
wenzelm@26215 | 94 |
DB_INFO="$(ls -l "$DB" 2>/dev/null)" |
wenzelm@26215 | 95 |
|
wenzelm@26215 | 96 |
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | { |
wenzelm@26215 | 97 |
read FPID; "$POLY" $ML_OPTIONS "$DB"; |
wenzelm@26215 | 98 |
RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
wenzelm@26215 | 99 |
RC="$?" |
wenzelm@26215 | 100 |
|
wenzelm@26215 | 101 |
NEW_DB_INFO="$(ls -l "$DB" 2>/dev/null)" |
wenzelm@26215 | 102 |
[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \ |
wenzelm@26215 | 103 |
"$POLY" $DISCGARB_OPTIONS "$OUTFILE" |
wenzelm@26215 | 104 |
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
wenzelm@26215 | 105 |
|
wenzelm@26215 | 106 |
exit "$RC" |