--- 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",
--- 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)
--- 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;
--- 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;
--- 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;
--- 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;
--- 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 *)
--- 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;