lib/scripts/run-polyml-5.5.2
author hoelzl
Wed, 28 Jan 2015 11:17:21 +0100
changeset 59453 4736ff5a41d8
parent 59344 e0ce214303c1
permissions -rwxr-xr-x
moved bcontfun from AFP/Ordinary_Differential_Equations
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
#
54717
42c209a6c225 support for polml-5.5.2;
wenzelm
parents: 53657
diff changeset
     6
# Startup script for Poly/ML 5.5.2.
52832
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=""
56627
cb912b7de3cf more general exit;
wenzelm
parents: 54717
diff changeset
    45
  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
52832
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
  MLEXIT=""
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    54
else
53657
64942a1f7187 prefer high-level ML_System.share_common_data, ML_System.save_state -- except for bootstrap images (RAW, Pure);
wenzelm
parents: 52835
diff changeset
    55
  if [ -z "$INFILE" ]; then
59344
e0ce214303c1 proper Session.save with shutdown, which is relevant to avoid persistent threads;
wenzelm
parents: 56627
diff changeset
    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);"
53657
64942a1f7187 prefer high-level ML_System.share_common_data, ML_System.save_state -- except for bootstrap images (RAW, Pure);
wenzelm
parents: 52835
diff changeset
    57
  else
59344
e0ce214303c1 proper Session.save with shutdown, which is relevant to avoid persistent threads;
wenzelm
parents: 56627
diff changeset
    58
    MLEXIT="Session.save \"$OUTFILE\";"
53657
64942a1f7187 prefer high-level ML_System.share_common_data, ML_System.save_state -- except for bootstrap images (RAW, Pure);
wenzelm
parents: 52835
diff changeset
    59
  fi
52832
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    60
  [ -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
    61
fi
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    62
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
## run it!
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    65
59344
e0ce214303c1 proper Session.save with shutdown, which is relevant to avoid persistent threads;
wenzelm
parents: 56627
diff changeset
    66
MLTEXT="$INIT $EXIT $MLTEXT"
52832
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    67
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    68
if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
52835
0906c00bb21d recode utf8 for ML, as done in feeder.pl;
wenzelm
parents: 52833
diff changeset
    69
  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
0906c00bb21d recode utf8 for ML, as done in feeder.pl;
wenzelm
parents: 52833
diff changeset
    70
    --error-exit </dev/null
52832
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    71
  RC="$?"
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
  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
    74
    FEEDER_OPTS=""
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    75
  else
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    76
    FEEDER_OPTS="-q"
52833
21843a4c6ba9 clarified options;
wenzelm
parents: 52832
diff changeset
    77
    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
    78
  fi
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    79
  "$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
    80
    { 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
    81
  RC="$?"
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    82
fi
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    83
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    84
[ -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
    85
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    86
exit "$RC"
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    87
980ca3d6ded4 specific startup script for Poly/ML 5.5.1, taking advantage of some of its new options;
wenzelm
parents:
diff changeset
    88
#:wrap=soft:maxLineLen=100: