# HG changeset patch # User blanchet # Date 1291369389 -3600 # Node ID 5cd8464dccbbab45ac9e9a7a6711c5e92f47b95a # Parent 500171e7aa59099e3588a45dc67e7f4ffd30b79d# Parent b9f56b4025d29aa3ce56ee8f673540326995f606 merged diff -r 500171e7aa59 -r 5cd8464dccbb src/HOL/Mutabelle/MutabelleExtra.thy --- a/src/HOL/Mutabelle/MutabelleExtra.thy Fri Dec 03 10:17:55 2010 +0100 +++ b/src/HOL/Mutabelle/MutabelleExtra.thy Fri Dec 03 10:43:09 2010 +0100 @@ -26,7 +26,7 @@ nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12] refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat] *) -ML {* Auto_Tools.time_limit := 10 *} +ML {* Auto_Tools.time_limit := 10.0 *} ML {* val mtds = [ MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random", diff -r 500171e7aa59 -r 5cd8464dccbb src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Dec 03 10:17:55 2010 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Dec 03 10:43:09 2010 +0100 @@ -114,13 +114,14 @@ (** quickcheck **) fun invoke_quickcheck change_options quickcheck_generator thy t = - TimeLimit.timeLimit (Time.fromSeconds (!Auto_Tools.time_limit)) + TimeLimit.timeLimit (seconds (!Auto_Tools.time_limit)) (fn _ => case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy)) false [] [t] of (NONE, _) => (NoCex, ([], NONE)) | (SOME _, _) => (GenuineCex, ([], NONE))) () - handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Tools.time_limit)], NONE)) + handle TimeLimit.TimeOut => + (Timeout, ([("timelimit", Real.floor (!Auto_Tools.time_limit))], NONE)) fun quickcheck_mtd change_options quickcheck_generator = ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator) diff -r 500171e7aa59 -r 5cd8464dccbb src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Dec 03 10:17:55 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Dec 03 10:43:09 2010 +0100 @@ -383,9 +383,8 @@ "set and display the default parameters for Nitpick" Keyword.thy_decl parse_nitpick_params_command -fun auto_nitpick state = - if not (!auto) then (false, state) else pick_nits [] true 1 0 state +val auto_nitpick = pick_nits [] true 1 0 -val setup = Auto_Tools.register_tool ("nitpick", auto_nitpick) +val setup = Auto_Tools.register_tool (auto, auto_nitpick) end; diff -r 500171e7aa59 -r 5cd8464dccbb src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Dec 03 10:17:55 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Dec 03 10:43:09 2010 +0100 @@ -347,14 +347,11 @@ parse_sledgehammer_params_command fun auto_sledgehammer state = - if not (!auto) then - (false, state) - else - let val ctxt = Proof.context_of state in - run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override - (minimize_command [] 1) state - end + let val ctxt = Proof.context_of state in + run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override + (minimize_command [] 1) state + end -val setup = Auto_Tools.register_tool (sledgehammerN, auto_sledgehammer) +val setup = Auto_Tools.register_tool (auto, auto_sledgehammer) end; diff -r 500171e7aa59 -r 5cd8464dccbb src/HOL/Tools/try.ML --- a/src/HOL/Tools/try.ML Fri Dec 03 10:17:55 2010 +0100 +++ b/src/HOL/Tools/try.ML Fri Dec 03 10:43:09 2010 +0100 @@ -110,8 +110,8 @@ (Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout) o Toplevel.proof_of))) -fun auto_try st = if not (!auto) then (false, st) else do_try true NONE st +val auto_try = do_try true NONE -val setup = Auto_Tools.register_tool (tryN, auto_try) +val setup = Auto_Tools.register_tool (auto, auto_try) end; diff -r 500171e7aa59 -r 5cd8464dccbb src/Tools/auto_tools.ML --- a/src/Tools/auto_tools.ML Fri Dec 03 10:17:55 2010 +0100 +++ b/src/Tools/auto_tools.ML Fri Dec 03 10:43:09 2010 +0100 @@ -6,10 +6,11 @@ signature AUTO_TOOLS = sig - val time_limit: int Unsynchronized.ref + val time_limit: real Unsynchronized.ref val register_tool : - string * (Proof.state -> bool * Proof.state) -> theory -> theory + bool Unsynchronized.ref * (Proof.state -> bool * Proof.state) -> theory + -> theory end; structure Auto_Tools : AUTO_TOOLS = @@ -17,20 +18,20 @@ (* preferences *) -val time_limit = Unsynchronized.ref 4000 +val time_limit = Unsynchronized.ref 4.0 +val auto_tools_time_limitN = "auto-tools-time-limit" val _ = ProofGeneralPgip.add_preference Preferences.category_tracing - (Preferences.nat_pref time_limit - "auto-tools-time-limit" - "Time limit for automatic tools (in milliseconds).") + (Preferences.real_pref time_limit + auto_tools_time_limitN "Time limit for automatic tools (in seconds).") (* configuration *) structure Data = Theory_Data ( - type T = (string * (Proof.state -> bool * Proof.state)) list + type T = (bool Unsynchronized.ref * (Proof.state -> bool * Proof.state)) list val empty = [] val extend = I fun merge data : T = AList.merge (op =) (K true) data @@ -41,18 +42,30 @@ (* automatic testing *) +fun run_tools tools state = + tools |> map_filter (fn (auto, tool) => if !auto then SOME tool else NONE) + |> Par_List.get_some (fn tool => + case try tool state of + SOME (true, state) => SOME state + | _ => NONE) + |> the_default state + +(* Too large values are understood as milliseconds, ensuring compatibility with + old setting files. No users can possibly in their right mind want the user + interface to block for more than 100 seconds. *) +fun smart_seconds r = + seconds (if r >= 100.0 then + (legacy_feature (quote auto_tools_time_limitN ^ + " expressed in milliseconds -- use seconds instead"); 0.001 * r) + else + r) + val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state => - case !time_limit of - 0 => state - | ms => - TimeLimit.timeLimit (Time.fromMilliseconds ms) - (fn () => - if interact andalso not (!Toplevel.quiet) then - fold_rev (fn (_, tool) => fn (true, state) => (true, state) - | (false, state) => tool state) - (Data.get (Proof.theory_of state)) (false, state) |> snd - else - state) () - handle TimeLimit.TimeOut => state)) + if interact andalso not (!Toplevel.quiet) andalso !time_limit > 0.0 then + TimeLimit.timeLimit (smart_seconds (!time_limit)) + (run_tools (Data.get (Proof.theory_of state))) state + handle TimeLimit.TimeOut => state + else + state)) end; diff -r 500171e7aa59 -r 5cd8464dccbb src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Fri Dec 03 10:17:55 2010 +0100 +++ b/src/Tools/quickcheck.ML Fri Dec 03 10:43:09 2010 +0100 @@ -303,24 +303,21 @@ (* automatic testing *) fun auto_quickcheck state = - if not (!auto) then - (false, state) - else - let - val ctxt = Proof.context_of state; - val res = - state - |> Proof.map_context (Config.put report false #> Config.put quiet true) - |> try (test_goal [] 1); - in - case res of - NONE => (false, state) - | SOME (NONE, report) => (false, state) - | SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "", - Pretty.mark Markup.hilite (pretty_counterex ctxt true cex)])) state) - end + let + val ctxt = Proof.context_of state; + val res = + state + |> Proof.map_context (Config.put report false #> Config.put quiet true) + |> try (test_goal [] 1); + in + case res of + NONE => (false, state) + | SOME (NONE, report) => (false, state) + | SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "", + Pretty.mark Markup.hilite (pretty_counterex ctxt true cex)])) state) + end -val setup = Auto_Tools.register_tool ("quickcheck", auto_quickcheck) +val setup = Auto_Tools.register_tool (auto, auto_quickcheck) #> setup_config (* Isar commands *) diff -r 500171e7aa59 -r 5cd8464dccbb src/Tools/solve_direct.ML --- a/src/Tools/solve_direct.ML Fri Dec 03 10:17:55 2010 +0100 +++ b/src/Tools/solve_direct.ML Fri Dec 03 10:43:09 2010 +0100 @@ -97,9 +97,8 @@ (* hook *) -fun auto_solve_direct state = - if not (! auto) then (false, state) else solve_direct true state; +val auto_solve_direct = solve_direct true -val setup = Auto_Tools.register_tool (solve_directN, auto_solve_direct); +val setup = Auto_Tools.register_tool (auto, auto_solve_direct); end;