# HG changeset patch
# User wenzelm
# Date 1614961789 -3600
# Node ID 3b5196dac4c8d43ee6d76bda045919573110dfca
# Parent 3fb201ca8fb5a051d398a5a2af73d43cf795693d
clarified timeouts in Isabelle/ML;
diff -r 3fb201ca8fb5 -r 3b5196dac4c8 NEWS
--- a/NEWS Fri Mar 05 17:02:32 2021 +0100
+++ b/NEWS Fri Mar 05 17:29:49 2021 +0100
@@ -7,6 +7,16 @@
New in this Isabelle version
----------------------------
+*** General ***
+
+* Timeouts for Isabelle/ML tools are subject to system option
+"timeout_scale" --- this already used for the overall session build
+process before, and allows to adapt to slow machines. The underlying
+Timeout.apply in Isabelle/ML treats an original timeout specification 0
+as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY
+in boundary cases.
+
+
*** HOL ***
* Theory Multiset: dedicated predicate "multiset" is gone, use
diff -r 3fb201ca8fb5 -r 3b5196dac4c8 etc/options
--- a/etc/options Fri Mar 05 17:02:32 2021 +0100
+++ b/etc/options Fri Mar 05 17:29:49 2021 +0100
@@ -66,7 +66,7 @@
-- "additional print modes for prover output (separated by commas)"
-section "Parallel Processing"
+section "Parallel Processing and Timing"
public option threads : int = 0
-- "maximum number of worker threads for prover process (0 = hardware max.)"
@@ -87,6 +87,9 @@
option command_timing_threshold : real = 0.1
-- "default threshold for persistent command timing (seconds)"
+public option timeout_scale : real = 1.0
+ -- "scale factor for timeout in Isabelle/ML and session build"
+
section "Detail of Proof Checking"
@@ -108,9 +111,6 @@
option timeout : real = 0
-- "timeout for session build job (seconds > 0)"
-option timeout_scale : real = 1.0
- -- "scale factor for session timeout"
-
option process_output_limit : int = 100
-- "build process output limit (in million characters, 0 = unlimited)"
diff -r 3fb201ca8fb5 -r 3b5196dac4c8 src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML Fri Mar 05 17:02:32 2021 +0100
+++ b/src/HOL/Library/refute.ML Fri Mar 05 17:29:49 2021 +0100
@@ -993,7 +993,7 @@
else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
fun wrapper () =
let
- val timer = Timer.startRealTimer ()
+ val time_start = Time.now ()
val t =
if no_assms then t
else if negate then Logic.list_implies (assm_ts, t)
@@ -1029,9 +1029,9 @@
else ()
fun find_model_loop universe =
let
- val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer)
- val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime
- orelse raise Timeout.TIMEOUT (Time.fromMilliseconds msecs_spent)
+ val time_spent = Time.now () - time_start
+ val _ = maxtime = 0 orelse time_spent < Timeout.scale_time (Time.fromSeconds maxtime)
+ orelse raise Timeout.TIMEOUT time_spent
val init_model = (universe, [])
val init_args = {maxvars = maxvars, def_eq = false, next_idx = 1,
bounds = [], wellformed = True}
@@ -1114,15 +1114,13 @@
writeln ("Trying to find a model that "
^ (if negate then "refutes" else "satisfies") ^ ": "
^ Syntax.string_of_term ctxt t);
- if maxtime > 0 then (
- Timeout.apply (Time.fromSeconds maxtime)
- wrapper ()
- handle Timeout.TIMEOUT _ =>
- (writeln ("Search terminated, time limit (" ^
- string_of_int maxtime
- ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
- check_expect "unknown")
- ) else wrapper ()
+ Timeout.apply (Time.fromSeconds maxtime)
+ wrapper ()
+ handle Timeout.TIMEOUT _ =>
+ (writeln ("Search terminated, time limit (" ^
+ string_of_int maxtime
+ ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
+ check_expect "unknown")
end;
diff -r 3fb201ca8fb5 -r 3b5196dac4c8 src/HOL/Nitpick_Examples/minipick.ML
--- a/src/HOL/Nitpick_Examples/minipick.ML Fri Mar 05 17:02:32 2021 +0100
+++ b/src/HOL/Nitpick_Examples/minipick.ML Fri Mar 05 17:29:49 2021 +0100
@@ -430,7 +430,7 @@
fun solve_any_kodkod_problem thy problems =
let
val {debug, overlord, timeout, ...} = Nitpick_Commands.default_params thy []
- val deadline = Time.now () + timeout
+ val deadline = Timeout.end_time timeout
val max_threads = 1
val max_solutions = 1
in
diff -r 3fb201ca8fb5 -r 3b5196dac4c8 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Mar 05 17:02:32 2021 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Mar 05 17:29:49 2021 +0100
@@ -947,7 +947,7 @@
in
let
val unknown_outcome = (unknownN, [])
- val deadline = Time.now () + timeout
+ val deadline = Timeout.end_time timeout
val outcome as (outcome_code, _) =
Timeout.apply (timeout + timeout_bonus)
(pick_them_nits_in_term deadline state params mode i n step subst
diff -r 3fb201ca8fb5 -r 3b5196dac4c8 src/HOL/Tools/Nitpick/nitpick_tests.ML
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Fri Mar 05 17:02:32 2021 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Fri Mar 05 17:29:49 2021 +0100
@@ -211,7 +211,7 @@
fun run_all_tests () =
let
val {debug, overlord, timeout, ...} = Nitpick_Commands.default_params \<^theory> []
- val deadline = Time.now () + timeout
+ val deadline = Timeout.end_time timeout
val max_threads = 1
val max_solutions = 1
in
diff -r 3fb201ca8fb5 -r 3b5196dac4c8 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Mar 05 17:02:32 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Mar 05 17:29:49 2021 +0100
@@ -1266,7 +1266,7 @@
let
val hard_timeout = Time.scale learn_timeout_slack timeout
val birth_time = Time.now ()
- val death_time = birth_time + hard_timeout
+ val death_time = birth_time + Timeout.scale_time hard_timeout
val desc = ("Machine learner for Sledgehammer", "")
in
Async_Manager_Legacy.thread MaShN birth_time death_time desc task
diff -r 3fb201ca8fb5 -r 3b5196dac4c8 src/Pure/Concurrent/timeout.ML
--- a/src/Pure/Concurrent/timeout.ML Fri Mar 05 17:02:32 2021 +0100
+++ b/src/Pure/Concurrent/timeout.ML Fri Mar 05 17:29:49 2021 +0100
@@ -1,12 +1,17 @@
(* Title: Pure/Concurrent/timeout.ML
Author: Makarius
-Execution with (relative) timeout.
+Execution with relative timeout:
+ - timeout specification < 1ms means no timeout
+ - actual timeout is subject to system option "timeout_scale"
*)
signature TIMEOUT =
sig
exception TIMEOUT of Time.time
+ val scale: unit -> real
+ val scale_time: Time.time -> Time.time
+ val end_time: Time.time -> Time.time
val apply: Time.time -> ('a -> 'b) -> 'a -> 'b
val print: Time.time -> string
end;
@@ -16,26 +21,33 @@
exception TIMEOUT of Time.time;
+fun scale () = Options.default_real "timeout_scale";
+fun scale_time t = Time.scale (scale ()) t;
+
+fun end_time timeout = Time.now () + scale_time timeout;
+
fun apply timeout f x =
- Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts =>
- let
- val self = Thread.self ();
- val start = Time.now ();
+ if timeout < Time.fromMilliseconds 1 then f x
+ else
+ Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts =>
+ let
+ val self = Thread.self ();
+ val start = Time.now ();
- val request =
- Event_Timer.request {physical = false} (start + timeout)
- (fn () => Isabelle_Thread.interrupt_unsynchronized self);
- val result =
- Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) ();
+ val request =
+ Event_Timer.request {physical = false} (start + scale_time timeout)
+ (fn () => Isabelle_Thread.interrupt_unsynchronized self);
+ val result =
+ Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) ();
- val stop = Time.now ();
- val was_timeout = not (Event_Timer.cancel request);
- val test = Exn.capture Thread_Attributes.expose_interrupt ();
- in
- if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
- then raise TIMEOUT (stop - start)
- else (Exn.release test; Exn.release result)
- end);
+ val stop = Time.now ();
+ val was_timeout = not (Event_Timer.cancel request);
+ val test = Exn.capture Thread_Attributes.expose_interrupt ();
+ in
+ if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
+ then raise TIMEOUT (stop - start)
+ else (Exn.release test; Exn.release result)
+ end);
fun print t = "Timeout after " ^ Value.print_time t ^ "s";