discontinued support for Poly/ML 5.0 and 5.1 versions;
authorwenzelm
Tue Aug 17 18:41:55 2010 +0200 (2010-08-17)
changeset 38470484e483eb606
parent 38469 5c6c5d63f3c3
child 38471 0924654b8163
discontinued support for Poly/ML 5.0 and 5.1 versions;
NEWS
README
lib/scripts/run-polyml-5.0
src/Pure/IsaMakefile
src/Pure/ML-Systems/compiler_polyml-5.0.ML
src/Pure/ML-Systems/compiler_polyml-5.3.ML
src/Pure/ML-Systems/polyml-5.0.ML
src/Pure/ML-Systems/polyml-5.1.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ROOT.ML
src/Pure/pure_setup.ML
     1.1 --- a/NEWS	Tue Aug 17 18:04:08 2010 +0200
     1.2 +++ b/NEWS	Tue Aug 17 18:41:55 2010 +0200
     1.3 @@ -139,6 +139,11 @@
     1.4  change in semantics.
     1.5  
     1.6  
     1.7 +*** System ***
     1.8 +
     1.9 +* Discontinued support for Poly/ML 5.0 and 5.1 versions.
    1.10 +
    1.11 +
    1.12  
    1.13  New in Isabelle2009-2 (June 2010)
    1.14  ---------------------------------
     2.1 --- a/README	Tue Aug 17 18:04:08 2010 +0200
     2.2 +++ b/README	Tue Aug 17 18:41:55 2010 +0200
     2.3 @@ -13,7 +13,7 @@
     2.4     Windows with Cygwin, Mac OS) and depends on the following main
     2.5     add-on tools:
     2.6  
     2.7 -     * The Poly/ML compiler and runtime system (version 5.x).
     2.8 +     * The Poly/ML compiler and runtime system (version 5.2.1 or later).
     2.9       * The GNU bash shell (version 3.x or 2.x).
    2.10       * Perl (version 5.x).
    2.11       * GNU Emacs (version 22) -- for the Proof General interface.
     3.1 --- a/lib/scripts/run-polyml-5.0	Tue Aug 17 18:04:08 2010 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,87 +0,0 @@
     3.4 -#!/usr/bin/env bash
     3.5 -#
     3.6 -# Author: Makarius
     3.7 -#
     3.8 -# Poly/ML 5.0 startup script.
     3.9 -
    3.10 -export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
    3.11 -
    3.12 -
    3.13 -## diagnostics
    3.14 -
    3.15 -function fail_out()
    3.16 -{
    3.17 -  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
    3.18 -  exit 2
    3.19 -}
    3.20 -
    3.21 -function check_file()
    3.22 -{
    3.23 -  if [ ! -f "$1" ]; then
    3.24 -    echo "Unable to locate $1" >&2
    3.25 -    echo "Please check your ML system settings!" >&2
    3.26 -    exit 2
    3.27 -  fi
    3.28 -}
    3.29 -
    3.30 -
    3.31 -## compiler executables and libraries
    3.32 -
    3.33 -POLY="$ML_HOME/poly"
    3.34 -check_file "$POLY"
    3.35 -
    3.36 -if [ "$(basename "$ML_HOME")" = bin ]; then
    3.37 -  POLYLIB="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib; pwd)"
    3.38 -else
    3.39 -  POLYLIB="$ML_HOME"
    3.40 -fi
    3.41 -
    3.42 -export LD_LIBRARY_PATH="$POLYLIB:$LD_LIBRARY_PATH"
    3.43 -export DYLD_LIBRARY_PATH="$POLYLIB:$DYLD_LIBRARY_PATH"
    3.44 -
    3.45 -
    3.46 -## prepare databases
    3.47 -
    3.48 -if [ -z "$INFILE" ]; then
    3.49 -  PRG="$POLY"
    3.50 -  EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
    3.51 -else
    3.52 -  check_file "$INFILE"
    3.53 -  PRG="$INFILE"
    3.54 -  EXIT=""
    3.55 -fi
    3.56 -
    3.57 -if [ -z "$OUTFILE" ]; then
    3.58 -  COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
    3.59 -else
    3.60 -  COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
    3.61 -  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    3.62 -  rm -f "${OUTFILE}.o" || fail_out
    3.63 -fi
    3.64 -
    3.65 -
    3.66 -## run it!
    3.67 -
    3.68 -MLTEXT="$EXIT $COMMIT $MLTEXT"
    3.69 -MLEXIT="commit();"
    3.70 -
    3.71 -if [ -z "$TERMINATE" ]; then
    3.72 -  FEEDER_OPTS=""
    3.73 -else
    3.74 -  FEEDER_OPTS="-q"
    3.75 -fi
    3.76 -
    3.77 -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    3.78 -  { read FPID; "$PRG" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    3.79 -RC="$?"
    3.80 -
    3.81 -if [ -n "$OUTFILE" ]; then
    3.82 -  if [ -e "${OUTFILE}.o" ]; then
    3.83 -    cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml $POLY_LINK_OPTIONS || fail_out
    3.84 -    rm -f "${OUTFILE}.o"
    3.85 -    [ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE"
    3.86 -  fi
    3.87 -  [ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    3.88 -fi
    3.89 -
    3.90 -exit "$RC"
     4.1 --- a/src/Pure/IsaMakefile	Tue Aug 17 18:04:08 2010 +0200
     4.2 +++ b/src/Pure/IsaMakefile	Tue Aug 17 18:41:55 2010 +0200
     4.3 @@ -21,7 +21,6 @@
     4.4  
     4.5  BOOTSTRAP_FILES = 					\
     4.6    ML-Systems/bash.ML 					\
     4.7 -  ML-Systems/compiler_polyml-5.0.ML			\
     4.8    ML-Systems/compiler_polyml-5.2.ML			\
     4.9    ML-Systems/compiler_polyml-5.3.ML			\
    4.10    ML-Systems/ml_name_space.ML				\
    4.11 @@ -29,8 +28,6 @@
    4.12    ML-Systems/multithreading.ML				\
    4.13    ML-Systems/multithreading_polyml.ML			\
    4.14    ML-Systems/overloading_smlnj.ML			\
    4.15 -  ML-Systems/polyml-5.0.ML				\
    4.16 -  ML-Systems/polyml-5.1.ML				\
    4.17    ML-Systems/polyml-5.2.1.ML				\
    4.18    ML-Systems/polyml-5.2.ML				\
    4.19    ML-Systems/polyml.ML					\
     5.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Tue Aug 17 18:04:08 2010 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,32 +0,0 @@
     5.4 -(*  Title:      Pure/ML-Systems/compiler_polyml-5.0.ML
     5.5 -
     5.6 -Runtime compilation for Poly/ML 5.0 and 5.1.
     5.7 -*)
     5.8 -
     5.9 -fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
    5.10 -  let
    5.11 -    val in_buffer = Unsynchronized.ref (explode (tune_source txt));
    5.12 -    val out_buffer = Unsynchronized.ref ([]: string list);
    5.13 -    fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    5.14 -
    5.15 -    val current_line = Unsynchronized.ref line;
    5.16 -    fun get () =
    5.17 -      (case ! in_buffer of
    5.18 -        [] => ""
    5.19 -      | c :: cs => (in_buffer := cs; if c = "\n" then current_line := ! current_line + 1 else (); c));
    5.20 -    fun put s = out_buffer := s :: ! out_buffer;
    5.21 -
    5.22 -    fun exec () =
    5.23 -      (case ! in_buffer of
    5.24 -        [] => ()
    5.25 -      | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
    5.26 -  in
    5.27 -    exec () handle exn => (error (output ()); reraise exn);
    5.28 -    if verbose then print (output ()) else ()
    5.29 -  end;
    5.30 -
    5.31 -fun use_file context verbose name =
    5.32 -  let
    5.33 -    val instream = TextIO.openIn name;
    5.34 -    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    5.35 -  in use_text context (1, name) verbose txt end;
     6.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Tue Aug 17 18:04:08 2010 +0200
     6.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Tue Aug 17 18:41:55 2010 +0200
     6.3 @@ -1,6 +1,6 @@
     6.4  (*  Title:      Pure/ML-Systems/compiler_polyml-5.3.ML
     6.5  
     6.6 -Runtime compilation for Poly/ML 5.3.0.
     6.7 +Runtime compilation for Poly/ML 5.3 and 5.4.
     6.8  *)
     6.9  
    6.10  local
     7.1 --- a/src/Pure/ML-Systems/polyml-5.0.ML	Tue Aug 17 18:04:08 2010 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,19 +0,0 @@
     7.4 -(*  Title:      Pure/ML-Systems/polyml-5.0.ML
     7.5 -
     7.6 -Compatibility wrapper for Poly/ML 5.0.
     7.7 -*)
     7.8 -
     7.9 -fun reraise exn = raise exn;
    7.10 -
    7.11 -use "ML-Systems/unsynchronized.ML";
    7.12 -use "ML-Systems/universal.ML";
    7.13 -use "ML-Systems/thread_dummy.ML";
    7.14 -use "ML-Systems/ml_name_space.ML";
    7.15 -use "ML-Systems/polyml_common.ML";
    7.16 -use "ML-Systems/compiler_polyml-5.0.ML";
    7.17 -use "ML-Systems/pp_polyml.ML";
    7.18 -
    7.19 -val pointer_eq = PolyML.pointerEq;
    7.20 -
    7.21 -fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
    7.22 -
     8.1 --- a/src/Pure/ML-Systems/polyml-5.1.ML	Tue Aug 17 18:04:08 2010 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,18 +0,0 @@
     8.4 -(*  Title:      Pure/ML-Systems/polyml-5.1.ML
     8.5 -
     8.6 -Compatibility wrapper for Poly/ML 5.1.
     8.7 -*)
     8.8 -
     8.9 -fun reraise exn = raise exn;
    8.10 -
    8.11 -use "ML-Systems/unsynchronized.ML";
    8.12 -use "ML-Systems/thread_dummy.ML";
    8.13 -use "ML-Systems/ml_name_space.ML";
    8.14 -use "ML-Systems/polyml_common.ML";
    8.15 -use "ML-Systems/compiler_polyml-5.0.ML";
    8.16 -use "ML-Systems/pp_polyml.ML";
    8.17 -
    8.18 -val pointer_eq = PolyML.pointerEq;
    8.19 -
    8.20 -fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
    8.21 -
     9.1 --- a/src/Pure/ML-Systems/polyml.ML	Tue Aug 17 18:04:08 2010 +0200
     9.2 +++ b/src/Pure/ML-Systems/polyml.ML	Tue Aug 17 18:41:55 2010 +0200
     9.3 @@ -1,6 +1,6 @@
     9.4  (*  Title:      Pure/ML-Systems/polyml.ML
     9.5  
     9.6 -Compatibility wrapper for Poly/ML 5.3.0.
     9.7 +Compatibility wrapper for Poly/ML 5.3 and 5.4.
     9.8  *)
     9.9  
    9.10  use "ML-Systems/unsynchronized.ML";
    10.1 --- a/src/Pure/ROOT.ML	Tue Aug 17 18:04:08 2010 +0200
    10.2 +++ b/src/Pure/ROOT.ML	Tue Aug 17 18:41:55 2010 +0200
    10.3 @@ -179,9 +179,9 @@
    10.4  use "ML/ml_syntax.ML";
    10.5  use "ML/ml_env.ML";
    10.6  use "Isar/runtime.ML";
    10.7 -if ml_system = "polyml-5.3.0"
    10.8 -then use "ML/ml_compiler_polyml-5.3.ML"
    10.9 -else use "ML/ml_compiler.ML";
   10.10 +if member (op =) ["polyml-5.2", "polyml-5.2.1", "smlnj-110"] ml_system
   10.11 +then use "ML/ml_compiler.ML"
   10.12 +else use "ML/ml_compiler_polyml-5.3.ML";
   10.13  use "ML/ml_context.ML";
   10.14  
   10.15  (*theory sources*)
    11.1 --- a/src/Pure/pure_setup.ML	Tue Aug 17 18:04:08 2010 +0200
    11.2 +++ b/src/Pure/pure_setup.ML	Tue Aug 17 18:41:55 2010 +0200
    11.3 @@ -18,8 +18,9 @@
    11.4  
    11.5  (* ML toplevel pretty printing *)
    11.6  
    11.7 -if String.isPrefix "smlnj" ml_system then ()
    11.8 -else toplevel_pp ["String", "string"] "ML_Syntax.pretty_string";
    11.9 +if String.isPrefix "polyml" ml_system
   11.10 +then toplevel_pp ["String", "string"] "ML_Syntax.pretty_string"
   11.11 +else ();
   11.12  
   11.13  toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
   11.14  toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
   11.15 @@ -39,15 +40,10 @@
   11.16  toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
   11.17  toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
   11.18  
   11.19 -if ml_system = "polyml-5.3.0"
   11.20 -then use "ML/install_pp_polyml-5.3.ML"
   11.21 -else if String.isPrefix "polyml" ml_system
   11.22 +if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1"
   11.23  then use "ML/install_pp_polyml.ML"
   11.24 -else ();
   11.25 -
   11.26 -if ml_system = "polyml-5.0" orelse ml_system = "polyml-5.1" then
   11.27 -  Secure.use_text ML_Parse.global_context (0, "") false
   11.28 -    "PolyML.Compiler.maxInlineSize := 20"
   11.29 +else if String.isPrefix "polyml" ml_system
   11.30 +then use "ML/install_pp_polyml-5.3.ML"
   11.31  else ();
   11.32  
   11.33