lib/scripts/run-polyml-5.6
author wenzelm
Fri Jan 01 16:40:47 2016 +0100 (2016-01-01)
changeset 62028 2ecee4679f99
parent 61715 5dc95d957569
child 62386 10e55e168672
permissions -rwxr-xr-x
updated for release;
     1 #!/usr/bin/env bash
     2 # :mode=shellscript:
     3 #
     4 # Author: Makarius
     5 #
     6 # Startup script for Poly/ML 5.6.
     7 
     8 export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
     9 
    10 
    11 ## diagnostics
    12 
    13 function fail()
    14 {
    15   echo "$1" >&2
    16   exit 2
    17 }
    18 
    19 function fail_out()
    20 {
    21   fail "Unable to create output heap file: \"$OUTFILE\""
    22 }
    23 
    24 function check_file()
    25 {
    26   [ ! -f "$1" ] && fail "Unable to locate \"$1\""
    27 }
    28 
    29 
    30 ## compiler executables and libraries
    31 
    32 [ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
    33 
    34 POLY="$ML_HOME/poly"
    35 check_file "$POLY"
    36 
    37 librarypath "$ML_HOME"
    38 
    39 
    40 
    41 ## prepare databases
    42 
    43 case "$ML_PLATFORM" in
    44   *-windows)
    45     PLATFORM_INFILE="$(platform_path -m "$INFILE")"
    46     PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")"
    47     ;;
    48   *)
    49     PLATFORM_INFILE="$INFILE"
    50     PLATFORM_OUTFILE="$OUTFILE"
    51     ;;
    52 esac
    53 
    54 if [ -z "$INFILE" ]; then
    55   INIT=""
    56   case "$ML_PLATFORM" in
    57     *-windows)
    58       EXIT="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc));"
    59       ;;
    60     *)
    61       EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
    62       ;;
    63   esac
    64 else
    65   check_file "$INFILE"
    66   INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));"
    67   EXIT=""
    68 fi
    69 
    70 if [ -z "$OUTFILE" ]; then
    71   MLEXIT=""
    72 else
    73   if [ -z "$INFILE" ]; then
    74     MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$PLATFORM_OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); OS.Process.exit OS.Process.success);"
    75   else
    76     MLEXIT="Session.save \"$OUTFILE\";"
    77   fi
    78   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    79 fi
    80 
    81 
    82 ## run it!
    83 
    84 MLTEXT="$INIT $EXIT $MLTEXT"
    85 
    86 if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
    87   "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
    88     --error-exit </dev/null
    89   RC="$?"
    90 else
    91   if [ -z "$TERMINATE" ]; then
    92     FEEDER_OPTS=""
    93   else
    94     FEEDER_OPTS="-q"
    95     ML_OPTIONS="$ML_OPTIONS --error-exit"
    96   fi
    97   "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    98     { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
    99   RC="$?"
   100 fi
   101 
   102 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
   103 
   104 exit "$RC"
   105 
   106 #:wrap=soft:maxLineLen=100: