--- a/Admin/isatest/settings/at-poly Tue Feb 08 16:10:10 2011 +0100
+++ b/Admin/isatest/settings/at-poly Tue Feb 08 17:38:43 2011 +0100
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.2"
- ML_SYSTEM="polyml-5.2"
+ POLYML_HOME="/home/polyml/polyml-5.3.0"
+ ML_SYSTEM="polyml-5.3.0"
ML_PLATFORM="x86-linux"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 500"
--- a/NEWS Tue Feb 08 16:10:10 2011 +0100
+++ b/NEWS Tue Feb 08 17:38:43 2011 +0100
@@ -10,6 +10,9 @@
Goal.parallel_proofs_threshold (default 100). See also isabelle
usedir option -Q.
+* Discontinued support for Poly/ML 5.2, which was the last version
+without proper multithreading and TimeLimit implementation.
+
*** HOL ***
--- a/src/Pure/Concurrent/future.ML Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/Concurrent/future.ML Tue Feb 08 17:38:43 2011 +0100
@@ -182,7 +182,8 @@
if ok then
Exn.capture (fn () =>
Multithreading.with_attributes Multithreading.private_interrupts
- (fn _ => Position.setmp_thread_data pos e ())) ()
+ (fn _ =>
+ Position.setmp_thread_data pos e () before Multithreading.interrupted ())) ()
else Exn.interrupt_exn;
in assign_result group result res end;
in (result, job) end;
--- a/src/Pure/Concurrent/time_limit.ML Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/Concurrent/time_limit.ML Tue Feb 08 17:38:43 2011 +0100
@@ -2,6 +2,13 @@
Author: Makarius
Execution with time limit.
+
+Notes:
+
+ * There is considerable overhead due to fork of watchdog thread.
+
+ * In rare situations asynchronous interrupts might be mistaken as
+ timeout event, and turned into exception TimeOut accidentally.
*)
signature TIME_LIMIT =
@@ -15,18 +22,29 @@
exception TimeOut;
-fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
- let
- val worker = Thread.self ();
- val timeout = Unsynchronized.ref false;
- val watchdog = Thread.fork (fn () =>
- (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
+val wait_time = seconds 0.0001;
+
+fun timeLimit time f x =
+ Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
+ let
+ val main = Thread.self ();
+ val timeout = Unsynchronized.ref false;
+ val watchdog = Simple_Thread.fork true (fn () =>
+ (OS.Process.sleep time; timeout := true; Thread.interrupt main));
- val result = Exn.capture (restore_attributes f) x;
- val was_timeout = Exn.is_interrupt_exn result andalso ! timeout;
+ val result =
+ Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
+
+ val _ = Thread.interrupt watchdog handle Thread _ => ();
+ val _ = while Thread.isActive watchdog do OS.Process.sleep wait_time;
- val _ = Thread.interrupt watchdog handle Thread _ => ();
- in if was_timeout then raise TimeOut else Exn.release result end) ();
+ val test = Exn.capture Multithreading.interrupted ();
+ in
+ if ! timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
+ then raise TimeOut
+ else if Exn.is_interrupt_exn test then Exn.interrupt ()
+ else Exn.release result
+ end);
end;
--- a/src/Pure/Concurrent/time_limit_dummy.ML Tue Feb 08 16:10:10 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* Title: Pure/Concurrent/time_limit_dummy.ML
- Author: Makarius
-
-Execution with time limit -- dummy version.
-*)
-
-structure TimeLimit: TIME_LIMIT =
-struct
-
-exception TimeOut;
-
-fun timeLimit _ f x = (warning "No timeout support on this ML platform"; f x);
-
-end;
-
--- a/src/Pure/IsaMakefile Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/IsaMakefile Tue Feb 08 17:38:43 2011 +0100
@@ -30,7 +30,6 @@
ML-Systems/multithreading_polyml.ML \
ML-Systems/overloading_smlnj.ML \
ML-Systems/polyml-5.2.1.ML \
- ML-Systems/polyml-5.2.ML \
ML-Systems/polyml.ML \
ML-Systems/polyml_common.ML \
ML-Systems/pp_dummy.ML \
@@ -69,7 +68,6 @@
Concurrent/synchronized_sequential.ML \
Concurrent/task_queue.ML \
Concurrent/time_limit.ML \
- Concurrent/time_limit_dummy.ML \
General/alist.ML \
General/antiquote.ML \
General/balanced_tree.ML \
--- a/src/Pure/Isar/runtime.ML Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/Isar/runtime.ML Tue Feb 08 17:38:43 2011 +0100
@@ -106,10 +106,8 @@
| exn as EXCURSION_FAIL _ => Exn.Exn exn))
else f x;
-fun controlled_execution f =
- f
- |> debugging
- |> Future.interruptible_task;
+fun controlled_execution f x =
+ ((f |> debugging |> Future.interruptible_task) x before Multithreading.interrupted ());
fun toplevel_error output_exn f x = f x
handle exn =>
--- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML Tue Feb 08 17:38:43 2011 +0100
@@ -1,6 +1,6 @@
(* Title: Pure/ML-Systems/compiler_polyml-5.2.ML
-Runtime compilation for Poly/ML 5.2 and 5.2.1.
+Runtime compilation for Poly/ML 5.2.x.
*)
local
--- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Tue Feb 08 17:38:43 2011 +0100
@@ -1,6 +1,6 @@
(* Title: Pure/ML-Systems/compiler_polyml-5.3.ML
-Runtime compilation for Poly/ML 5.3 and 5.4.
+Runtime compilation for Poly/ML 5.3.0 and 5.4.0.
*)
local
--- a/src/Pure/ML-Systems/multithreading.ML Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML Tue Feb 08 17:38:43 2011 +0100
@@ -21,6 +21,7 @@
val public_interrupts: Thread.threadAttribute list
val private_interrupts: Thread.threadAttribute list
val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
+ val interrupted: unit -> unit (*exception Interrupt*)
val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
val sync_wait: Thread.threadAttribute list option -> Time.time option ->
ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
@@ -50,6 +51,8 @@
val private_interrupts = [];
fun sync_interrupts _ = [];
+fun interrupted () = ();
+
fun with_attributes _ e = e [];
fun sync_wait _ _ _ _ = Exn.Result true;
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Tue Feb 08 17:38:43 2011 +0100
@@ -45,6 +45,9 @@
val no_interrupts =
[Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
+val test_interrupts =
+ [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
+
val public_interrupts =
[Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
@@ -61,6 +64,14 @@
Thread.InterruptState Thread.InterruptAsynchOnce
| x => x);
+fun interrupted () =
+ let
+ val orig_atts = safe_interrupts (Thread.getAttributes ());
+ val _ = Thread.setAttributes test_interrupts;
+ val test = Exn.capture Thread.testInterrupt ();
+ val _ = Thread.setAttributes orig_atts;
+ in Exn.release test end;
+
fun with_attributes new_atts e =
let
val orig_atts = safe_interrupts (Thread.getAttributes ());
--- a/src/Pure/ML-Systems/polyml-5.2.ML Tue Feb 08 16:10:10 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(* Title: Pure/ML-Systems/polyml-5.2.ML
-
-Compatibility wrapper for Poly/ML 5.2.
-*)
-
-open Thread;
-
-structure ML_Name_Space =
-struct
- open PolyML.NameSpace;
- type T = PolyML.NameSpace.nameSpace;
- val global = PolyML.globalNameSpace;
-end;
-
-fun reraise exn = raise exn;
-
-use "ML-Systems/polyml_common.ML";
-use "ML-Systems/thread_dummy.ML";
-use "ML-Systems/multithreading.ML";
-use "ML-Systems/unsynchronized.ML";
-
-val _ = PolyML.Compiler.forgetValue "ref";
-val _ = PolyML.Compiler.forgetType "ref";
-
-val pointer_eq = PolyML.pointerEq;
-
-fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-
-use "ML-Systems/compiler_polyml-5.2.ML";
-use "ML-Systems/pp_polyml.ML";
-use "ML-Systems/pp_dummy.ML";
-
--- a/src/Pure/ML-Systems/polyml_common.ML Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML Tue Feb 08 17:38:43 2011 +0100
@@ -73,36 +73,6 @@
-(** interrupts **)
-
-local
-
-val sig_int = 2;
-val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
-
-val _ = Signal.signal (sig_int, default_handler);
-val _ = PolyML.onEntry (fn () => (Signal.signal (sig_int, default_handler); ()));
-
-fun change_signal new_handler f x =
- let
- (*RACE wrt. other signals!*)
- val old_handler = Signal.signal (sig_int, new_handler);
- val result = Exn.capture (f old_handler) x;
- val _ = Signal.signal (sig_int, old_handler);
- in Exn.release result end;
-
-in
-
-fun interruptible f = change_signal default_handler (fn _ => f);
-
-fun uninterruptible f =
- change_signal Signal.SIG_IGN
- (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
-
-end;
-
-
-
(** OS related **)
(* current directory *)
--- a/src/Pure/ROOT.ML Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/ROOT.ML Tue Feb 08 17:38:43 2011 +0100
@@ -72,9 +72,8 @@
if Multithreading.available then ()
else use "Concurrent/synchronized_sequential.ML";
-use "Concurrent/time_limit.ML";
-if Multithreading.available then ()
-else use "Concurrent/time_limit_dummy.ML";
+if String.isPrefix "smlnj" ml_system then ()
+else use "Concurrent/time_limit.ML";
if Multithreading.available
then use "Concurrent/bash.ML"
@@ -193,8 +192,7 @@
use "ML/ml_env.ML";
use "Isar/runtime.ML";
use "ML/ml_compiler.ML";
-if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" orelse
- String.isPrefix "smlnj" ml_system then ()
+if ml_system = "polyml-5.2.1" orelse String.isPrefix "smlnj" ml_system then ()
else use "ML/ml_compiler_polyml-5.3.ML";
use "ML/ml_context.ML";
--- a/src/Pure/pure_setup.ML Tue Feb 08 16:10:10 2011 +0100
+++ b/src/Pure/pure_setup.ML Tue Feb 08 17:38:43 2011 +0100
@@ -36,7 +36,7 @@
toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
-if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1"
+if ml_system = "polyml-5.2.1"
then use "ML/install_pp_polyml.ML"
else if String.isPrefix "polyml" ml_system
then use "ML/install_pp_polyml-5.3.ML"