Poly/ML 5.0 setup for Isabelle2005.
authorwenzelm
Thu Dec 07 14:11:39 2006 +0100 (2006-12-07)
changeset 21688e5287f12f1e1
parent 21687 f689f729afab
child 21689 58abd6d8abd1
Poly/ML 5.0 setup for Isabelle2005.
Admin/Isabelle2005-polyml-5.0/README-polyml-5.0
Admin/Isabelle2005-polyml-5.0/lib/scripts/run-polyml-5.0
Admin/Isabelle2005-polyml-5.0/src/Pure/ML-Systems/polyml-5.0.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/Admin/Isabelle2005-polyml-5.0/README-polyml-5.0	Thu Dec 07 14:11:39 2006 +0100
     1.3 @@ -0,0 +1,23 @@
     1.4 +
     1.5 +Using Isabelle2005 with Poly/ML 5.0 requires the following
     1.6 +compatibility wrappers:
     1.7 +
     1.8 +  Isabelle2005/src/Pure/ML-Systems/polyml-5.0.ML
     1.9 +  Isabelle2005/lib/scripts/run-polyml-5.0
    1.10 +
    1.11 +Moreover the Isabelle settings need to specify that version, by
    1.12 +including something like this in Isabelle2005/etc/settings or
    1.13 +~/isabelle/etc/settings:
    1.14 +
    1.15 +ML_PLATFORM=""
    1.16 +ML_HOME=/usr/local/bin
    1.17 +ML_SYSTEM=polyml-5.0
    1.18 +ML_OPTIONS="-H 500"
    1.19 +
    1.20 +Then logics can be compiled as usual, cf. the INSTALL instructions.
    1.21 +
    1.22 +
    1.23 +	Makarius
    1.24 +	07-Dec-2006
    1.25 +
    1.26 +$Id$
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/Admin/Isabelle2005-polyml-5.0/lib/scripts/run-polyml-5.0	Thu Dec 07 14:11:39 2006 +0100
     2.3 @@ -0,0 +1,90 @@
     2.4 +#!/usr/bin/env bash
     2.5 +#
     2.6 +# $Id$
     2.7 +# Author: Makarius
     2.8 +#
     2.9 +# Poly/ML startup script (for 5.0)
    2.10 +
    2.11 +export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
    2.12 +
    2.13 +
    2.14 +## diagnostics
    2.15 +
    2.16 +function fail_out()
    2.17 +{
    2.18 +  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
    2.19 +  exit 2
    2.20 +}
    2.21 +
    2.22 +function check_file()
    2.23 +{
    2.24 +  if [ ! -f "$1" ]; then
    2.25 +    echo "Unable to locate $1" >&2
    2.26 +    echo "Please check your ML system settings!" >&2
    2.27 +    exit 2
    2.28 +  fi
    2.29 +}
    2.30 +
    2.31 +
    2.32 +## compiler executables and libraries
    2.33 +
    2.34 +POLY="$ML_HOME/poly"
    2.35 +check_file "$POLY"
    2.36 +
    2.37 +if [ "$(basename "$ML_HOME")" = bin ]; then
    2.38 +  POLYLIB="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib; pwd)"
    2.39 +else
    2.40 +  POLYLIB="$ML_HOME"
    2.41 +fi
    2.42 +
    2.43 +export LD_LIBRARY_PATH="$POLYLIB:$LD_LIBRARY_PATH"
    2.44 +export DYLD_LIBRARY_PATH="$POLYLIB:$DYLD_LIBRARY_PATH"
    2.45 +
    2.46 +
    2.47 +## prepare databases
    2.48 +
    2.49 +if [ -z "$INFILE" ]; then
    2.50 +  EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
    2.51 +else
    2.52 +  check_file "$INFILE"
    2.53 +  POLY="$INFILE"
    2.54 +  EXIT=""
    2.55 +fi
    2.56 +
    2.57 +if [ -z "$OUTFILE" ]; then
    2.58 +  COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
    2.59 +else
    2.60 +  if [ -z "$COMPRESS" ]; then
    2.61 +    COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
    2.62 +  else
    2.63 +    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
    2.64 +  fi
    2.65 +  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    2.66 +  rm -f "${OUTFILE}.o" || fail_out
    2.67 +fi
    2.68 +
    2.69 +
    2.70 +## run it!
    2.71 +
    2.72 +MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $EXIT $COMMIT $MLTEXT"
    2.73 +MLEXIT="commit();"
    2.74 +
    2.75 +if [ -z "$TERMINATE" ]; then
    2.76 +  FEEDER_OPTS=""
    2.77 +else
    2.78 +  FEEDER_OPTS="-q"
    2.79 +fi
    2.80 +
    2.81 +"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    2.82 +  { read FPID; "$POLY" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    2.83 +RC="$?"
    2.84 +
    2.85 +if [ -n "$OUTFILE" ]; then
    2.86 +  if [ -e "${OUTFILE}.o" ]; then
    2.87 +    cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml -lstdc++ || fail_out
    2.88 +    rm -f "${OUTFILE}.o"
    2.89 +  fi
    2.90 +  [ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    2.91 +fi
    2.92 +
    2.93 +exit "$RC"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/Admin/Isabelle2005-polyml-5.0/src/Pure/ML-Systems/polyml-5.0.ML	Thu Dec 07 14:11:39 2006 +0100
     3.3 @@ -0,0 +1,33 @@
     3.4 +(*  Title:      Pure/ML-Systems/polyml-5.0.ML
     3.5 +    ID:         $Id$
     3.6 +
     3.7 +Compatibility wrapper for Poly/ML 5.0 -- version for Isabelle2005.
     3.8 +*)
     3.9 +
    3.10 +structure Posix =
    3.11 +struct
    3.12 +  open Posix;
    3.13 +  structure IO =
    3.14 +  struct
    3.15 +    open IO;
    3.16 +    val mkReader = mkTextReader;
    3.17 +    val mkWriter = mkTextWriter;
    3.18 +  end;
    3.19 +end;
    3.20 +
    3.21 +structure TextIO =
    3.22 +struct
    3.23 +  open TextIO;
    3.24 +  fun inputLine is = Option.getOpt (TextIO.inputLine is, "");
    3.25 +end;
    3.26 +
    3.27 +structure Substring =
    3.28 +struct
    3.29 +  open Substring;
    3.30 +  val all = full;
    3.31 +end;
    3.32 +
    3.33 +
    3.34 +use "ML-Systems/polyml.ML";
    3.35 +
    3.36 +val pointer_eq = PolyML.pointerEq;