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