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 +if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1"
11.21 +then use "ML/install_pp_polyml.ML"
11.22 +else if String.isPrefix "polyml" ml_system
11.23 then use "ML/install_pp_polyml-5.3.ML"
11.24 -else if String.isPrefix "polyml" ml_system
11.25 -then use "ML/install_pp_polyml.ML"
11.26 -else ();
11.27 -
11.28 -if ml_system = "polyml-5.0" orelse ml_system = "polyml-5.1" then
11.29 - Secure.use_text ML_Parse.global_context (0, "") false
11.30 - "PolyML.Compiler.maxInlineSize := 20"
11.31 else ();
11.32
11.33