# HG changeset patch # User boehmes # Date 1253515531 -7200 # Node ID 35094c8fd8bff6a595644f624fafdd8475621810 # Parent bfbdeddc03bc9cfd2f36dc783c95df793dcb3764# Parent 02f45a09a9f2d376e7427029fc516c9e910ae8f9 merged diff -r 02f45a09a9f2 -r 35094c8fd8bf src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Sep 21 08:34:56 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Sep 21 08:45:31 2009 +0200 @@ -38,9 +38,9 @@ } datatype min_data = MinData of { - calls: int, - ratios: int, - lemmas: int + succs: int, + ab_ratios: int, + it_ratios: int } (* The first me_data component is only used if "minimize" is on. @@ -52,8 +52,8 @@ ShData{calls=calls, success=success, lemmas=lemmas, time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail} -fun make_min_data (calls, ratios, lemmas) = - MinData{calls=calls, ratios=ratios, lemmas=lemmas} +fun make_min_data (succs, ab_ratios, it_ratios) = + MinData{succs=succs, ab_ratios=ab_ratios, it_ratios=it_ratios} fun make_me_data (calls, success, time, timeout, lemmas, posns) = MeData{calls=calls, success=success, time=time, timeout=timeout, lemmas=lemmas, posns=posns} @@ -61,7 +61,7 @@ val empty_data = Data(make_sh_data (0, 0, 0, 0, 0, 0), make_me_data(0, 0, 0, 0, 0, []), - MinData{calls=0, ratios=0, lemmas=0}, + MinData{succs=0, ab_ratios=0, it_ratios=0}, make_me_data(0, 0, 0, 0, 0, [])) fun map_sh_data f @@ -70,8 +70,8 @@ meda0, minda, meda) fun map_min_data f - (Data(shda, meda0, MinData{calls,ratios,lemmas}, meda)) = - Data(shda, meda0, make_min_data(f(calls,ratios,lemmas)), meda) + (Data(shda, meda0, MinData{succs,ab_ratios,it_ratios}, meda)) = + Data(shda, meda0, make_min_data(f(succs,ab_ratios,it_ratios)), meda) fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout,lemmas,posns}, minda, meda)) = Data(shda, make_me_data(f (calls,success,time,timeout,lemmas,posns)), minda, meda) @@ -103,11 +103,14 @@ map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail) => (calls, success, lemmas, time_isa, time_atp, time_atp_fail + t)) -val inc_min_calls = - map_min_data (fn (calls, ratios, lemmas) => (calls + 1, ratios, lemmas)) +val inc_min_succs = + map_min_data (fn (succs,ab_ratios,it_ratios) => (succs+1, ab_ratios, it_ratios)) -fun inc_min_ratios n = - map_min_data (fn (calls, ratios, lemmas) => (calls, ratios + n, lemmas)) +fun inc_min_ab_ratios r = + map_min_data (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios+r, it_ratios)) + +fun inc_min_it_ratios r = + map_min_data (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r)) val inc_metis_calls = map_me_data (fn (calls, success, time, timeout, lemmas,posns) @@ -202,9 +205,10 @@ else () ) -fun log_min_data log calls ratios = - (log ("Number of minimizations: " ^ string_of_int calls); - log ("Minimization ratios: " ^ string_of_int ratios) +fun log_min_data log succs ab_ratios it_ratios = + (log ("Number of successful minimizations: " ^ string_of_int succs); + log ("After/before ratios: " ^ string_of_int ab_ratios); + log ("Iterations ratios: " ^ string_of_int it_ratios) ) in @@ -215,7 +219,7 @@ MeData{calls=metis_calls0, success=metis_success0, time=metis_time0, timeout=metis_timeout0, lemmas=metis_lemmas0,posns=metis_posns0}, - MinData{calls=min_calls, ratios=min_ratios, lemmas=min_lemmas}, + MinData{succs=min_succs, ab_ratios=ab_ratios, it_ratios=it_ratios}, MeData{calls=metis_calls, success=metis_success, time=metis_time, timeout=metis_timeout, lemmas=metis_lemmas,posns=metis_posns})) = @@ -228,7 +232,7 @@ metis_success metis_time metis_timeout metis_lemmas metis_posns else (); log ""; if metis_calls0 > 0 - then (log_min_data log min_calls min_ratios; log ""; + then (log_min_data log min_succs ab_ratios it_ratios; log ""; log_metis_data log "unminimized " sh_calls sh_success metis_calls0 metis_success0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0) else () @@ -360,8 +364,9 @@ in case minimize timeout st (these (!named_thms)) of (SOME (named_thms',its), msg) => - (change_data id inc_min_calls; - change_data id (inc_min_ratios ((100*its) div n0)); + (change_data id inc_min_succs; + change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0)); + change_data id (inc_min_it_ratios ((100*its) div n0)); if length named_thms' = n0 then log (minimize_tag id ^ "already minimal") else (named_thms := SOME named_thms'; @@ -405,20 +410,20 @@ val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_time0, inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0) val named_thms = ref (NONE : (string * thm list) list option) - - fun if_enabled k f = - if AList.defined (op =) args k andalso is_some (!named_thms) - then f id st else () - - val _ = Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st - val _ = if_enabled minimizeK - (Mirabelle.catch metis_tag (run_metis metis0_fns args (these (!named_thms)))) - val _ = if_enabled minimizeK - (Mirabelle.catch minimize_tag (run_minimize args named_thms)) - val _ = if is_some (!named_thms) - then Mirabelle.catch metis_tag (run_metis metis_fns args (these (!named_thms))) id st - else () - in () end + val minimize = AList.defined (op =) args minimizeK + in + Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st; + if is_some (!named_thms) + then + (if minimize + then Mirabelle.catch metis_tag (run_metis metis0_fns args (these (!named_thms))) id st + else (); + if minimize andalso not(null(these(!named_thms))) + then Mirabelle.catch minimize_tag (run_minimize args named_thms) id st + else (); + Mirabelle.catch metis_tag (run_metis metis_fns args (these (!named_thms))) id st) + else () + end fun invoke args = let diff -r 02f45a09a9f2 -r 35094c8fd8bf src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Mon Sep 21 08:34:56 2009 +0200 +++ b/src/HOL/Tools/inductive.ML Mon Sep 21 08:45:31 2009 +0200 @@ -103,6 +103,7 @@ "(P & True) = P" "(True & P) = P" by (fact simp_thms)+}; +val simp_thms'' = inf_fun_eq :: inf_bool_eq :: simp_thms'; (** context data **) @@ -559,7 +560,7 @@ [rewrite_goals_tac [inductive_conj_def], DETERM (rtac raw_fp_induct 1), REPEAT (resolve_tac [le_funI, le_boolI] 1), - rewrite_goals_tac (inf_fun_eq :: inf_bool_eq :: simp_thms'), + rewrite_goals_tac simp_thms'', (*This disjE separates out the introduction rules*) REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])), (*Now break down the individual cases. No disjE here in case @@ -568,7 +569,7 @@ REPEAT (FIRSTGOAL (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))), EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule - (inductive_conj_def :: rec_preds_defs @ simp_thms') prem, + (inductive_conj_def :: rec_preds_defs @ simp_thms'') prem, conjI, refl] 1)) prems)]); val lemma = SkipProof.prove ctxt'' [] [] diff -r 02f45a09a9f2 -r 35094c8fd8bf src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Mon Sep 21 08:34:56 2009 +0200 +++ b/src/HOL/ex/ROOT.ML Mon Sep 21 08:45:31 2009 +0200 @@ -68,8 +68,7 @@ "Landau" ]; -Future.shutdown (); -(setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy)) +(setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy)) "Hilbert_Classical"; use_thy "SVC_Oracle"; diff -r 02f45a09a9f2 -r 35094c8fd8bf src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Mon Sep 21 08:34:56 2009 +0200 +++ b/src/Pure/Concurrent/future.ML Mon Sep 21 08:45:31 2009 +0200 @@ -237,7 +237,7 @@ val total = length (! workers); val active = count_active (); in - "SCHEDULE " ^ string_of_int (Time.toMilliseconds now) ^ ": " ^ + "SCHEDULE " ^ Time.toString now ^ ": " ^ string_of_int ready ^ " ready, " ^ string_of_int pending ^ " pending, " ^ string_of_int running ^ " running; " ^ @@ -257,7 +257,7 @@ "SCHEDULE: disposed " ^ string_of_int (length dead) ^ " dead worker threads"))); val m = if ! do_shutdown then 0 else Multithreading.max_threads_value (); - val mm = (m * 3) div 2; + val mm = if m = 9999 then 1 else (m * 3) div 2; val l = length (! workers); val _ = excessive := l - mm; val _ = diff -r 02f45a09a9f2 -r 35094c8fd8bf src/Pure/Concurrent/par_list.ML --- a/src/Pure/Concurrent/par_list.ML Mon Sep 21 08:34:56 2009 +0200 +++ b/src/Pure/Concurrent/par_list.ML Mon Sep 21 08:45:31 2009 +0200 @@ -27,8 +27,10 @@ struct fun raw_map f xs = - let val group = Task_Queue.new_group (Future.worker_group ()) - in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end; + if Multithreading.enabled () then + let val group = Task_Queue.new_group (Future.worker_group ()) + in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end + else map (Exn.capture f) xs; fun map f xs = Exn.release_first (raw_map f xs);