lib/scripts/run-polyml
author wenzelm
Fri Sep 01 17:54:58 2000 +0200 (2000-09-01)
changeset 9789 7e5e6c47c0b5
parent 9765 46def28153d6
child 9977 32955afeb835
permissions -rwxr-xr-x
GPLed;
more robust handling of spaces in args / file names;
wenzelm@3007
     1
#!/bin/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@2301
     8
#
wenzelm@8360
     9
# Global vars: INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
wenzelm@2301
    10
# and from settings
wenzelm@2301
    11
wenzelm@2301
    12
wenzelm@2301
    13
## diagnostics
wenzelm@2301
    14
wenzelm@2349
    15
function fail_out()
wenzelm@2301
    16
{
wenzelm@2349
    17
  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
wenzelm@2301
    18
  exit 2
wenzelm@2301
    19
}
wenzelm@2301
    20
wenzelm@5063
    21
function check_mlhome_file()
wenzelm@5063
    22
{
wenzelm@5063
    23
  if [ ! -f "$1" ]; then
wenzelm@5063
    24
    echo "Unable to locate $1" >&2
wenzelm@5063
    25
    echo "Please check your ML_HOME setting!" >&2
wenzelm@5063
    26
    exit 2
wenzelm@5063
    27
  fi
wenzelm@5063
    28
}
wenzelm@5063
    29
wenzelm@2301
    30
wenzelm@2400
    31
## Poly/ML programs
wenzelm@2301
    32
wenzelm@9789
    33
POLY="$ML_HOME/poly"
wenzelm@9789
    34
DISCGARB="$ML_HOME/discgarb"
wenzelm@2301
    35
wenzelm@5063
    36
check_mlhome_file "$POLY"
wenzelm@5063
    37
check_mlhome_file "$DISCGARB"
wenzelm@5063
    38
wenzelm@2301
    39
wenzelm@9765
    40
case "$ML_SYSTEM" in
wenzelm@9765
    41
  polyml-4.*)
wenzelm@9765
    42
    EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
wenzelm@9765
    43
    ;;
wenzelm@9765
    44
  *)
wenzelm@9765
    45
    EXIT="val exit = PolyML.exit;"
wenzelm@9765
    46
    ;;
wenzelm@9765
    47
esac
wenzelm@9765
    48
wenzelm@9765
    49
wenzelm@2301
    50
## prepare databases
wenzelm@2301
    51
wenzelm@3055
    52
COPYDB=true
wenzelm@2349
    53
wenzelm@2301
    54
if [ -z "$INFILE" ]; then
wenzelm@2400
    55
  INFILE="$ML_HOME/ML_dbase"
wenzelm@5063
    56
  check_mlhome_file "$INFILE"
wenzelm@3055
    57
  COPYDB=""
wenzelm@9765
    58
  MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
wenzelm@2301
    59
fi
wenzelm@2301
    60
wenzelm@2301
    61
if [ -z "$OUTFILE" ]; then
wenzelm@2301
    62
  DB="$INFILE"
wenzelm@2349
    63
  ML_OPTIONS="-r $ML_OPTIONS"  
wenzelm@2349
    64
elif [ "$INFILE" -ef "$OUTFILE" ]; then
wenzelm@2301
    65
  DB="$INFILE"
wenzelm@2301
    66
elif [ -n "$COPYDB" ]; then
wenzelm@2936
    67
  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
wenzelm@2548
    68
  cp "$INFILE" "$OUTFILE" || fail_out
wenzelm@2349
    69
  chmod +w "$OUTFILE" || fail_out
wenzelm@2301
    70
  DB="$OUTFILE"
wenzelm@2301
    71
else
wenzelm@2936
    72
  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
wenzelm@9789
    73
  echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
wenzelm@2301
    74
  [ -f "$OUTFILE" ] || fail_out
wenzelm@2301
    75
  DB="$OUTFILE"
wenzelm@2301
    76
fi
wenzelm@2301
    77
wenzelm@2301
    78
wenzelm@2301
    79
## run it!
wenzelm@2301
    80
wenzelm@4505
    81
if [ -z "$TERMINATE" ]; then
wenzelm@4505
    82
  FEEDER_OPTS="-s"
wenzelm@4505
    83
else
wenzelm@4505
    84
  FEEDER_OPTS="-q"
wenzelm@4505
    85
fi
wenzelm@4505
    86
wenzelm@2400
    87
DB_INFO=$(ls -l "$DB")
wenzelm@2349
    88
wenzelm@9789
    89
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \
wenzelm@9789
    90
  { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
wenzelm@9789
    91
RC="$?"
wenzelm@2301
    92
wenzelm@2400
    93
NEW_DB_INFO=$(ls -l "$DB")
wenzelm@9789
    94
[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && "$DISCGARB" -c "$OUTFILE"
wenzelm@4505
    95
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
wenzelm@2301
    96
wenzelm@9789
    97
exit "$RC"