lib/scripts/run-polyml-4.1.3
author wenzelm
Sat Dec 20 11:55:34 2008 +0100 (2008-12-20)
changeset 29145 b1c6f4563df7
parent 26215 94d32a7cd0fb
permissions -rwxr-xr-x
removed Ids;
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"