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;
wenzelm@52832
     1
#!/usr/bin/env bash
wenzelm@52832
     2
# :mode=shellscript:
wenzelm@52832
     3
#
wenzelm@52832
     4
# Author: Makarius
wenzelm@52832
     5
#
wenzelm@61715
     6
# Startup script for Poly/ML 5.6.
wenzelm@52832
     7
wenzelm@52832
     8
export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
wenzelm@52832
     9
wenzelm@52832
    10
wenzelm@52832
    11
## diagnostics
wenzelm@52832
    12
wenzelm@52832
    13
function fail()
wenzelm@52832
    14
{
wenzelm@52832
    15
  echo "$1" >&2
wenzelm@52832
    16
  exit 2
wenzelm@52832
    17
}
wenzelm@52832
    18
wenzelm@52832
    19
function fail_out()
wenzelm@52832
    20
{
wenzelm@52832
    21
  fail "Unable to create output heap file: \"$OUTFILE\""
wenzelm@52832
    22
}
wenzelm@52832
    23
wenzelm@52832
    24
function check_file()
wenzelm@52832
    25
{
wenzelm@52832
    26
  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
wenzelm@52832
    27
}
wenzelm@52832
    28
wenzelm@52832
    29
wenzelm@52832
    30
## compiler executables and libraries
wenzelm@52832
    31
wenzelm@52832
    32
[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
wenzelm@52832
    33
wenzelm@52832
    34
POLY="$ML_HOME/poly"
wenzelm@52832
    35
check_file "$POLY"
wenzelm@52832
    36
wenzelm@52832
    37
librarypath "$ML_HOME"
wenzelm@52832
    38
wenzelm@52832
    39
wenzelm@52832
    40
wenzelm@52832
    41
## prepare databases
wenzelm@52832
    42
wenzelm@60967
    43
case "$ML_PLATFORM" in
wenzelm@60967
    44
  *-windows)
wenzelm@61294
    45
    PLATFORM_INFILE="$(platform_path -m "$INFILE")"
wenzelm@61294
    46
    PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")"
wenzelm@60967
    47
    ;;
wenzelm@60967
    48
  *)
wenzelm@60967
    49
    PLATFORM_INFILE="$INFILE"
wenzelm@60967
    50
    PLATFORM_OUTFILE="$OUTFILE"
wenzelm@60967
    51
    ;;
wenzelm@60967
    52
esac
wenzelm@60967
    53
wenzelm@52832
    54
if [ -z "$INFILE" ]; then
wenzelm@52832
    55
  INIT=""
wenzelm@60962
    56
  case "$ML_PLATFORM" in
wenzelm@60962
    57
    *-windows)
wenzelm@60962
    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));"
wenzelm@60962
    59
      ;;
wenzelm@60962
    60
    *)
wenzelm@60962
    61
      EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
wenzelm@60962
    62
      ;;
wenzelm@60962
    63
  esac
wenzelm@52832
    64
else
wenzelm@52832
    65
  check_file "$INFILE"
wenzelm@60966
    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));"
wenzelm@52832
    67
  EXIT=""
wenzelm@52832
    68
fi
wenzelm@52832
    69
wenzelm@52832
    70
if [ -z "$OUTFILE" ]; then
wenzelm@52832
    71
  MLEXIT=""
wenzelm@52832
    72
else
wenzelm@53657
    73
  if [ -z "$INFILE" ]; then
wenzelm@60967
    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);"
wenzelm@53657
    75
  else
wenzelm@59344
    76
    MLEXIT="Session.save \"$OUTFILE\";"
wenzelm@53657
    77
  fi
wenzelm@52832
    78
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
wenzelm@52832
    79
fi
wenzelm@52832
    80
wenzelm@52832
    81
wenzelm@52832
    82
## run it!
wenzelm@52832
    83
wenzelm@59344
    84
MLTEXT="$INIT $EXIT $MLTEXT"
wenzelm@52832
    85
wenzelm@52832
    86
if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
wenzelm@52835
    87
  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
wenzelm@52835
    88
    --error-exit </dev/null
wenzelm@52832
    89
  RC="$?"
wenzelm@52832
    90
else
wenzelm@52832
    91
  if [ -z "$TERMINATE" ]; then
wenzelm@52832
    92
    FEEDER_OPTS=""
wenzelm@52832
    93
  else
wenzelm@52832
    94
    FEEDER_OPTS="-q"
wenzelm@52833
    95
    ML_OPTIONS="$ML_OPTIONS --error-exit"
wenzelm@52832
    96
  fi
wenzelm@52832
    97
  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
wenzelm@52832
    98
    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
wenzelm@52832
    99
  RC="$?"
wenzelm@52832
   100
fi
wenzelm@52832
   101
wenzelm@52832
   102
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
wenzelm@52832
   103
wenzelm@52832
   104
exit "$RC"
wenzelm@52832
   105
wenzelm@52832
   106
#:wrap=soft:maxLineLen=100: