# HG changeset patch
# User wenzelm
# Date 1638268267 -3600
# Node ID d54b3c96ee50e24f4b7339a294f51d0548eddf0d
# Parent  c5ce1e2f26ab0c52ec06177eb325397848d81b34
more robust physical timeout (despite 1bea05713dde), especially relevant for quickcheck where large unary numerals may cause excessive heap allocations and resulting GC is better included in the timing;

diff -r c5ce1e2f26ab -r d54b3c96ee50 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Fri Nov 26 16:25:58 2021 +0100
+++ b/src/HOL/Tools/try0.ML	Tue Nov 30 11:31:07 2021 +0100
@@ -24,7 +24,7 @@
 fun can_apply timeout_opt pre post tac st =
   let val {goal, ...} = Proof.goal st in
     (case (case timeout_opt of
-            SOME timeout => Timeout.apply timeout
+            SOME timeout => Timeout.apply_physical timeout
           | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
       SOME (x, _) => Thm.nprems_of (post x) < Thm.nprems_of goal
     | NONE => false)
diff -r c5ce1e2f26ab -r d54b3c96ee50 src/Pure/Concurrent/timeout.ML
--- a/src/Pure/Concurrent/timeout.ML	Fri Nov 26 16:25:58 2021 +0100
+++ b/src/Pure/Concurrent/timeout.ML	Tue Nov 30 11:31:07 2021 +0100
@@ -14,6 +14,7 @@
   val scale_time: Time.time -> Time.time
   val end_time: Time.time -> Time.time
   val apply: Time.time -> ('a -> 'b) -> 'a -> 'b
+  val apply_physical: Time.time -> ('a -> 'b) -> 'a -> 'b
   val print: Time.time -> string
 end;
 
@@ -29,7 +30,7 @@
 
 fun end_time timeout = Time.now () + scale_time timeout;
 
-fun apply timeout f x =
+fun apply' {physical, timeout} f x =
   if ignored timeout then f x
   else
     Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts =>
@@ -38,7 +39,7 @@
         val start = Time.now ();
 
         val request =
-          Event_Timer.request {physical = false} (start + scale_time timeout)
+          Event_Timer.request {physical = physical} (start + scale_time timeout)
             (fn () => Isabelle_Thread.interrupt_unsynchronized self);
         val result =
           Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) ();
@@ -52,6 +53,9 @@
         else (Exn.release test; Exn.release result)
       end);
 
+fun apply timeout f x = apply' {physical = false, timeout = timeout} f x;
+fun apply_physical timeout f x = apply' {physical = true, timeout = timeout} f x;
+
 fun print t = "Timeout after " ^ Value.print_time t ^ "s";
 
 end;
diff -r c5ce1e2f26ab -r d54b3c96ee50 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Fri Nov 26 16:25:58 2021 +0100
+++ b/src/Tools/quickcheck.ML	Tue Nov 30 11:31:07 2021 +0100
@@ -281,7 +281,7 @@
 
 fun limit timeout (limit_time, is_interactive) f exc () =
   if limit_time then
-    Timeout.apply timeout f ()
+    Timeout.apply_physical timeout f ()
       handle timeout_exn as Timeout.TIMEOUT _ =>
         if is_interactive then exc () else Exn.reraise timeout_exn
   else f ();
diff -r c5ce1e2f26ab -r d54b3c96ee50 src/Tools/try.ML
--- a/src/Tools/try.ML	Fri Nov 26 16:25:58 2021 +0100
+++ b/src/Tools/try.ML	Tue Nov 30 11:31:07 2021 +0100
@@ -89,7 +89,7 @@
               val auto_time_limit = Options.default_real \<^system_option>\<open>auto_time_limit\<close>
             in
               if auto_time_limit > 0.0 then
-                (case Timeout.apply (seconds auto_time_limit) (fn () => body true state) () of
+                (case Timeout.apply_physical (seconds auto_time_limit) (fn () => body true state) () of
                   (true, (_, outcome)) => List.app Output.information outcome
                 | _ => ())
               else ()