lib/scripts/run-polyml
author wenzelm
Tue Jun 14 22:08:53 2005 +0200 (2005-06-14)
changeset 16392 7212040b71f2
parent 16374 f4b7cf8975af
child 16393 4bc08baa3fbb
permissions -rwxr-xr-x
discontinued polyml-3.x;
made cygwin functionality less intrusive;
more quoting of expressions;
wenzelm@10555
     1
#!/usr/bin/env bash
wenzelm@2301
     2
#
wenzelm@2314
     3
# $Id$
wenzelm@9789
     4
# Author: Markus Wenzel, TU Muenchen
wenzelm@2314
     5
#
wenzelm@2301
     6
# Poly/ML startup script.
wenzelm@9977
     7
wenzelm@10105
     8
export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
wenzelm@2301
     9
wenzelm@2301
    10
wenzelm@2301
    11
## diagnostics
wenzelm@2301
    12
wenzelm@2349
    13
function fail_out()
wenzelm@2301
    14
{
wenzelm@2349
    15
  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
wenzelm@2301
    16
  exit 2
wenzelm@2301
    17
}
wenzelm@2301
    18
wenzelm@10206
    19
function check_file()
wenzelm@5063
    20
{
wenzelm@5063
    21
  if [ ! -f "$1" ]; then
wenzelm@5063
    22
    echo "Unable to locate $1" >&2
wenzelm@10206
    23
    echo "Please check your ML system settings!" >&2
wenzelm@5063
    24
    exit 2
wenzelm@5063
    25
  fi
wenzelm@5063
    26
}
wenzelm@5063
    27
wenzelm@2301
    28
wenzelm@16392
    29
## Poly/ML executable and database
wenzelm@2301
    30
wenzelm@10206
    31
ML_DBASE_PREFIX=""
wenzelm@16374
    32
ML_DBASE_SUFFIX=""
wenzelm@16374
    33
wenzelm@16374
    34
case "$ML_PLATFORM" in
wenzelm@16374
    35
  *-cygwin)
wenzelm@16374
    36
    ML_DBASE_SUFFIX=".pmd"
wenzelm@16374
    37
    POLY="$ML_HOME/PolyML.exe"
wenzelm@16392
    38
    function fixpath () { cygpath -m "$@"; }
wenzelm@16374
    39
    ;;
wenzelm@16374
    40
  *)
wenzelm@16374
    41
    POLY="$ML_HOME/poly"
wenzelm@16392
    42
    function fixpath () { echo -n "$@"; }
wenzelm@16374
    43
    ;;
wenzelm@16374
    44
esac
wenzelm@16374
    45
wenzelm@10206
    46
check_file "$POLY"
wenzelm@2301
    47
wenzelm@16392
    48
if [ -z "$ML_DBASE" ]; then
wenzelm@16392
    49
  if [ -z "$COPYDB" ]; then
wenzelm@16392
    50
    ML_DBASE_PREFIX="$ML_HOME/"
wenzelm@16392
    51
    ML_DBASE="ML_dbase${ML_DBASE_SUFFIX}"
wenzelm@16392
    52
  else
wenzelm@16392
    53
    ML_DBASE="$ML_HOME/ML_dbase${ML_DBASE_SUFFIX}"
wenzelm@16392
    54
  fi
wenzelm@16392
    55
  export POLYPATH="$(fixpath "$ML_HOME")"
wenzelm@16392
    56
else
wenzelm@16392
    57
  export POLYPATH="$(fixpath "$(dirname "$ML_DBASE")")"
wenzelm@16392
    58
fi
wenzelm@10206
    59
wenzelm@16392
    60
DISCGARB="$POLY"
wenzelm@16392
    61
DISCGARB_OPTIONS="-d -c"
wenzelm@10206
    62
wenzelm@16392
    63
EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
wenzelm@9765
    64
wenzelm@9765
    65
wenzelm@2301
    66
## prepare databases
wenzelm@2301
    67
wenzelm@2301
    68
if [ -z "$INFILE" ]; then
wenzelm@10206
    69
  check_file "$ML_DBASE_PREFIX$ML_DBASE"
wenzelm@10206
    70
  INFILE="$ML_DBASE"
wenzelm@9765
    71
  MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
wenzelm@16285
    72
  case "$ML_SYSTEM" in
wenzelm@16285
    73
    polyml-4.1.[12])
wenzelm@16285
    74
      DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180"
wenzelm@16285
    75
      ;;
wenzelm@16285
    76
    polyml-4.1.*)
wenzelm@16285
    77
      DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
wenzelm@16285
    78
      ;;
wenzelm@16285
    79
  esac
wenzelm@10105
    80
else
wenzelm@10105
    81
  COPYDB=true
wenzelm@2301
    82
fi
wenzelm@2301
    83
wenzelm@2301
    84
if [ -z "$OUTFILE" ]; then
wenzelm@2301
    85
  DB="$INFILE"
wenzelm@15850
    86
  ML_OPTIONS="-r $ML_OPTIONS"
wenzelm@2349
    87
elif [ "$INFILE" -ef "$OUTFILE" ]; then
wenzelm@2301
    88
  DB="$INFILE"
wenzelm@2301
    89
elif [ -n "$COPYDB" ]; then
wenzelm@2936
    90
  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
wenzelm@2548
    91
  cp "$INFILE" "$OUTFILE" || fail_out
wenzelm@2349
    92
  chmod +w "$OUTFILE" || fail_out
wenzelm@2301
    93
  DB="$OUTFILE"
wenzelm@2301
    94
else
wenzelm@2936
    95
  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
wenzelm@16392
    96
  echo "PolyML.make_database \"$(fixpath "$OUTFILE")\"; PolyML.quit();" | "$POLY" -r "$(fixpath "$INFILE")"
wenzelm@2301
    97
  [ -f "$OUTFILE" ] || fail_out
wenzelm@2301
    98
  DB="$OUTFILE"
wenzelm@2301
    99
fi
wenzelm@2301
   100
wenzelm@2301
   101
wenzelm@2301
   102
## run it!
wenzelm@2301
   103
wenzelm@16254
   104
if [ -z "$TERMINATE" ]; then
wenzelm@16254
   105
  FEEDER_OPTS=""
wenzelm@16254
   106
else
wenzelm@16254
   107
  FEEDER_OPTS="-q"
wenzelm@16254
   108
fi
wenzelm@16254
   109
wenzelm@16392
   110
DB_INFO="$(ls -l "$DB" 2>/dev/null)"
wenzelm@15850
   111
wenzelm@16392
   112
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | {
wenzelm@16392
   113
  read FPID; "$POLY" $ML_OPTIONS "$(fixpath "$DB")";
wenzelm@16392
   114
  RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
wenzelm@9789
   115
RC="$?"
wenzelm@2301
   116
wenzelm@16392
   117
NEW_DB_INFO="$(ls -l "$DB" 2>/dev/null)"
wenzelm@10206
   118
[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \
wenzelm@10206
   119
  "$DISCGARB" $DISCGARB_OPTIONS "$OUTFILE"
wenzelm@4505
   120
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
wenzelm@2301
   121
wenzelm@9789
   122
exit "$RC"