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