lib/scripts/run-polyml-5.5.1
author wenzelm
Fri Jan 01 16:40:47 2016 +0100 (2016-01-01)
changeset 62028 2ecee4679f99
parent 59344 e0ce214303c1
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@52832
     6
# Startup script for Poly/ML 5.5.1.
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@52832
    43
if [ -z "$INFILE" ]; then
wenzelm@52832
    44
  INIT=""
wenzelm@56627
    45
  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
wenzelm@52832
    46
else
wenzelm@52832
    47
  check_file "$INFILE"
wenzelm@52832
    48
  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));"
wenzelm@52832
    49
  EXIT=""
wenzelm@52832
    50
fi
wenzelm@52832
    51
wenzelm@52832
    52
if [ -z "$OUTFILE" ]; then
wenzelm@52832
    53
  MLEXIT=""
wenzelm@52832
    54
else
wenzelm@53657
    55
  if [ -z "$INFILE" ]; then
wenzelm@59344
    56
    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);"
wenzelm@53657
    57
  else
wenzelm@59344
    58
    MLEXIT="Session.save \"$OUTFILE\";"
wenzelm@53657
    59
  fi
wenzelm@52832
    60
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
wenzelm@52832
    61
fi
wenzelm@52832
    62
wenzelm@52832
    63
wenzelm@52832
    64
## run it!
wenzelm@52832
    65
wenzelm@59344
    66
MLTEXT="$INIT $EXIT $MLTEXT"
wenzelm@52832
    67
wenzelm@52832
    68
if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
wenzelm@52835
    69
  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
wenzelm@52835
    70
    --error-exit </dev/null
wenzelm@52832
    71
  RC="$?"
wenzelm@52832
    72
else
wenzelm@52832
    73
  if [ -z "$TERMINATE" ]; then
wenzelm@52832
    74
    FEEDER_OPTS=""
wenzelm@52832
    75
  else
wenzelm@52832
    76
    FEEDER_OPTS="-q"
wenzelm@52833
    77
    ML_OPTIONS="$ML_OPTIONS --error-exit"
wenzelm@52832
    78
  fi
wenzelm@52832
    79
  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
wenzelm@52832
    80
    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
wenzelm@52832
    81
  RC="$?"
wenzelm@52832
    82
fi
wenzelm@52832
    83
wenzelm@52832
    84
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
wenzelm@52832
    85
wenzelm@52832
    86
exit "$RC"
wenzelm@52832
    87
wenzelm@52832
    88
#:wrap=soft:maxLineLen=100: