--- a/NEWS Sat Mar 05 13:57:25 2016 +0100
+++ b/NEWS Sat Mar 05 17:01:45 2016 +0100
@@ -197,6 +197,10 @@
balanced blocks of Local_Theory.open_target versus
Local_Theory.close_target instead. Rare INCOMPATIBILITY.
+* Structure TimeLimit (originally from the SML/NJ library) has been
+replaced by structure Timeout, with slightly different signature.
+INCOMPATIBILITY.
+
*** System ***
--- a/src/HOL/Library/Old_SMT/old_smt_config.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_config.ML Sat Mar 05 17:01:45 2016 +0100
@@ -177,8 +177,8 @@
(* tools *)
fun with_timeout ctxt f x =
- TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x
- handle TimeLimit.TimeOut => raise Old_SMT_Failure.SMT Old_SMT_Failure.Time_Out
+ Timeout.apply (seconds (Config.get ctxt timeout)) f x
+ handle Timeout.TIMEOUT _ => raise Old_SMT_Failure.SMT Old_SMT_Failure.Time_Out
(* certificates *)
--- a/src/HOL/Library/refute.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Library/refute.ML Sat Mar 05 17:01:45 2016 +0100
@@ -1031,7 +1031,7 @@
let
val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer)
val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime
- orelse raise TimeLimit.TimeOut
+ orelse raise Timeout.TIMEOUT (Time.fromMilliseconds msecs_spent)
val init_model = (universe, [])
val init_args = {maxvars = maxvars, def_eq = false, next_idx = 1,
bounds = [], wellformed = True}
@@ -1115,9 +1115,9 @@
^ (if negate then "refutes" else "satisfies") ^ ": "
^ Syntax.string_of_term ctxt t);
if maxtime > 0 then (
- TimeLimit.timeLimit (Time.fromSeconds maxtime)
+ Timeout.apply (Time.fromSeconds maxtime)
wrapper ()
- handle TimeLimit.TimeOut =>
+ handle Timeout.TIMEOUT _ =>
(writeln ("Search terminated, time limit (" ^
string_of_int maxtime
^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Sat Mar 05 17:01:45 2016 +0100
@@ -156,7 +156,7 @@
val {context = ctxt, facts, goal} = Proof.goal st
val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt)
in
- (case try (TimeLimit.timeLimit time (Seq.pull o full_tac)) goal of
+ (case try (Timeout.apply time (Seq.pull o full_tac)) goal of
SOME (SOME _) => true
| _ => false)
end
--- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Sat Mar 05 17:01:45 2016 +0100
@@ -14,7 +14,7 @@
if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
then log (arith_tag id ^ "succeeded")
else ()
- handle TimeLimit.TimeOut => log (arith_tag id ^ "timeout")
+ handle Timeout.TIMEOUT _ => log (arith_tag id ^ "timeout")
fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done)
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Sat Mar 05 17:01:45 2016 +0100
@@ -27,7 +27,7 @@
|> add_info
|> log
end
- handle TimeLimit.TimeOut => log (metis_tag id ^ "timeout")
+ handle Timeout.TIMEOUT _ => log (metis_tag id ^ "timeout")
| ERROR msg => log (metis_tag id ^ "error: " ^ msg)
fun invoke _ = Mirabelle.register (init, Mirabelle.catch metis_tag run, done)
--- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Sat Mar 05 17:01:45 2016 +0100
@@ -15,11 +15,11 @@
val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
val quickcheck = Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key args)) 1
in
- (case TimeLimit.timeLimit timeout quickcheck pre of
+ (case Timeout.apply timeout quickcheck pre of
NONE => log (qc_tag id ^ "no counterexample")
| SOME _ => log (qc_tag id ^ "counterexample found"))
end
- handle TimeLimit.TimeOut => log (qc_tag id ^ "timeout")
+ handle Timeout.TIMEOUT _ => log (qc_tag id ^ "timeout")
| ERROR msg => log (qc_tag id ^ "error: " ^ msg)
fun invoke args =
--- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Sat Mar 05 17:01:45 2016 +0100
@@ -14,7 +14,7 @@
val thm = #goal (Proof.raw_goal st)
val refute = Refute.refute_goal thy args thm
- val _ = TimeLimit.timeLimit timeout refute subgoal
+ val _ = Timeout.apply timeout refute subgoal
in
val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Mar 05 17:01:45 2016 +0100
@@ -404,7 +404,7 @@
val time_limit =
(case hard_timeout of
NONE => I
- | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
+ | SOME secs => Timeout.apply (Time.fromSeconds secs))
fun failed failure =
({outcome = SOME failure, used_facts = [], used_from = [],
preferred_methss = (Sledgehammer_Proof_Methods.Auto_Method, []), run_time = Time.zeroTime,
@@ -434,7 +434,7 @@
{comment = "", state = st', goal = goal, subgoal = i,
subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss}
in prover params problem end)) ()
- handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
+ handle Timeout.TIMEOUT _ => failed ATP_Proof.TimedOut
| Fail "inappropriate" => failed ATP_Proof.Inappropriate
val time_prover = run_time |> Time.toMilliseconds
val msg = message (fn () => Sledgehammer.play_one_line_proof minimize preplay_timeout used_facts
@@ -590,7 +590,7 @@
"succeeded (" ^ string_of_int t ^ ")")
fun timed_method named_thms =
(with_time (Mirabelle.cpu_time apply_method named_thms), true)
- handle TimeLimit.TimeOut => (change_data id inc_proof_method_timeout; ("timeout", false))
+ handle Timeout.TIMEOUT _ => (change_data id inc_proof_method_timeout; ("timeout", false))
| ERROR msg => ("error: " ^ msg, false)
val _ = log separator
@@ -628,7 +628,7 @@
if AList.lookup (op =) args check_trivialK |> the_default trivial_default
|> Markup.parse_bool then
Try0.try0 (SOME try_timeout) ([], [], [], []) pre
- handle TimeLimit.TimeOut => false
+ handle Timeout.TIMEOUT _ => false
else false
fun apply_method () =
(Mirabelle.catch_result (proof_method_tag meth) false
--- a/src/HOL/Mirabelle/Tools/mirabelle_try0.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_try0.ML Sat Mar 05 17:01:45 2016 +0100
@@ -13,10 +13,10 @@
fun times_ten time = Time.fromMilliseconds (10 * Time.toMilliseconds time)
fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) =
- if TimeLimit.timeLimit (times_ten timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre
+ if Timeout.apply (times_ten timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre
then log (try0_tag id ^ "succeeded")
else ()
- handle TimeLimit.TimeOut => log (try0_tag id ^ "timeout")
+ handle Timeout.TIMEOUT _ => log (try0_tag id ^ "timeout")
fun invoke _ = Mirabelle.register (init, Mirabelle.catch try0_tag run, done)
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sat Mar 05 17:01:45 2016 +0100
@@ -110,7 +110,7 @@
(** quickcheck **)
fun invoke_quickcheck change_options thy t =
- TimeLimit.timeLimit (seconds 30.0)
+ Timeout.apply (seconds 30.0)
(fn _ =>
let
val ctxt' = change_options (Proof_Context.init_global thy)
@@ -123,7 +123,7 @@
NONE => (NoCex, Quickcheck.timings_of result)
| SOME _ => (GenuineCex, Quickcheck.timings_of result)
end) ()
- handle TimeLimit.TimeOut =>
+ handle Timeout.TIMEOUT _ =>
(Timeout, [("timelimit", Real.floor (Options.default_real @{system_option auto_time_limit}))])
fun quickcheck_mtd change_options quickcheck_generator =
@@ -314,7 +314,7 @@
let
val ctxt = Proof_Context.init_global thy
in
- can (TimeLimit.timeLimit (seconds 30.0)
+ can (Timeout.apply (seconds 30.0)
(Quickcheck.test_terms
((Context.proof_map (Quickcheck.set_active_testers ["exhaustive"]) #>
Config.put Quickcheck.finite_types true #>
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Sat Mar 05 17:01:45 2016 +0100
@@ -162,14 +162,14 @@
Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp
val free_Ts = fold Term.add_tfrees (op @ tsp) [] |> map TFree
val (mono_free_Ts, nonmono_free_Ts) =
- TimeLimit.timeLimit mono_timeout
+ Timeout.apply mono_timeout
(List.partition is_type_actually_monotonic) free_Ts
in
if not (null mono_free_Ts) then "MONO"
else if not (null nonmono_free_Ts) then "NONMONO"
else "NIX"
end
- handle TimeLimit.TimeOut => "TIMEOUT"
+ handle Timeout.TIMEOUT _ => "TIMEOUT"
| NOT_SUPPORTED _ => "UNSUP"
| exn => if Exn.is_interrupt exn then Exn.reraise exn else "UNKNOWN"
@@ -182,11 +182,11 @@
val t = th |> Thm.prop_of |> Type.legacy_freeze |> close_form
val neg_t = Logic.mk_implies (t, @{prop False})
val (nondef_ts, def_ts, _, _, _, _) =
- TimeLimit.timeLimit preproc_timeout (preprocess_formulas hol_ctxt [])
+ Timeout.apply preproc_timeout (preprocess_formulas hol_ctxt [])
neg_t
val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
in File.append path (res ^ "\n"); writeln res end
- handle TimeLimit.TimeOut => ()
+ handle Timeout.TIMEOUT _ => ()
in thy |> theorems_of |> List.app check_theorem end
*}
--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy Sat Mar 05 17:01:45 2016 +0100
@@ -35,7 +35,7 @@
ML {*
(*default timeout is 1 min*)
fun interpret timeout file thy =
- TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
+ Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout))
(TPTP_Interpret.interpret_file
false
[Path.explode "$TPTP"]
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Sat Mar 05 17:01:45 2016 +0100
@@ -1060,7 +1060,7 @@
tactic takes too long*)
val try_make_step =
(*FIXME const timeout*)
- (* TimeLimit.timeLimit (Time.fromSeconds 5) *)
+ (* Timeout.apply (Time.fromSeconds 5) *)
(fn ctxt' =>
let
fun thm ctxt'' = prover_tac ctxt'' prob_name (hd skel |> stock_to_string)
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Sat Mar 05 17:01:45 2016 +0100
@@ -634,7 +634,7 @@
let
val timer = Timer.startRealTimer ()
in
- TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
+ Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout))
(test_partial_reconstruction thy
#> light_output ? erase_inference_fmlas
#> @{make_string} (* FIXME *)
@@ -662,7 +662,7 @@
|> Path.implode
|> TPTP_Problem_Name.Nonstandard
in
- TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
+ Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout))
(fn prob_name =>
(can
(TPTP_Reconstruct.reconstruct ctxt (fn prob_name =>
--- a/src/HOL/TPTP/atp_problem_import.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML Sat Mar 05 17:01:45 2016 +0100
@@ -137,10 +137,8 @@
let
val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
val result =
- TimeLimit.timeLimit (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
- handle
- TimeLimit.TimeOut => NONE
- | ERROR _ => NONE
+ Timeout.apply (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
+ handle Timeout.TIMEOUT _ => NONE | ERROR _ => NONE
in
(case result of
NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
--- a/src/HOL/TPTP/atp_theory_export.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Sat Mar 05 17:01:45 2016 +0100
@@ -63,11 +63,11 @@
arguments ctxt false "" atp_timeout (File.shell_path prob_file)
(ord, K [], K [])
val outcome =
- TimeLimit.timeLimit atp_timeout Isabelle_System.bash_output command
+ Timeout.apply atp_timeout Isabelle_System.bash_output command
|> fst
|> extract_tstplike_proof_and_outcome false proof_delims known_failures
|> snd
- handle TimeLimit.TimeOut => SOME TimedOut
+ handle Timeout.TIMEOUT _ => SOME TimedOut
val _ =
tracing ("Ran ATP: " ^
(case outcome of
--- a/src/HOL/Tools/ATP/atp_systems.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Sat Mar 05 17:01:45 2016 +0100
@@ -633,7 +633,7 @@
val remote_systems = Synchronized.var "atp_remote_systems" ([] : string list)
fun get_remote_systems () =
- TimeLimit.timeLimit (seconds 10.0) (fn () =>
+ Timeout.apply (seconds 10.0) (fn () =>
(case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
(output, 0) => split_lines output
| (output, _) =>
@@ -641,7 +641,7 @@
(case extract_known_atp_failure known_perl_failures output of
SOME failure => string_of_atp_failure failure
| NONE => trim_line output ^ "."); []))) ()
- handle TimeLimit.TimeOut => []
+ handle Timeout.TIMEOUT _ => []
fun find_remote_system name [] systems =
find_first (String.isPrefix (name ^ "---")) systems
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Mar 05 17:01:45 2016 +0100
@@ -211,6 +211,7 @@
fun pick_them_nits_in_term deadline state (params : params) mode i n step
subst def_assm_ts nondef_assm_ts orig_t =
let
+ val time_start = Time.now ()
val timer = Timer.startRealTimer ()
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
@@ -248,10 +249,11 @@
val print_v = pprint_v o K o plazy
fun check_deadline () =
- if Time.compare (Time.now (), deadline) <> LESS then
- raise TimeLimit.TimeOut
- else
- ()
+ let val t = Time.now () in
+ if Time.compare (t, deadline) <> LESS
+ then raise Timeout.TIMEOUT (Time.- (t, time_start))
+ else ()
+ end
val (def_assm_ts, nondef_assm_ts) =
if assms orelse mode <> Normal then (def_assm_ts, nondef_assm_ts)
@@ -376,9 +378,9 @@
(not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
is_number_type ctxt T orelse is_bit_type T
fun is_type_actually_monotonic T =
- TimeLimit.timeLimit tac_timeout (formulas_monotonic hol_ctxt binarize T)
+ Timeout.apply tac_timeout (formulas_monotonic hol_ctxt binarize T)
(nondef_ts, def_ts)
- handle TimeLimit.TimeOut => false
+ handle Timeout.TIMEOUT _ => false
fun is_type_kind_of_monotonic T =
case triple_lookup (type_match thy) monos T of
SOME (SOME false) => false
@@ -806,7 +808,7 @@
end
end
| KK.TimedOut unsat_js =>
- (update_checked_problems problems unsat_js; raise TimeLimit.TimeOut)
+ (update_checked_problems problems unsat_js; raise Timeout.TIMEOUT Time.zeroTime)
| KK.Error (s, unsat_js) =>
(update_checked_problems problems unsat_js;
print_v (K ("Kodkod error: " ^ s ^ "."));
@@ -958,7 +960,7 @@
val outcome_code =
run_batches 0 (length batches) batches
(false, max_potential, max_genuine, 0)
- handle TimeLimit.TimeOut =>
+ handle Timeout.TIMEOUT _ =>
(print_nt (fn () => excipit "ran out of time after checking");
if !met_potential > 0 then potentialN else unknownN)
val _ = print_v (fn () =>
@@ -986,7 +988,7 @@
val unknown_outcome = (unknownN, [])
val deadline = Time.+ (Time.now (), timeout)
val outcome as (outcome_code, _) =
- TimeLimit.timeLimit (Time.+ (timeout, timeout_bonus))
+ Timeout.apply (Time.+ (timeout, timeout_bonus))
(pick_them_nits_in_term deadline state params mode i n step subst
def_assm_ts nondef_assm_ts) orig_t
handle TOO_LARGE (_, details) =>
@@ -999,7 +1001,7 @@
(print_t "% SZS status GaveUp";
print_nt ("Malformed Kodkodi output: " ^ details ^ ".");
unknown_outcome)
- | TimeLimit.TimeOut =>
+ | Timeout.TIMEOUT _ =>
(print_t "% SZS status TimedOut";
print_nt "Nitpick ran out of time."; unknown_outcome)
in
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Mar 05 17:01:45 2016 +0100
@@ -577,18 +577,18 @@
|> List.partition (member (op =) ["dptsat", "cdclite"] o fst)
val res =
if null nonml_solvers then
- TimeLimit.timeLimit tac_timeout (snd (hd ml_solvers)) prop
+ Timeout.apply tac_timeout (snd (hd ml_solvers)) prop
else
- TimeLimit.timeLimit ml_solver_timeout (snd (hd ml_solvers)) prop
- handle TimeLimit.TimeOut =>
- TimeLimit.timeLimit tac_timeout
+ Timeout.apply ml_solver_timeout (snd (hd ml_solvers)) prop
+ handle Timeout.TIMEOUT _ =>
+ Timeout.apply tac_timeout
(SAT_Solver.invoke_solver "auto") prop
in
case res of
SAT_Solver.SATISFIABLE assigns => do_assigns assigns
| _ => (trace_msg (K "*** Unsolvable"); NONE)
end
- handle TimeLimit.TimeOut => (trace_msg (K "*** Timed out"); NONE)
+ handle Timeout.TIMEOUT _ => (trace_msg (K "*** Timed out"); NONE)
end
type mcontext =
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Mar 05 17:01:45 2016 +0100
@@ -273,7 +273,7 @@
val eta_expand = ATP_Util.eta_expand
fun DETERM_TIMEOUT delay tac st =
- Seq.of_list (the_list (TimeLimit.timeLimit delay (fn () => SINGLE tac st) ()))
+ Seq.of_list (the_list (Timeout.apply delay (fn () => SINGLE tac st) ()))
val indent_size = 2
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Mar 05 17:01:45 2016 +0100
@@ -882,7 +882,7 @@
val args' = map (rename_vars_term renaming) args
val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p
val _ = tracing ("Generated prolog program:\n" ^ prog)
- val solution = TimeLimit.timeLimit timeout (fn prog =>
+ val solution = Timeout.apply timeout (fn prog =>
Isabelle_System.with_tmp_file "prolog_file" "" (fn prolog_file =>
(File.write prolog_file prog; invoke system prolog_file))) prog
val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Mar 05 17:01:45 2016 +0100
@@ -1890,7 +1890,7 @@
let
val [nrandom, size, depth] = map Code_Numeral.natural_of_integer arguments
in
- rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
+ rpair NONE (Timeout.apply time_limit (fn () => fst (Limited_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict
(get_dseq_random_result, put_dseq_random_result,
"Predicate_Compile_Core.put_dseq_random_result")
@@ -1902,7 +1902,7 @@
depth true)) ())
end
| DSeq =>
- rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
+ rpair NONE (Timeout.apply time_limit (fn () => fst (Limited_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict
(get_dseq_result, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
ctxt NONE Limited_Sequence.map t' [])
@@ -1911,7 +1911,7 @@
let
val depth = Code_Numeral.natural_of_integer (the_single arguments)
in
- rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
+ rpair NONE (Timeout.apply time_limit (fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict
(get_new_dseq_result, put_new_dseq_result,
"Predicate_Compile_Core.put_new_dseq_result")
@@ -1925,7 +1925,7 @@
in
if stats then
apsnd (SOME o accumulate o map Code_Numeral.integer_of_natural)
- (split_list (TimeLimit.timeLimit time_limit
+ (split_list (Timeout.apply time_limit
(fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict
(get_lseq_random_stats_result, put_lseq_random_stats_result,
@@ -1936,7 +1936,7 @@
|> Lazy_Sequence.map (apfst proc))
t' [] nrandom size seed depth))) ()))
else rpair NONE
- (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
+ (Timeout.apply time_limit (fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict
(get_lseq_random_result, put_lseq_random_result,
"Predicate_Compile_Core.put_lseq_random_result")
@@ -1947,11 +1947,11 @@
t' [] nrandom size seed depth))) ())
end
| _ =>
- rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Predicate.yieldn k
+ rpair NONE (Timeout.apply time_limit (fn () => fst (Predicate.yieldn k
(Code_Runtime.dynamic_value_strict
(get_pred_result, put_pred_result, "Predicate_Compile_Core.put_pred_result")
ctxt NONE Predicate.map t' []))) ()))
- handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
+ handle Timeout.TIMEOUT _ => error "Reached timeout during execution of values"
in ((T, ts), statistics) end;
fun values param_user_modes ((raw_expected, stats), comp_options) k t_compr ctxt =
--- a/src/HOL/Tools/SMT/smt_config.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Sat Mar 05 17:01:45 2016 +0100
@@ -196,8 +196,8 @@
(* tools *)
fun with_time_limit ctxt timeout_config f x =
- TimeLimit.timeLimit (seconds (Config.get ctxt timeout_config)) f x
- handle TimeLimit.TimeOut => raise SMT_Failure.SMT SMT_Failure.Time_Out
+ Timeout.apply (seconds (Config.get ctxt timeout_config)) f x
+ handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
fun with_timeout ctxt = with_time_limit ctxt timeout
--- a/src/HOL/Tools/SMT/z3_replay.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/SMT/z3_replay.ML Sat Mar 05 17:01:45 2016 +0100
@@ -72,7 +72,7 @@
val replay = Timing.timing (replay_thm ctxt assumed nthms)
val ({elapsed, ...}, thm) =
SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay step
- handle TimeLimit.TimeOut => raise SMT_Failure.SMT SMT_Failure.Time_Out
+ handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
val stats' = Symtab.cons_list (Z3_Proof.string_of_rule rule, Time.toMilliseconds elapsed) stats
in (Inttab.update (id, (fixes, thm)) proofs, stats') end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sat Mar 05 17:01:45 2016 +0100
@@ -207,12 +207,12 @@
in (outcome_code, message) end
in
if mode = Auto_Try then
- let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
+ let val (outcome_code, message) = Timeout.apply timeout go () in
(outcome_code, if outcome_code = someN then [message ()] else [])
end
else
let
- val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
+ val (outcome_code, message) = Timeout.apply hard_timeout go ()
val outcome =
if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else ""
val _ =
@@ -305,7 +305,7 @@
end
in
launch_provers ()
- handle TimeLimit.TimeOut =>
+ handle Timeout.TIMEOUT _ =>
(print "Sledgehammer ran out of time."; (unknownN, []))
end
|> `(fn (outcome_code, _) => outcome_code = someN))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Mar 05 17:01:45 2016 +0100
@@ -418,7 +418,7 @@
let val thy = Proof_Context.theory_of ctxt in
stmt_xs
|> filter (fn (_, T) => type_match thy (T, ind_T))
- |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout
+ |> map_filter (try (Timeout.apply instantiate_induct_timeout
(instantiate_induct_rule ctxt stmt p_name ax)))
end
| NONE => [ax])
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sat Mar 05 17:01:45 2016 +0100
@@ -97,8 +97,8 @@
fun take_time timeout tac arg =
let val timing = Timing.start () in
- (TimeLimit.timeLimit timeout tac arg; Played (#cpu (Timing.result timing)))
- handle TimeLimit.TimeOut => Play_Timed_Out timeout
+ (Timeout.apply timeout tac arg; Played (#cpu (Timing.result timing)))
+ handle Timeout.TIMEOUT _ => Play_Timed_Out timeout
end
fun resolve_fact_names ctxt names =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sat Mar 05 17:01:45 2016 +0100
@@ -296,7 +296,7 @@
|> File.write_list prob_path
val ((output, run_time), (atp_proof, outcome)) =
- TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
+ Timeout.apply generous_slice_timeout Isabelle_System.bash_output command
|>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
|> fst |> split_time
|> (fn accum as (output, _) =>
@@ -305,7 +305,7 @@
|>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name)
atp_problem
handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable)))
- handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
+ handle Timeout.TIMEOUT _ => (("", slice_timeout), ([], SOME TimedOut))
val outcome =
(case outcome of
--- a/src/HOL/Tools/try0.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/Tools/try0.ML Sat Mar 05 17:01:45 2016 +0100
@@ -27,7 +27,7 @@
fun can_apply timeout_opt pre post tac st =
let val {goal, ...} = Proof.goal st in
(case (case timeout_opt of
- SOME timeout => TimeLimit.timeLimit timeout
+ SOME timeout => Timeout.apply 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)
--- a/src/Pure/Concurrent/time_limit.ML Sat Mar 05 13:57:25 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-(* Title: Pure/Concurrent/time_limit.ML
- Author: Makarius
-
-Execution with time limit (relative timeout).
-*)
-
-signature TIME_LIMIT =
-sig
- exception TimeOut
- val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
-end;
-
-structure TimeLimit: TIME_LIMIT =
-struct
-
-exception TimeOut;
-
-fun timeLimit timeout f x =
- Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
- let
- val self = Thread.self ();
-
- val request =
- Event_Timer.request (Time.+ (Time.now (), timeout))
- (fn () => Standard_Thread.interrupt_unsynchronized self);
-
- val result =
- Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
-
- val was_timeout = not (Event_Timer.cancel request);
- val test = Exn.capture Multithreading.interrupted ();
- in
- if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
- then raise TimeOut
- else (Exn.release test; Exn.release result)
- end);
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/timeout.ML Sat Mar 05 17:01:45 2016 +0100
@@ -0,0 +1,42 @@
+(* Title: Pure/Concurrent/timeout.ML
+ Author: Makarius
+
+Execution with (relative) timeout.
+*)
+
+signature TIMEOUT =
+sig
+ exception TIMEOUT of Time.time
+ val apply: Time.time -> ('a -> 'b) -> 'a -> 'b
+ val print: Time.time -> string
+end;
+
+structure Timeout: TIMEOUT =
+struct
+
+exception TIMEOUT of Time.time;
+
+fun apply timeout f x =
+ Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
+ let
+ val self = Thread.self ();
+ val start = Time.now ();
+
+ val request =
+ Event_Timer.request (Time.+ (start, timeout))
+ (fn () => Standard_Thread.interrupt_unsynchronized self);
+ val result =
+ Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
+
+ val stop = Time.now ();
+ val was_timeout = not (Event_Timer.cancel request);
+ val test = Exn.capture Multithreading.interrupted ();
+ in
+ if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
+ then raise TIMEOUT (Time.- (stop, start))
+ else (Exn.release test; Exn.release result)
+ end);
+
+fun print t = "Timeout after " ^ Time.toString t ^ "s";
+
+end;
--- a/src/Pure/Isar/runtime.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/Pure/Isar/runtime.ML Sat Mar 05 17:01:45 2016 +0100
@@ -112,7 +112,7 @@
let
val msg =
(case exn of
- TimeLimit.TimeOut => "Timeout"
+ Timeout.TIMEOUT t => Timeout.print t
| TOPLEVEL_ERROR => "Error"
| ERROR "" => "Error"
| ERROR msg => msg
--- a/src/Pure/ROOT Sat Mar 05 13:57:25 2016 +0100
+++ b/src/Pure/ROOT Sat Mar 05 17:01:45 2016 +0100
@@ -19,7 +19,7 @@
"Concurrent/standard_thread.ML"
"Concurrent/synchronized.ML"
"Concurrent/task_queue.ML"
- "Concurrent/time_limit.ML"
+ "Concurrent/timeout.ML"
"Concurrent/unsynchronized.ML"
"General/alist.ML"
"General/antiquote.ML"
--- a/src/Pure/ROOT.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/Pure/ROOT.ML Sat Mar 05 17:01:45 2016 +0100
@@ -203,7 +203,7 @@
use "Concurrent/task_queue.ML";
use "Concurrent/future.ML";
use "Concurrent/event_timer.ML";
-use "Concurrent/time_limit.ML";
+use "Concurrent/timeout.ML";
use "Concurrent/lazy.ML";
use "Concurrent/par_list.ML";
--- a/src/Tools/quickcheck.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/Tools/quickcheck.ML Sat Mar 05 17:01:45 2016 +0100
@@ -282,9 +282,9 @@
fun limit timeout (limit_time, is_interactive) f exc () =
if limit_time then
- TimeLimit.timeLimit timeout f ()
- handle TimeLimit.TimeOut =>
- if is_interactive then exc () else raise TimeLimit.TimeOut
+ Timeout.apply timeout f ()
+ handle timeout_exn as Timeout.TIMEOUT _ =>
+ if is_interactive then exc () else Exn.reraise timeout_exn
else f ();
fun message ctxt s = if Config.get ctxt quiet then () else writeln s;
--- a/src/Tools/try.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/Tools/try.ML Sat Mar 05 17:01:45 2016 +0100
@@ -110,7 +110,7 @@
val auto_time_limit = Options.default_real @{system_option auto_time_limit}
in
if auto_time_limit > 0.0 then
- (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of
+ (case Timeout.apply (seconds auto_time_limit) (fn () => tool true state) () of
(true, (_, outcome)) => List.app Output.information outcome
| _ => ())
else ()