lib/scripts/run-polyml-4.1.3
changeset 26215 94d32a7cd0fb
child 29145 b1c6f4563df7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/scripts/run-polyml-4.1.3	Thu Mar 06 19:21:26 2008 +0100
     1.3 @@ -0,0 +1,107 @@
     1.4 +#!/usr/bin/env bash
     1.5 +#
     1.6 +# $Id$
     1.7 +# Author: Markus Wenzel, TU Muenchen
     1.8 +#
     1.9 +# Poly/ML 4.x startup script.
    1.10 +
    1.11 +export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
    1.12 +
    1.13 +
    1.14 +## diagnostics
    1.15 +
    1.16 +function fail_out()
    1.17 +{
    1.18 +  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
    1.19 +  exit 2
    1.20 +}
    1.21 +
    1.22 +function check_file()
    1.23 +{
    1.24 +  if [ ! -f "$1" ]; then
    1.25 +    echo "Unable to locate $1" >&2
    1.26 +    echo "Please check your ML system settings!" >&2
    1.27 +    exit 2
    1.28 +  fi
    1.29 +}
    1.30 +
    1.31 +
    1.32 +## Poly/ML executable and database
    1.33 +
    1.34 +ML_DBASE_PREFIX=""
    1.35 +
    1.36 +POLY="$ML_HOME/poly"
    1.37 +check_file "$POLY"
    1.38 +
    1.39 +if [ -z "$ML_DBASE" ]; then
    1.40 +  if [ ! -e "$ML_HOME/ML_dbase" -a "$(basename "$ML_HOME")" = bin ]; then
    1.41 +    ML_DBASE_HOME="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib/poly; pwd)"
    1.42 +  else
    1.43 +    ML_DBASE_HOME="$ML_HOME"
    1.44 +  fi
    1.45 +  if [ -z "$COPYDB" ]; then
    1.46 +    ML_DBASE_PREFIX="$ML_DBASE_HOME/"
    1.47 +    ML_DBASE="ML_dbase"
    1.48 +  else
    1.49 +    ML_DBASE="$ML_DBASE_HOME/ML_dbase"
    1.50 +  fi
    1.51 +  export POLYPATH="$ML_DBASE_HOME"
    1.52 +else
    1.53 +  export POLYPATH="$(dirname "$ML_DBASE")"
    1.54 +fi
    1.55 +
    1.56 +DISCGARB_OPTIONS="-d -c"
    1.57 +
    1.58 +EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
    1.59 +
    1.60 +
    1.61 +## prepare databases
    1.62 +
    1.63 +if [ -z "$INFILE" ]; then
    1.64 +  check_file "$ML_DBASE_PREFIX$ML_DBASE"
    1.65 +  INFILE="$ML_DBASE"
    1.66 +  MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
    1.67 +  DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max"
    1.68 +else
    1.69 +  COPYDB=true
    1.70 +fi
    1.71 +
    1.72 +if [ -z "$OUTFILE" ]; then
    1.73 +  DB="$INFILE"
    1.74 +  ML_OPTIONS="-r $ML_OPTIONS"
    1.75 +elif [ "$INFILE" -ef "$OUTFILE" ]; then
    1.76 +  DB="$INFILE"
    1.77 +elif [ -n "$COPYDB" ]; then
    1.78 +  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
    1.79 +  cp "$INFILE" "$OUTFILE" || fail_out
    1.80 +  chmod +w "$OUTFILE" || fail_out
    1.81 +  DB="$OUTFILE"
    1.82 +else
    1.83 +  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
    1.84 +  echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
    1.85 +  [ -f "$OUTFILE" ] || fail_out
    1.86 +  DB="$OUTFILE"
    1.87 +fi
    1.88 +
    1.89 +
    1.90 +## run it!
    1.91 +
    1.92 +if [ -z "$TERMINATE" ]; then
    1.93 +  FEEDER_OPTS=""
    1.94 +else
    1.95 +  FEEDER_OPTS="-q"
    1.96 +fi
    1.97 +
    1.98 +DB_INFO="$(ls -l "$DB" 2>/dev/null)"
    1.99 +
   1.100 +"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | {
   1.101 +  read FPID; "$POLY" $ML_OPTIONS "$DB";
   1.102 +  RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
   1.103 +RC="$?"
   1.104 +
   1.105 +NEW_DB_INFO="$(ls -l "$DB" 2>/dev/null)"
   1.106 +[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \
   1.107 +  "$POLY" $DISCGARB_OPTIONS "$OUTFILE"
   1.108 +[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
   1.109 +
   1.110 +exit "$RC"