# HG changeset patch # User blanchet # Date 1355597832 -3600 # Node ID 31313171deb5be0da7116be5fd56fe85adb1ed71 # Parent 6209bc89faa36818bb4f55b83433651f506873ec thread no timeout properly diff -r 6209bc89faa3 -r 31313171deb5 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Sat Dec 15 18:48:58 2012 +0100 +++ b/src/HOL/TPTP/mash_eval.ML Sat Dec 15 19:57:12 2012 +0100 @@ -16,8 +16,12 @@ structure MaSh_Eval : MASH_EVAL = struct +open Sledgehammer_Util open Sledgehammer_Fact +open Sledgehammer_MePo open Sledgehammer_MaSh +open Sledgehammer_Provers +open Sledgehammer_Isar val MePoN = "MePo" val MaShN = "MaSh" @@ -31,12 +35,12 @@ val _ = File.write report_path "" fun print s = (tracing s; File.append report_path (s ^ "\n")) val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = - Sledgehammer_Isar.default_params ctxt [] + default_params ctxt [] val prover = hd provers val slack_max_facts = generous_max_facts (the max_facts) val sugg_path = sugg_file_name |> Path.explode val lines = sugg_path |> File.read_lines - val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt + val css = clasimpset_rule_table_of ctxt val facts = all_facts ctxt true false Symtab.empty [] [] css val all_names = build_all_names nickname_of facts val mepo_ok = Unsynchronized.ref 0 @@ -46,7 +50,7 @@ fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) fun index_string (j, s) = s ^ "@" ^ string_of_int j fun str_of_res label facts ({outcome, run_time, used_facts, ...} - : Sledgehammer_Provers.prover_result) = + : prover_result) = let val facts = facts |> map (fn ((name, _), _) => name ()) in " " ^ label ^ ": " ^ (if is_none outcome then @@ -77,9 +81,9 @@ val isar_deps = isar_dependencies_of all_names th |> these val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) val mepo_facts = - Sledgehammer_MePo.mepo_suggested_facts ctxt params prover - slack_max_facts NONE hyp_ts concl_t facts - |> Sledgehammer_MePo.weight_mepo_facts + mepo_suggested_facts ctxt params prover slack_max_facts NONE hyp_ts + concl_t facts + |> weight_mepo_facts val (mash_facts, mash_unks) = find_mash_suggestions slack_max_facts suggs facts [] [] |>> weight_mash_facts @@ -93,9 +97,8 @@ "goal_" ^ string_of_int j ^ "__" ^ escape_meta name ^ "__" ^ heading in - Config.put Sledgehammer_Provers.dest_dir dir - #> Config.put Sledgehammer_Provers.problem_prefix - (prob_prefix ^ "__") + Config.put dest_dir dir + #> Config.put problem_prefix (prob_prefix ^ "__") #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix) end | set_file_name _ NONE = I @@ -105,7 +108,7 @@ val facts = facts |> map get - |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t + |> maybe_instantiate_inducts ctxt hyp_ts concl_t |> take (the max_facts) |> map nickify val ctxt = ctxt |> set_file_name heading prob_dir_name @@ -128,11 +131,12 @@ " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^ Real.fmt (StringCvt.FIX (SOME 1)) (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)" - val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts + val inst_inducts = Config.get ctxt instantiate_inducts val options = [prover, string_of_int (the max_facts) ^ " facts", "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc, - the_default "smart" lam_trans, ATP_Util.string_from_time timeout, + the_default "smart" lam_trans, + ATP_Util.string_from_time (timeout |> the_default one_year), "instantiate_inducts" |> not inst_inducts ? prefix "dont_"] val n = length lines in diff -r 6209bc89faa3 -r 31313171deb5 src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Dec 15 18:48:58 2012 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Dec 15 19:57:12 2012 +0100 @@ -283,9 +283,7 @@ val monomorphic_term = ATP_Util.monomorphic_term val specialize_type = ATP_Util.specialize_type val eta_expand = ATP_Util.eta_expand - -fun time_limit NONE = I - | time_limit (SOME delay) = TimeLimit.timeLimit delay +val time_limit = Sledgehammer_Util.time_limit fun DETERM_TIMEOUT delay tac st = Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ())) diff -r 6209bc89faa3 -r 31313171deb5 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Dec 15 18:48:58 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Dec 15 19:57:12 2012 +0100 @@ -249,8 +249,6 @@ end)] end -val the_timeout = the_default infinite_timeout - fun extract_params mode default_params override_params = let val raw_params = rev override_params @ rev default_params @@ -320,11 +318,10 @@ val slice = mode <> Auto_Try andalso lookup_bool "slice" val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize" - val timeout = - (if mode = Auto_Try then NONE else lookup_time "timeout") |> the_timeout + val timeout = if mode = Auto_Try then NONE else lookup_time "timeout" val preplay_timeout = - if mode = Auto_Try then Time.zeroTime - else lookup_time "preplay_timeout" |> the_timeout + if mode = Auto_Try then SOME Time.zeroTime + else lookup_time "preplay_timeout" val expect = lookup_string "expect" in {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, diff -r 6209bc89faa3 -r 31313171deb5 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Dec 15 18:48:58 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Dec 15 19:57:12 2012 +0100 @@ -818,7 +818,7 @@ if is_smt_prover ctxt prover then () else - launch_thread timeout (fn () => + launch_thread (timeout |> the_default one_day) (fn () => let val thy = Proof_Context.theory_of ctxt val name = freshish_name () @@ -920,7 +920,10 @@ (commit false adds [] []; ([], next_commit_time ())) else (adds, next_commit) - val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) + val timed_out = + case learn_timeout of + SOME timeout => Time.> (Timer.checkRealTimer timer, timeout) + | NONE => false in (adds, ([name], n, next_commit, timed_out)) end val n = if null new_facts then @@ -951,7 +954,10 @@ (commit false [] reps flops; ([], [], next_commit_time ())) else (reps, flops, next_commit) - val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) + val timed_out = + case learn_timeout of + SOME timeout => Time.> (Timer.checkRealTimer timer, timeout) + | NONE => false in ((reps, flops), (n, next_commit, timed_out)) end val n = if not run_prover orelse null old_facts then @@ -1003,15 +1009,15 @@ val num_facts = length facts val prover = hd provers fun learn auto_level run_prover = - mash_learn_facts ctxt params prover auto_level run_prover infinite_timeout - facts + mash_learn_facts ctxt params prover auto_level run_prover NONE facts |> Output.urgent_message in if run_prover then ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ - " timeout: " ^ string_from_time timeout ^ - ").\n\nCollecting Isar proofs first..." + (case timeout of + SOME timeout => " timeout: " ^ string_from_time timeout + | NONE => "") ^ ").\n\nCollecting Isar proofs first..." |> Output.urgent_message; learn 1 false; "Now collecting automatic proofs. This may take several hours. You can \ @@ -1048,9 +1054,12 @@ let fun maybe_learn () = if learn andalso not (Async_Manager.has_running_threads MaShN) andalso - Time.toSeconds timeout >= min_secs_for_learning then - let val timeout = time_mult learn_timeout_slack timeout in - launch_thread timeout + (timeout = NONE orelse + Time.toSeconds (the timeout) >= min_secs_for_learning) then + let + val timeout = Option.map (time_mult learn_timeout_slack) timeout + in + launch_thread (timeout |> the_default one_day) (fn () => (true, mash_learn_facts ctxt params prover 2 false timeout facts)) end diff -r 6209bc89faa3 -r 31313171deb5 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Dec 15 18:48:58 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Dec 15 19:57:12 2012 +0100 @@ -61,8 +61,12 @@ val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ - (if verbose then " (timeout: " ^ string_from_time timeout ^ ")" - else "") ^ "...") + (if verbose then + case timeout of + SOME timeout => " (timeout: " ^ string_from_time timeout ^ ")" + | _ => "" + else + "") ^ "...") val {goal, ...} = Proof.goal state val facts = facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) @@ -101,10 +105,11 @@ part of the timeout. *) val slack_msecs = 200 -fun new_timeout timeout run_time = - Int.min (Time.toMilliseconds timeout, - Time.toMilliseconds run_time + slack_msecs) - |> Time.fromMilliseconds +fun new_timeout NONE _ = NONE + | new_timeout (SOME timeout) run_time = + Int.min (Time.toMilliseconds timeout, + Time.toMilliseconds run_time + slack_msecs) + |> Time.fromMilliseconds |> SOME (* The linear algorithm usually outperforms the binary algorithm when over 60% of the facts are actually needed. The binary algorithm is much more @@ -222,11 +227,12 @@ | {outcome = SOME TimedOut, preplay, ...} => (NONE, (preplay, - fn _ => "Timeout: You can increase the time limit using the \ - \\"timeout\" option (e.g., \"timeout = " ^ - string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ - "\").", - "")) + fn _ => + "Timeout: You can increase the time limit using the \"timeout\" \ + \option (e.g., \"timeout = " ^ + string_of_int (10 + Time.toMilliseconds + (timeout |> the_default (seconds 60.0)) div 1000) ^ + "\").", "")) | {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message, ""))) handle ERROR msg => diff -r 6209bc89faa3 -r 31313171deb5 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Dec 15 18:48:58 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Dec 15 19:57:12 2012 +0100 @@ -37,8 +37,8 @@ isar_shrink : real, slice : bool, minimize : bool option, - timeout : Time.time, - preplay_timeout : Time.time, + timeout : Time.time option, + preplay_timeout : Time.time option, expect : string} type relevance_fudge = @@ -330,8 +330,8 @@ isar_shrink : real, slice : bool, minimize : bool option, - timeout : Time.time, - preplay_timeout : Time.time, + timeout : Time.time option, + preplay_timeout : Time.time option, expect : string} type relevance_fudge = @@ -479,7 +479,7 @@ let val {context = ctxt, facts, goal} = Proof.goal state val full_tac = Method.insert_tac facts i THEN tac ctxt i - in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end + in time_limit timeout (try (Seq.pull o full_tac)) goal end fun tac_for_reconstructor (Metis (type_enc, lam_trans)) = metis_tac [type_enc] lam_trans @@ -500,39 +500,40 @@ fun play_one_line_proof mode debug verbose timeout pairs state i preferred reconstrs = let - val _ = - if mode = Minimize andalso Time.> (timeout, Time.zeroTime) then - Output.urgent_message "Preplaying proof..." - else - () - val ths = pairs |> sort_wrt (fst o fst) |> map snd fun get_preferred reconstrs = if member (op =) reconstrs preferred then preferred else List.last reconstrs - fun play [] [] = Failed_to_Play (get_preferred reconstrs) - | play timed_outs [] = - Trust_Playable (get_preferred timed_outs, SOME timeout) - | play timed_out (reconstr :: reconstrs) = - let - val _ = - if verbose then - "Trying \"" ^ string_for_reconstructor reconstr ^ "\" for " ^ - string_from_time timeout ^ "..." - |> Output.urgent_message - else - () - val timer = Timer.startRealTimer () - in - case timed_reconstructor reconstr debug timeout ths state i of - SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer) - | _ => play timed_out reconstrs - end - handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs in - if timeout = Time.zeroTime then + if timeout = SOME Time.zeroTime then Trust_Playable (get_preferred reconstrs, NONE) else - play [] reconstrs + let + val _ = + if mode = Minimize then Output.urgent_message "Preplaying proof..." + else () + val ths = pairs |> sort_wrt (fst o fst) |> map snd + fun play [] [] = Failed_to_Play (get_preferred reconstrs) + | play timed_outs [] = + Trust_Playable (get_preferred timed_outs, timeout) + | play timed_out (reconstr :: reconstrs) = + let + val _ = + if verbose then + "Trying \"" ^ string_for_reconstructor reconstr ^ "\"" ^ + (case timeout of + SOME timeout => " for " ^ string_from_time timeout + | NONE => "") ^ "..." + |> Output.urgent_message + else + () + val timer = Timer.startRealTimer () + in + case timed_reconstructor reconstr debug timeout ths state i of + SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer) + | _ => play timed_out reconstrs + end + handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs + in play [] reconstrs end end @@ -734,20 +735,26 @@ val sound = is_type_enc_sound type_enc val real_ms = Real.fromInt o Time.toMilliseconds val slice_timeout = - ((real_ms time_left - |> (if slice < num_actual_slices - 1 then - curry Real.min (time_frac * real_ms timeout) - else - I)) - * 0.001) |> seconds + case time_left of + SOME time_left => + ((real_ms time_left + |> (if slice < num_actual_slices - 1 then + curry Real.min (time_frac * real_ms (the timeout)) + else + I)) + * 0.001) + |> seconds |> SOME + | NONE => NONE val generous_slice_timeout = - Time.+ (slice_timeout, atp_timeout_slack) + Option.map (curry Time.+ atp_timeout_slack) slice_timeout val _ = if debug then quote name ^ " slice #" ^ string_of_int (slice + 1) ^ " with " ^ string_of_int num_facts ^ " fact" ^ - plural_s num_facts ^ " for " ^ - string_from_time slice_timeout ^ "..." + plural_s num_facts ^ + (case slice_timeout of + SOME timeout => " for " ^ string_from_time timeout + | NONE => "") ^ "..." |> Output.urgent_message else () @@ -778,7 +785,8 @@ fun ord_info () = atp_problem_term_order_info atp_problem val ord = effective_term_order ctxt name val full_proof = debug orelse isar_proofs - val args = arguments ctxt full_proof extra slice_timeout + val args = arguments ctxt full_proof extra + (slice_timeout |> the_default one_day) (ord, ord_info, sel_weights) val command = "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ @@ -790,8 +798,8 @@ |> cons ("% " ^ command ^ "\n") |> File.write_list prob_path val ((output, run_time), (atp_proof, outcome)) = - TimeLimit.timeLimit generous_slice_timeout - Isabelle_System.bash_output command + time_limit generous_slice_timeout Isabelle_System.bash_output + command |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else @@ -805,7 +813,7 @@ handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete))) handle TimeLimit.TimeOut => - (("", slice_timeout), ([], SOME TimedOut)) + (("", the slice_timeout), ([], SOME TimedOut)) val outcome = case outcome of NONE => @@ -826,9 +834,13 @@ fun maybe_run_slice slice (result as (cache, (_, run_time0, _, SOME _))) = let - val time_left = Time.- (timeout, Timer.checkRealTimer timer) + val time_left = + Option.map + (fn timeout => Time.- (timeout, Timer.checkRealTimer timer)) + timeout in - if Time.<= (time_left, Time.zeroTime) then + if time_left <> NONE andalso + Time.<= (the time_left, Time.zeroTime) then result else run_slice time_left cache slice @@ -979,22 +991,25 @@ (repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances default_max_new_mono_instances) - val ms = timeout |> Time.toMilliseconds val slice_timeout = - if slice < max_slices then - Int.min (ms, - Int.max (1000 * Config.get ctxt smt_slice_min_secs, - Real.ceil (Config.get ctxt smt_slice_time_frac - * Real.fromInt ms))) - |> Time.fromMilliseconds + if slice < max_slices andalso timeout <> NONE then + let val ms = timeout |> the |> Time.toMilliseconds in + Int.min (ms, + Int.max (1000 * Config.get ctxt smt_slice_min_secs, + Real.ceil (Config.get ctxt smt_slice_time_frac + * Real.fromInt ms))) + |> Time.fromMilliseconds |> SOME + end else timeout val num_facts = length facts val _ = if debug then quote name ^ " slice " ^ string_of_int slice ^ " with " ^ - string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for " ^ - string_from_time slice_timeout ^ "..." + string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ + (case slice_timeout of + SOME timeout => " for " ^ string_from_time timeout + | NONE => "") ^ "..." |> Output.urgent_message else () @@ -1004,7 +1019,7 @@ val state_facts = these (try (#facts o Proof.goal) state) val (outcome, used_facts) = SMT_Solver.smt_filter_preprocess ctxt state_facts goal facts i - |> SMT_Solver.smt_filter_apply slice_timeout + |> SMT_Solver.smt_filter_apply (slice_timeout |> the_default one_day) |> (fn {outcome, used_facts} => (outcome, used_facts)) handle exn => if Exn.is_interrupt exn then reraise exn @@ -1022,10 +1037,14 @@ | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *) | SOME SMT_Failure.Out_Of_Memory => true | SOME (SMT_Failure.Other_Failure _) => true - val timeout = Time.- (timeout, Timer.checkRealTimer timer) + val timeout = + Option.map + (fn timeout => Time.- (timeout, Timer.checkRealTimer timer)) + timeout in if too_many_facts_perhaps andalso slice < max_slices andalso - num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then + num_facts > 0 andalso + (timeout = NONE orelse Time.> (the timeout, Time.zeroTime)) then let val new_num_facts = Real.ceil (Config.get ctxt smt_slice_fact_frac diff -r 6209bc89faa3 -r 31313171deb5 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sat Dec 15 18:48:58 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sat Dec 15 19:57:12 2012 +0100 @@ -23,7 +23,7 @@ type one_line_params = play * string * (string * stature) list * minimize_command * int * int type isar_params = - bool * bool * Time.time * real * string Symtab.table + bool * bool * Time.time option * real * string Symtab.table * (string * stature) list vector * int Symtab.table * string proof * thm val smtN : string @@ -592,7 +592,7 @@ in chain_proof NONE end type isar_params = - bool * bool * Time.time * real * string Symtab.table + bool * bool * Time.time option * real * string Symtab.table * (string * stature) list vector * int Symtab.table * string proof * thm fun isar_proof_text ctxt isar_proofs @@ -607,7 +607,7 @@ if is_typed_helper_used_in_atp_proof atp_proof then full_typesN else partial_typesN val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans - val preplay = preplay_timeout <> seconds 0.0 + val preplay = preplay_timeout <> SOME Time.zeroTime fun isar_proof_of () = let @@ -693,10 +693,12 @@ |> redirect_graph axioms tainted |> map (do_inf true) |> append assms - |> (if not preplay andalso isar_shrink <= 1.0 - then pair (false, (true, seconds 0.0)) #> swap - else shrink_proof debug ctxt type_enc lam_trans preplay - preplay_timeout (if isar_proofs then isar_shrink else 1000.0)) + |> (if not preplay andalso isar_shrink <= 1.0 then + pair (false, (true, seconds 0.0)) #> swap + else + shrink_proof debug ctxt type_enc lam_trans preplay + preplay_timeout + (if isar_proofs then isar_shrink else 1000.0)) (* |>> reorder_proof_to_minimize_jumps (* ? *) *) |>> chain_direct_proof |>> kill_useless_labels_in_proof diff -r 6209bc89faa3 -r 31313171deb5 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Dec 15 18:48:58 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Dec 15 19:57:12 2012 +0100 @@ -68,7 +68,7 @@ {state, goal, subgoal, subgoal_count, facts} name = let val ctxt = Proof.context_of state - val hard_timeout = Time.+ (timeout, timeout) + val hard_timeout = time_mult 2.0 (timeout |> the_default one_day) val birth_time = Time.now () val death_time = Time.+ (birth_time, hard_timeout) val max_facts = @@ -131,7 +131,7 @@ 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) = time_limit timeout go () in (outcome_code, state |> outcome_code = someN diff -r 6209bc89faa3 -r 31313171deb5 src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Sat Dec 15 18:48:58 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Sat Dec 15 19:57:12 2012 +0100 @@ -9,8 +9,8 @@ sig type isar_step = Sledgehammer_Proof.isar_step val shrink_proof : - bool -> Proof.context -> string -> string -> bool -> Time.time -> real - -> isar_step list -> isar_step list * (bool * (bool * Time.time)) + bool -> Proof.context -> string -> string -> bool -> Time.time option + -> real -> isar_step list -> isar_step list * (bool * (bool * Time.time)) end structure Sledgehammer_Shrink : SLEDGEHAMMER_SHRINK = @@ -46,7 +46,7 @@ (* Timing *) fun ext_time_add (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2)) -val no_time = (false, seconds 0.0) +val no_time = (false, Time.zeroTime) fun take_time timeout tac arg = let val timing = Timing.start () in (TimeLimit.timeLimit timeout tac arg; @@ -59,15 +59,18 @@ fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout isar_shrink proof = let + (* 60 seconds seems like a good interpreation of "no timeout" *) + val preplay_timeout = preplay_timeout |> the_default (seconds 60.0) + (* handle metis preplay fail *) local open Unsynchronized val metis_fail = ref false in fun handle_metis_fail try_metis () = - try_metis () handle _ => (metis_fail := true ; SOME (seconds 0.0)) + try_metis () handle _ => (metis_fail := true; SOME Time.zeroTime) fun get_time lazy_time = - if !metis_fail then SOME (seconds 0.0) else Lazy.force lazy_time + if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time val metis_fail = fn () => !metis_fail end @@ -120,7 +123,7 @@ |> maps (thms_of_name ctxt) fun try_metis timeout (succedent, Prove (_, _, t, byline)) = - if not preplay then (fn () => SOME (seconds 0.0)) else + if not preplay then (fn () => SOME Time.zeroTime) else (case byline of By_Metis fact_names => let @@ -154,7 +157,7 @@ in take_time timeout (fn () => goal tac) end) - | try_metis _ _ = (fn () => SOME (seconds 0.0) ) + | try_metis _ _ = (fn () => SOME Time.zeroTime) val try_metis_quietly = the_default NONE oo try oo try_metis @@ -195,7 +198,7 @@ NONE => (NONE, metis_time) | some_t12 => (SOME s12, metis_time - |> replace (seconds 0.0 |> SOME |> Lazy.value) i + |> replace (Time.zeroTime |> SOME |> Lazy.value) i |> replace (Lazy.value some_t12) j) end)) diff -r 6209bc89faa3 -r 31313171deb5 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Dec 15 18:48:58 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Dec 15 19:57:12 2012 +0100 @@ -19,6 +19,9 @@ val reserved_isar_keyword_table : unit -> unit Symtab.table val thms_in_proof : string Symtab.table option -> thm -> string list val thms_of_name : Proof.context -> string -> thm list + val one_day : Time.time + val one_year : Time.time + val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b end; @@ -119,6 +122,12 @@ |> Source.exhaust end +val one_day = seconds (24.0 * 60.0 * 60.0) +val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0) + +fun time_limit NONE = I + | time_limit (SOME delay) = TimeLimit.timeLimit delay + fun with_vanilla_print_mode f x = Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) f x