lib/scripts/run-polyml-5.5.1
author wenzelm
Thu, 01 Aug 2013 22:05:49 +0200
changeset 52833 21843a4c6ba9
parent 52832 980ca3d6ded4
child 52835 0906c00bb21d
permissions -rwxr-xr-x
clarified options;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52832
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
     2
# :mode=shellscript:
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
     3
#
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
     4
# Author: Makarius
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
     5
#
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
     6
# Startup script for Poly/ML 5.5.1.
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
     7
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
     8
export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
     9
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    10
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    11
## diagnostics
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    12
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    13
function fail()
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    14
{
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    15
  echo "$1" >&2
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    16
  exit 2
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    17
}
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    18
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    19
function fail_out()
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    20
{
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    21
  fail "Unable to create output heap file: \"$OUTFILE\""
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    22
}
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    23
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    24
function check_file()
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    25
{
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    26
  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    27
}
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    28
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    29
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    30
## compiler executables and libraries
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    31
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    32
[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    33
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    34
POLY="$ML_HOME/poly"
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    35
check_file "$POLY"
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    36
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    37
librarypath "$ML_HOME"
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    38
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    39
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    40
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    41
## prepare databases
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    42
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    43
if [ -z "$INFILE" ]; then
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    44
  INIT=""
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    45
  EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);"
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    46
else
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    47
  check_file "$INFILE"
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    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));"
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    49
  EXIT=""
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    50
fi
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    51
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    52
if [ -z "$OUTFILE" ]; then
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    53
  COMMIT='fun commit () = false;'
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    54
  MLEXIT=""
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    55
else
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    56
  COMMIT="fun commit () = (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);"
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    57
  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    58
  MLEXIT="commit();"
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    59
fi
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    60
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    61
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    62
## run it!
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    63
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    64
MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    65
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    66
if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    67
  "$POLY" -q -i $ML_OPTIONS --eval "$MLTEXT" --error-exit </dev/null
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    68
  RC="$?"
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    69
else
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    70
  if [ -z "$TERMINATE" ]; then
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    71
    FEEDER_OPTS=""
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    72
  else
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    73
    FEEDER_OPTS="-q"
52833
21843a4c6ba9 clarified options;
wenzelm
parents: 52832
diff changeset
    74
    ML_OPTIONS="$ML_OPTIONS --error-exit"
52832
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    75
  fi
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    76
  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    77
    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    78
  RC="$?"
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    79
fi
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    80
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    81
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    82
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    83
exit "$RC"
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    84
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    85
#:wrap=soft:maxLineLen=100: