pro-forma support for polyml-5.5.3 (presently SVN 1960);
authorwenzelm
Mon Sep 29 09:57:34 2014 +0200 (2014-09-29)
changeset 58470890d8286fd4e
parent 58469 66ddc5ad4f63
child 58471 ab4b94892c4c
pro-forma support for polyml-5.5.3 (presently SVN 1960);
lib/scripts/run-polyml-5.5.3
src/Pure/ML-Systems/polyml-5.5.3.ML
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/scripts/run-polyml-5.5.3	Mon Sep 29 09:57:34 2014 +0200
     1.3 @@ -0,0 +1,90 @@
     1.4 +#!/usr/bin/env bash
     1.5 +# :mode=shellscript:
     1.6 +#
     1.7 +# Author: Makarius
     1.8 +#
     1.9 +# Startup script for Poly/ML 5.5.3.
    1.10 +
    1.11 +export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
    1.12 +
    1.13 +
    1.14 +## diagnostics
    1.15 +
    1.16 +function fail()
    1.17 +{
    1.18 +  echo "$1" >&2
    1.19 +  exit 2
    1.20 +}
    1.21 +
    1.22 +function fail_out()
    1.23 +{
    1.24 +  fail "Unable to create output heap file: \"$OUTFILE\""
    1.25 +}
    1.26 +
    1.27 +function check_file()
    1.28 +{
    1.29 +  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
    1.30 +}
    1.31 +
    1.32 +
    1.33 +## compiler executables and libraries
    1.34 +
    1.35 +[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
    1.36 +
    1.37 +POLY="$ML_HOME/poly"
    1.38 +check_file "$POLY"
    1.39 +
    1.40 +librarypath "$ML_HOME"
    1.41 +
    1.42 +
    1.43 +
    1.44 +## prepare databases
    1.45 +
    1.46 +if [ -z "$INFILE" ]; then
    1.47 +  INIT=""
    1.48 +  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
    1.49 +else
    1.50 +  check_file "$INFILE"
    1.51 +  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));"
    1.52 +  EXIT=""
    1.53 +fi
    1.54 +
    1.55 +if [ -z "$OUTFILE" ]; then
    1.56 +  COMMIT='fun commit () = false;'
    1.57 +  MLEXIT=""
    1.58 +else
    1.59 +  if [ -z "$INFILE" ]; then
    1.60 +    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);"
    1.61 +  else
    1.62 +    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
    1.63 +  fi
    1.64 +  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    1.65 +  MLEXIT="commit();"
    1.66 +fi
    1.67 +
    1.68 +
    1.69 +## run it!
    1.70 +
    1.71 +MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
    1.72 +
    1.73 +if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
    1.74 +  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
    1.75 +    --error-exit </dev/null
    1.76 +  RC="$?"
    1.77 +else
    1.78 +  if [ -z "$TERMINATE" ]; then
    1.79 +    FEEDER_OPTS=""
    1.80 +  else
    1.81 +    FEEDER_OPTS="-q"
    1.82 +    ML_OPTIONS="$ML_OPTIONS --error-exit"
    1.83 +  fi
    1.84 +  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    1.85 +    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
    1.86 +  RC="$?"
    1.87 +fi
    1.88 +
    1.89 +[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    1.90 +
    1.91 +exit "$RC"
    1.92 +
    1.93 +#:wrap=soft:maxLineLen=100:
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/ML-Systems/polyml-5.5.3.ML	Mon Sep 29 09:57:34 2014 +0200
     2.3 @@ -0,0 +1,23 @@
     2.4 +(*  Title:      Pure/ML-Systems/polyml-5.5.3.ML
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Compatibility wrapper for Poly/ML 5.5.3.
     2.8 +*)
     2.9 +
    2.10 +structure Thread =
    2.11 +struct
    2.12 +  open Thread;
    2.13 +
    2.14 +  structure Thread =
    2.15 +  struct
    2.16 +    open Thread;
    2.17 +
    2.18 +    fun numProcessors () =
    2.19 +      (case Thread.numPhysicalProcessors () of
    2.20 +        SOME n => n
    2.21 +      | NONE => Thread.numProcessors ());
    2.22 +  end;
    2.23 +end;
    2.24 +
    2.25 +use "ML-Systems/polyml.ML";
    2.26 +
     3.1 --- a/src/Pure/ROOT	Mon Sep 29 08:13:23 2014 +0200
     3.2 +++ b/src/Pure/ROOT	Mon Sep 29 09:57:34 2014 +0200
     3.3 @@ -14,6 +14,7 @@
     3.4      "ML-Systems/overloading_smlnj.ML"
     3.5      "ML-Systems/polyml.ML"
     3.6      "ML-Systems/polyml-5.5.2.ML"
     3.7 +    "ML-Systems/polyml-5.5.3.ML"
     3.8      "ML-Systems/pp_dummy.ML"
     3.9      "ML-Systems/proper_int.ML"
    3.10      "ML-Systems/single_assignment.ML"
    3.11 @@ -39,6 +40,7 @@
    3.12      "ML-Systems/overloading_smlnj.ML"
    3.13      "ML-Systems/polyml.ML"
    3.14      "ML-Systems/polyml-5.5.2.ML"
    3.15 +    "ML-Systems/polyml-5.5.3.ML"
    3.16      "ML-Systems/pp_dummy.ML"
    3.17      "ML-Systems/proper_int.ML"
    3.18      "ML-Systems/single_assignment.ML"
     4.1 --- a/src/Pure/ROOT.ML	Mon Sep 29 08:13:23 2014 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Mon Sep 29 09:57:34 2014 +0200
     4.3 @@ -96,12 +96,14 @@
     4.4  
     4.5  if ML_System.name = "polyml-5.5.1"
     4.6    orelse ML_System.name = "polyml-5.5.2"
     4.7 +  orelse ML_System.name = "polyml-5.5.3"
     4.8  then use "ML/exn_trace_polyml-5.5.1.ML"
     4.9  else ();
    4.10  
    4.11  if ML_System.name = "polyml-5.5.0"
    4.12    orelse ML_System.name = "polyml-5.5.1"
    4.13    orelse ML_System.name = "polyml-5.5.2"
    4.14 +  orelse ML_System.name = "polyml-5.5.3"
    4.15  then use "ML/ml_statistics_polyml-5.5.0.ML"
    4.16  else use "ML/ml_statistics_dummy.ML";
    4.17