lib/scripts/run-polyml
author wenzelm
Fri Jan 01 16:40:47 2016 +0100 (2016-01-01)
changeset 62028 2ecee4679f99
parent 59344 e0ce214303c1
child 62461 075ef5ec115c
permissions -rwxr-xr-x
updated for release;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Makarius
     4 #
     5 # Startup script for Poly/ML 5.1 ... 5.5.
     6 
     7 export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
     8 
     9 
    10 ## diagnostics
    11 
    12 function fail()
    13 {
    14   echo "$1" >&2
    15   exit 2
    16 }
    17 
    18 function fail_out()
    19 {
    20   fail "Unable to create output heap file: \"$OUTFILE\""
    21 }
    22 
    23 function check_file()
    24 {
    25   [ ! -f "$1" ] && fail "Unable to locate \"$1\""
    26 }
    27 
    28 
    29 ## compiler executables and libraries
    30 
    31 [ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
    32 
    33 POLY="$ML_HOME/poly"
    34 check_file "$POLY"
    35 
    36 librarypath "$ML_HOME"
    37 
    38 
    39 
    40 ## prepare databases
    41 
    42 if [ -z "$INFILE" ]; then
    43   INIT=""
    44   EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
    45 else
    46   check_file "$INFILE"
    47   INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
    48   EXIT=""
    49 fi
    50 
    51 if [ -z "$OUTFILE" ]; then
    52   MLEXIT=""
    53 else
    54   if [ -z "$INFILE" ]; then
    55     MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
    56   else
    57     MLEXIT="Session.save \"$OUTFILE\";"
    58   fi
    59   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    60 fi
    61 
    62 
    63 ## run it!
    64 
    65 MLTEXT="$INIT $EXIT $MLTEXT"
    66 
    67 if [ -z "$TERMINATE" ]; then
    68   FEEDER_OPTS=""
    69 else
    70   FEEDER_OPTS="-q"
    71 fi
    72 
    73 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    74   { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
    75 RC="$?"
    76 
    77 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    78 
    79 exit "$RC"
    80 
    81 #:wrap=soft:maxLineLen=100: