# HG changeset patch # User bulwahn # Date 1311142601 -7200 # Node ID ef347714c5c119a9666f4ffba704183c29bed31d # Parent 64819f353c5336ef8ef48997040c8be836fbb1a5 removing inner time limits in quickcheck diff -r 64819f353c53 -r ef347714c5c1 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Jul 20 08:16:39 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Jul 20 08:16:41 2011 +0200 @@ -285,9 +285,9 @@ end in with_size 0 end in - Quickcheck.limit timeout (limit_time, is_interactive) - (fn () => with_tmp_dir tmp_prefix run) - (fn () => (message (excipit ()); (NONE, !current_result))) () + (*Quickcheck.limit timeout (limit_time, is_interactive) + (fn () =>*) with_tmp_dir tmp_prefix run + (*(fn () => (message (excipit ()); (NONE, !current_result))) ()*) end; fun dynamic_value_strict opts cookie thy postproc t = diff -r 64819f353c53 -r ef347714c5c1 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Wed Jul 20 08:16:39 2011 +0200 +++ b/src/Tools/quickcheck.ML Wed Jul 20 08:16:41 2011 +0200 @@ -319,7 +319,7 @@ case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q end; in - limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () => + (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)( let val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => compile ctxt [(t, eval_terms)]); @@ -329,7 +329,7 @@ val _ = add_response names eval_terms response current_result val _ = add_timing exec_time current_result in !current_result end) - (fn () => (message (excipit ()); !current_result)) () +(* (fn () => (message (excipit ()); !current_result)) ()*) end; fun validate_terms ctxt ts = @@ -399,7 +399,7 @@ map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt size)) |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2))) in - limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () => + (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)( let val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => compile ctxt ts) val _ = add_timing comp_time current_result @@ -407,7 +407,7 @@ SOME (card, ts) => add_response names (nth eval_terms (card - 1)) (SOME ts) current_result | NONE => () in !current_result end) - (fn () => (message "Quickcheck ran out of time"; !current_result)) () + (*(fn () => (message "Quickcheck ran out of time"; !current_result)) ()*) end fun get_finite_types ctxt = @@ -490,14 +490,18 @@ collect_results (test_term compile ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) [] end; + +fun message ctxt s = if Config.get ctxt quiet then () else Output.urgent_message s fun test_goal_terms ctxt (limit_time, is_interactive) insts goals = case active_testers ctxt of [] => error "No active testers for quickcheck" - | testers => testers |> Par_List.get_some (fn tester => + | testers => limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) + (fn () => Par_List.get_some (fn tester => tester ctxt (limit_time, is_interactive) insts goals |> - (fn result => if exists found_counterexample result then SOME result else NONE)) - + (fn result => if exists found_counterexample result then SOME result else NONE)) testers) + (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) (); + fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state = let val lthy = Proof.context_of state;