# HG changeset patch # User blanchet # Date 1282144597 -7200 # Node ID bd443b426d56931d6ba4636a683fe5c1818d3779 # Parent b03f8fe043ec1a7a3e5440ddf8e9061e220ebbc2 get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize" diff -r b03f8fe043ec -r bd443b426d56 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Aug 18 17:09:05 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Aug 18 17:16:37 2010 +0200 @@ -389,7 +389,7 @@ |> Option.map (fst o read_int o explode) |> the_default 5 val params = Sledgehammer_Isar.default_params thy - [("atps", prover_name), ("minimize_timeout", Int.toString timeout ^ " s")] + [("atps", prover_name), ("timeout", Int.toString timeout ^ " s")] val minimize = Sledgehammer_Fact_Minimize.minimize_theorems params 1 (subgoal_count st) val _ = log separator diff -r b03f8fe043ec -r bd443b426d56 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 18 17:09:05 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 18 17:16:37 2010 +0200 @@ -25,8 +25,7 @@ defs_relevant: bool, isar_proof: bool, isar_shrink_factor: int, - timeout: Time.time, - minimize_timeout: Time.time} + timeout: Time.time} type problem = {subgoal: int, goal: Proof.context * (thm list * thm), @@ -95,8 +94,7 @@ defs_relevant: bool, isar_proof: bool, isar_shrink_factor: int, - timeout: Time.time, - minimize_timeout: Time.time} + timeout: Time.time} type problem = {subgoal: int, diff -r b03f8fe043ec -r bd443b426d56 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 18 17:09:05 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 18 17:16:37 2010 +0200 @@ -58,8 +58,7 @@ relevance_convergence = relevance_convergence, max_relevant_per_iter = NONE, theory_relevant = NONE, defs_relevant = defs_relevant, isar_proof = isar_proof, - isar_shrink_factor = isar_shrink_factor, timeout = timeout, - minimize_timeout = timeout} + isar_shrink_factor = isar_shrink_factor, timeout = timeout} val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs val {context = ctxt, facts, goal} = Proof.goal state val problem = @@ -95,20 +94,18 @@ (* Give the ATP some slack. The ATP gets further slack because the Sledgehammer preprocessing time is included in the estimate below but isn't part of the timeout. *) -val fudge_msecs = 250 +val fudge_msecs = 1000 fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set." | minimize_theorems (params as {debug, atps = atp :: _, full_types, isar_proof, - isar_shrink_factor, minimize_timeout, ...}) + isar_shrink_factor, timeout, ...}) i n state name_thms_pairs = let val thy = Proof.theory_of state val prover = get_prover_fun thy atp - val msecs = Time.toMilliseconds minimize_timeout - val _ = - priority ("Sledgehammer minimize: ATP " ^ quote atp ^ - " with a time limit of " ^ string_of_int msecs ^ " ms.") + val msecs = Time.toMilliseconds timeout + val _ = priority ("Sledgehammer minimize: ATP " ^ quote atp ^ ".") val {context = ctxt, goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i val explicit_apply = @@ -119,7 +116,7 @@ test_theorems params prover explicit_apply timeout i state val timer = Timer.startRealTimer () in - (case do_test minimize_timeout name_thms_pairs of + (case do_test timeout name_thms_pairs of result as {outcome = NONE, pool, used_thm_names, conjecture_shape, ...} => let diff -r b03f8fe043ec -r bd443b426d56 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 18 17:09:05 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 18 17:16:37 2010 +0200 @@ -73,8 +73,7 @@ ("theory_relevant", "smart"), ("defs_relevant", "false"), ("isar_proof", "false"), - ("isar_shrink_factor", "1"), - ("minimize_timeout", "5 s")] + ("isar_shrink_factor", "1")] val alias_params = [("atp", "atps")] @@ -90,7 +89,7 @@ val params_for_minimize = ["debug", "verbose", "overlord", "full_types", "isar_proof", - "isar_shrink_factor", "minimize_timeout"] + "isar_shrink_factor", "timeout"] val property_dependent_params = ["atps", "full_types", "timeout"] @@ -179,7 +178,6 @@ val isar_proof = lookup_bool "isar_proof" val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") val timeout = lookup_time "timeout" - val minimize_timeout = lookup_time "minimize_timeout" in {debug = debug, verbose = verbose, overlord = overlord, atps = atps, full_types = full_types, explicit_apply = explicit_apply, @@ -188,7 +186,7 @@ max_relevant_per_iter = max_relevant_per_iter, theory_relevant = theory_relevant, defs_relevant = defs_relevant, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, - timeout = timeout, minimize_timeout = minimize_timeout} + timeout = timeout} end fun get_params thy = extract_params (default_raw_params thy) @@ -207,9 +205,6 @@ val kill_atpsN = "kill_atps" val refresh_tptpN = "refresh_tptp" -fun minimizize_raw_param_name "timeout" = "minimize_timeout" - | minimizize_raw_param_name name = name - val is_raw_param_relevant_for_minimize = member (op =) params_for_minimize o fst o unalias_raw_param fun string_for_raw_param (key, values) = @@ -233,9 +228,8 @@ (minimize_command override_params i) state end else if subcommand = minimizeN then - run_minimize (get_params thy (map (apfst minimizize_raw_param_name) - override_params)) - (the_default 1 opt_i) (#add relevance_override) state + run_minimize (get_params thy override_params) (the_default 1 opt_i) + (#add relevance_override) state else if subcommand = messagesN then messages opt_i else if subcommand = available_atpsN then