author | wenzelm |
Sat, 20 Dec 2008 11:55:34 +0100 | |
changeset 29145 | b1c6f4563df7 |
parent 26375 | 234f10289d97 |
child 31315 | 3c7b40548a84 |
permissions | -rwxr-xr-x |
wenzelm@21653 | 1 |
#!/usr/bin/env bash |
wenzelm@21653 | 2 |
# |
wenzelm@21653 | 3 |
# Author: Makarius |
wenzelm@21653 | 4 |
# |
wenzelm@26213 | 5 |
# Poly/ML 5.0 startup script. |
wenzelm@21653 | 6 |
|
wenzelm@21653 | 7 |
export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE |
wenzelm@21653 | 8 |
|
wenzelm@21653 | 9 |
|
wenzelm@21653 | 10 |
## diagnostics |
wenzelm@21653 | 11 |
|
wenzelm@21653 | 12 |
function fail_out() |
wenzelm@21653 | 13 |
{ |
wenzelm@21653 | 14 |
echo "Unable to create output heap file: \"$OUTFILE\"" >&2 |
wenzelm@21653 | 15 |
exit 2 |
wenzelm@21653 | 16 |
} |
wenzelm@21653 | 17 |
|
wenzelm@21653 | 18 |
function check_file() |
wenzelm@21653 | 19 |
{ |
wenzelm@21653 | 20 |
if [ ! -f "$1" ]; then |
wenzelm@21653 | 21 |
echo "Unable to locate $1" >&2 |
wenzelm@21653 | 22 |
echo "Please check your ML system settings!" >&2 |
wenzelm@21653 | 23 |
exit 2 |
wenzelm@21653 | 24 |
fi |
wenzelm@21653 | 25 |
} |
wenzelm@21653 | 26 |
|
wenzelm@21653 | 27 |
|
wenzelm@21653 | 28 |
## compiler executables and libraries |
wenzelm@21653 | 29 |
|
wenzelm@21653 | 30 |
POLY="$ML_HOME/poly" |
wenzelm@21653 | 31 |
check_file "$POLY" |
wenzelm@21653 | 32 |
|
wenzelm@21653 | 33 |
if [ "$(basename "$ML_HOME")" = bin ]; then |
wenzelm@21653 | 34 |
POLYLIB="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib; pwd)" |
wenzelm@21653 | 35 |
else |
wenzelm@21653 | 36 |
POLYLIB="$ML_HOME" |
wenzelm@21653 | 37 |
fi |
wenzelm@21653 | 38 |
|
wenzelm@21653 | 39 |
export LD_LIBRARY_PATH="$POLYLIB:$LD_LIBRARY_PATH" |
wenzelm@21653 | 40 |
export DYLD_LIBRARY_PATH="$POLYLIB:$DYLD_LIBRARY_PATH" |
wenzelm@21653 | 41 |
|
wenzelm@21653 | 42 |
|
wenzelm@21653 | 43 |
## prepare databases |
wenzelm@21653 | 44 |
|
wenzelm@21653 | 45 |
if [ -z "$INFILE" ]; then |
wenzelm@21713 | 46 |
PRG="$POLY" |
wenzelm@21653 | 47 |
EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" |
wenzelm@21653 | 48 |
else |
wenzelm@21653 | 49 |
check_file "$INFILE" |
wenzelm@21713 | 50 |
PRG="$INFILE" |
wenzelm@21653 | 51 |
EXIT="" |
wenzelm@21653 | 52 |
fi |
wenzelm@21653 | 53 |
|
wenzelm@21653 | 54 |
if [ -z "$OUTFILE" ]; then |
wenzelm@21653 | 55 |
COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' |
wenzelm@21653 | 56 |
else |
wenzelm@21653 | 57 |
if [ -z "$COMPRESS" ]; then |
wenzelm@24296 | 58 |
COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" |
wenzelm@21653 | 59 |
else |
wenzelm@24296 | 60 |
COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" |
wenzelm@21653 | 61 |
fi |
wenzelm@21653 | 62 |
[ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
wenzelm@21653 | 63 |
rm -f "${OUTFILE}.o" || fail_out |
wenzelm@21653 | 64 |
fi |
wenzelm@21653 | 65 |
|
wenzelm@21653 | 66 |
|
wenzelm@21653 | 67 |
## run it! |
wenzelm@21653 | 68 |
|
wenzelm@25124 | 69 |
MLTEXT="$EXIT $COMMIT $MLTEXT" |
wenzelm@21653 | 70 |
MLEXIT="commit();" |
wenzelm@21653 | 71 |
|
wenzelm@21653 | 72 |
if [ -z "$TERMINATE" ]; then |
wenzelm@21653 | 73 |
FEEDER_OPTS="" |
wenzelm@21653 | 74 |
else |
wenzelm@21653 | 75 |
FEEDER_OPTS="-q" |
wenzelm@21653 | 76 |
fi |
wenzelm@21653 | 77 |
|
wenzelm@26375 | 78 |
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
wenzelm@26375 | 79 |
{ read FPID; "$PRG" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
wenzelm@21653 | 80 |
RC="$?" |
wenzelm@21653 | 81 |
|
wenzelm@21653 | 82 |
if [ -n "$OUTFILE" ]; then |
wenzelm@21653 | 83 |
if [ -e "${OUTFILE}.o" ]; then |
wenzelm@24480 | 84 |
cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml $POLY_LINK_OPTIONS || fail_out |
wenzelm@21653 | 85 |
rm -f "${OUTFILE}.o" |
wenzelm@21711 | 86 |
[ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE" |
wenzelm@21653 | 87 |
fi |
wenzelm@21653 | 88 |
[ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
wenzelm@21653 | 89 |
fi |
wenzelm@21653 | 90 |
|
wenzelm@21653 | 91 |
exit "$RC" |