# HG changeset patch # User wenzelm # Date 1697101005 -7200 # Node ID a3dcae9a2ebe3ce3dddc5643364f2b48dfd1c037 # Parent b7157c13785566b634c93420d335250ae2e2fc42 distinguish proper interrupts from Poly/ML RTS breakdown; diff -r b7157c137855 -r a3dcae9a2ebe NEWS --- a/NEWS Wed Oct 11 14:03:16 2023 +0200 +++ b/NEWS Thu Oct 12 10:56:45 2023 +0200 @@ -33,6 +33,12 @@ INCOMPATIBILITY, better use \<^try>\...\ with 'catch' or 'finally', or as last resort declare [[ML_catch_all]] within the theory context. +* Proper interrupts (e.g. timeouts) are now distinguished from Poly/ML +runtime system breakdown, using Exn.Interrupt_Breakdown as quasi-error. +Exn.is_interrupt covers all kinds of interrupts as before, but +Exn.is_interrupt_proper and Exn.is_interrupt_breakdown are more +specific. Subtle INCOMPATIBILITY in the semantics of ML evaluation. + *** HOL *** diff -r b7157c137855 -r a3dcae9a2ebe src/Pure/Concurrent/isabelle_thread.ML --- a/src/Pure/Concurrent/isabelle_thread.ML Wed Oct 11 14:03:16 2023 +0200 +++ b/src/Pure/Concurrent/isabelle_thread.ML Thu Oct 12 10:56:45 2023 +0200 @@ -42,7 +42,7 @@ (* abstract type *) -abstype T = T of {thread: Thread.Thread.thread, name: string, id: int} +abstype T = T of {thread: Thread.Thread.thread, name: string, id: int, break: bool Synchronized.var} with val make = T; fun dest (T args) = args; @@ -69,7 +69,8 @@ fun init_self name = let - val t = make {thread = Thread.Thread.self (), name = name, id = make_id ()}; + val break = Synchronized.var "Isabelle_Thread.break" false; + val t = make {thread = Thread.Thread.self (), name = name, id = make_id (), break = break}; in Thread_Data.put self_var (SOME t); t end; fun self () = @@ -136,13 +137,25 @@ (* interrupts *) -val interrupt = Thread.Thread.Interrupt; +val interrupt = Exn.Interrupt_Break; val interrupt_exn = Exn.Exn interrupt; fun interrupt_self () = raise interrupt; fun interrupt_other t = - Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => (); + Synchronized.change (#break (dest t)) + (fn b => (Thread.Thread.interrupt (get_thread t); true) handle Thread.Thread _ => b); + +fun check_interrupt exn = + if Exn.is_interrupt_raw exn then + let + val t = self (); + val break = Synchronized.change_result (#break (dest t)) (fn b => (b, false)); + in if break then Exn.Interrupt_Break else Exn.Interrupt_Breakdown end + else exn; + +fun check_interrupt_exn result = + Exn.map_exn check_interrupt result; structure Exn: EXN = struct @@ -157,7 +170,7 @@ fun main () = (Thread_Attributes.set_attributes Thread_Attributes.test_interrupts; Thread.Thread.testInterrupt ()); - val test = Exn.capture_body main; + val test = check_interrupt_exn (Exn.capture_body main); val _ = Thread_Attributes.set_attributes orig_atts; in test end; @@ -165,11 +178,12 @@ fun try_catch e f = Thread_Attributes.uninterruptible_body (fn run => - run e () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else f exn); + run e () handle exn => + if Exn.is_interrupt exn then Exn.reraise (check_interrupt exn) else f exn); fun try_finally e f = Thread_Attributes.uninterruptible_body (fn run => - Exn.release (Exn.capture_body (run e) before f ())); + Exn.release (check_interrupt_exn (Exn.capture_body (run e)) before f ())); fun try e = Basics.try e (); fun can e = Basics.can e (); diff -r b7157c137855 -r a3dcae9a2ebe src/Pure/Concurrent/par_exn.ML --- a/src/Pure/Concurrent/par_exn.ML Wed Oct 11 14:03:16 2023 +0200 +++ b/src/Pure/Concurrent/par_exn.ML Thu Oct 12 10:56:45 2023 +0200 @@ -21,10 +21,10 @@ exception Par_Exn of exn list; (*non-empty list with unique identified elements sorted by Exn_Properties.ord; - no occurrences of Par_Exn or Exn.is_interrupt*) + no occurrences of Par_Exn or Exn.is_interrupt_proper*) fun par_exns (Par_Exn exns) = exns - | par_exns exn = if Exn.is_interrupt exn then [] else [Exn_Properties.identify [] exn]; + | par_exns exn = if Exn.is_interrupt_proper exn then [] else [Exn_Properties.identify [] exn]; fun make exns = let @@ -33,14 +33,14 @@ in if null exns' then Isabelle_Thread.interrupt else Par_Exn exns' end; fun dest (Par_Exn exns) = SOME exns - | dest exn = if Exn.is_interrupt exn then SOME [] else NONE; + | dest exn = if Exn.is_interrupt_proper exn then SOME [] else NONE; (* parallel results *) fun is_interrupted results = exists Exn.is_exn results andalso - Exn.is_interrupt (make (map_filter Exn.get_exn results)); + Exn.is_interrupt_proper (make (map_filter Exn.get_exn results)); fun release_all results = if forall Exn.is_res results @@ -49,7 +49,7 @@ fun plain_exn (Exn.Res _) = NONE | plain_exn (Exn.Exn (Par_Exn _)) = NONE - | plain_exn (Exn.Exn exn) = if Exn.is_interrupt exn then NONE else SOME exn; + | plain_exn (Exn.Exn exn) = if Exn.is_interrupt_proper exn then NONE else SOME exn; fun release_first results = (case get_first plain_exn results of diff -r b7157c137855 -r a3dcae9a2ebe src/Pure/General/exn.ML --- a/src/Pure/General/exn.ML Wed Oct 11 14:03:16 2023 +0200 +++ b/src/Pure/General/exn.ML Thu Oct 12 10:56:45 2023 +0200 @@ -27,7 +27,14 @@ val maps_res: ('a -> 'b result) -> 'a result -> 'b result val map_exn: (exn -> exn) -> 'a result -> 'a result val cause: exn -> exn + exception Interrupt_Break + exception Interrupt_Breakdown + val is_interrupt_raw: exn -> bool + val is_interrupt_break: exn -> bool + val is_interrupt_breakdown: exn -> bool + val is_interrupt_proper: exn -> bool val is_interrupt: exn -> bool + val is_interrupt_proper_exn: 'a result -> bool val is_interrupt_exn: 'a result -> bool val result: ('a -> 'b) -> 'a -> 'b result val failure_rc: exn -> int @@ -100,10 +107,17 @@ fun cause (IO.Io {cause = exn, ...}) = cause exn | cause exn = exn; -fun is_interrupt exn = - (case cause exn of - Thread.Thread.Interrupt => true - | _ => false); +exception Interrupt_Break; +exception Interrupt_Breakdown; + +fun is_interrupt_raw exn = (case cause exn of Thread.Thread.Interrupt => true | _ => false); +fun is_interrupt_break exn = (case cause exn of Interrupt_Break => true | _ => false); +fun is_interrupt_breakdown exn = (case cause exn of Interrupt_Breakdown => true | _ => false); +fun is_interrupt_proper exn = is_interrupt_raw exn orelse is_interrupt_break exn; +fun is_interrupt exn = is_interrupt_proper exn orelse is_interrupt_breakdown exn; + +fun is_interrupt_proper_exn (Exn exn) = is_interrupt_proper exn + | is_interrupt_proper_exn _ = false; fun is_interrupt_exn (Exn exn) = is_interrupt exn | is_interrupt_exn _ = false; diff -r b7157c137855 -r a3dcae9a2ebe src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Wed Oct 11 14:03:16 2023 +0200 +++ b/src/Pure/Isar/toplevel.ML Thu Oct 12 10:56:45 2023 +0200 @@ -662,7 +662,7 @@ (case transition int tr st of (st', NONE) => st' | (_, SOME (exn, info)) => - if Exn.is_interrupt exn then Exn.reraise exn + if Exn.is_interrupt_proper exn then Exn.reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)); val command = command_exception false; diff -r b7157c137855 -r a3dcae9a2ebe src/Pure/ML/exn_properties.ML --- a/src/Pure/ML/exn_properties.ML Wed Oct 11 14:03:16 2023 +0200 +++ b/src/Pure/ML/exn_properties.ML Thu Oct 12 10:56:45 2023 +0200 @@ -72,7 +72,7 @@ (* identification via serial numbers *) fun identify default_props exn = - if Exn.is_interrupt exn then exn + if Exn.is_interrupt_proper exn then exn else let val props = get exn; diff -r b7157c137855 -r a3dcae9a2ebe src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Wed Oct 11 14:03:16 2023 +0200 +++ b/src/Pure/proofterm.ML Thu Oct 12 10:56:45 2023 +0200 @@ -2245,9 +2245,8 @@ (case Exn.capture_body export_body of Exn.Res res => res | Exn.Exn exn => - if Exn.is_interrupt exn then - raise Fail ("Interrupt: potential resource problems while exporting proof " ^ - string_of_int i) + if Exn.is_interrupt_breakdown exn then + raise Fail ("Resource problems while exporting proof " ^ string_of_int i) else Exn.reraise exn)) else no_export;