# HG changeset patch # User blanchet # Date 1377205401 -7200 # Node ID c898409d8630990627fea0f193ed47af4d6e142e # Parent 8e8941fea27836e02bfbe383c15a58d7400aa4ee fixed subtle bug with "take" + thread overlord through diff -r 8e8941fea278 -r c898409d8630 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 22 21:15:43 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 22 23:03:21 2013 +0200 @@ -404,15 +404,16 @@ else if subcommand = supported_proversN then supported_provers ctxt else if subcommand = kill_allN then - (kill_provers (); kill_learners ctxt) + (kill_provers (); + kill_learners ctxt (get_params Normal ctxt override_params)) else if subcommand = running_proversN then running_provers () else if subcommand = unlearnN then - mash_unlearn ctxt + mash_unlearn ctxt (get_params Normal ctxt override_params) else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse subcommand = relearn_isarN orelse subcommand = relearn_proverN then (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then - mash_unlearn ctxt + mash_unlearn ctxt (get_params Normal ctxt override_params) else (); mash_learn ctxt diff -r 8e8941fea278 -r c898409d8630 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Aug 22 21:15:43 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Aug 22 23:03:21 2013 +0200 @@ -36,7 +36,7 @@ structure MaSh: sig - val unlearn : Proof.context -> unit + val unlearn : Proof.context -> bool -> unit val learn : Proof.context -> bool -> (string * string list * string list * string list) list -> unit @@ -49,7 +49,7 @@ -> string list end - val mash_unlearn : Proof.context -> unit + val mash_unlearn : Proof.context -> params -> unit val nickname_of_thm : thm -> string val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list @@ -90,14 +90,14 @@ val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit val is_mash_enabled : unit -> bool - val mash_can_suggest_facts : Proof.context -> bool + val mash_can_suggest_facts : Proof.context -> bool -> bool val generous_max_facts : int -> int val mepo_weight : real val mash_weight : real val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list -> term -> raw_fact list -> (string * fact list) list - val kill_learners : Proof.context -> unit + val kill_learners : Proof.context -> params -> unit val running_learners : unit -> unit end; @@ -253,13 +253,13 @@ structure MaSh = struct -fun shutdown ctxt = - run_mash_tool ctxt false [shutdown_server_arg] ([], K "") (K ()) +fun shutdown ctxt overlord = + run_mash_tool ctxt overlord [shutdown_server_arg] ([], K "") (K ()) -fun unlearn ctxt = +fun unlearn ctxt overlord = let val path = mash_model_dir () in trace_msg ctxt (K "MaSh unlearn"); - shutdown ctxt; + shutdown ctxt overlord; try (File.fold_dir (fn file => fn _ => try File.rm (Path.append path (Path.basic file))) path) NONE; @@ -359,8 +359,8 @@ | _ => NONE) | _ => NONE -fun load _ (state as (true, _)) = state - | load ctxt _ = +fun load _ _ (state as (true, _)) = state + | load ctxt overlord _ = let val path = mash_state_file () in (true, case try File.read_lines path of @@ -383,7 +383,7 @@ length node_lines) | LESS => (* can't parse old file *) - (MaSh.unlearn ctxt; (Graph.empty, 0)) + (MaSh.unlearn ctxt overlord; (Graph.empty, 0)) | GREATER => raise FILE_VERSION_TOO_NEW () in trace_msg ctxt (fn () => @@ -423,22 +423,22 @@ in -fun map_state ctxt f = - Synchronized.change global_state (load ctxt ##> (f #> save ctxt)) +fun map_state ctxt overlord f = + Synchronized.change global_state (load ctxt overlord ##> (f #> save ctxt)) handle FILE_VERSION_TOO_NEW () => () -fun peek_state ctxt f = +fun peek_state ctxt overlord f = Synchronized.change_result global_state - (perhaps (try (load ctxt)) #> `snd #>> f) + (perhaps (try (load ctxt overlord)) #> `snd #>> f) -fun clear_state ctxt = +fun clear_state ctxt overlord = Synchronized.change global_state (fn _ => - (MaSh.unlearn ctxt; (* also removes the state file *) + (MaSh.unlearn ctxt overlord; (* also removes the state file *) (false, empty_state))) end -val mash_unlearn = clear_state +fun mash_unlearn ctxt ({overlord, ...} : params) = clear_state ctxt overlord (*** Isabelle helpers ***) @@ -589,7 +589,7 @@ fun maybe_singleton_str _ "" = [] | maybe_singleton_str pref s = [pref ^ s] -val max_pat_breadth = 10 +val max_pat_breadth = 10 (* FUDGE *) fun term_features_of ctxt prover thy_name num_facts const_tab term_max_depth type_max_depth ts = @@ -641,7 +641,7 @@ 0.0 else let val count = Symtab.lookup const_tab s |> the_default 1 in - (Real.fromInt num_facts / Real.fromInt count) (* FUDGE *) + Real.fromInt num_facts / Real.fromInt count (* FUDGE *) end) fun pattify_term _ _ 0 _ = [] | pattify_term _ args _ (Const (x as (s, _))) = @@ -906,7 +906,7 @@ val chained_feature_factor = 0.5 val extra_feature_factor = 0.1 -val num_extra_feature_facts = 10 (* FUDGE *) +val num_extra_feature_facts = 0 (* FUDGE *) (* FUDGE *) fun weight_of_proximity_fact rank = @@ -958,7 +958,7 @@ |> features_of ctxt prover (theory_of_thm th) num_facts const_tab stature |> map (apsnd (fn r => weight * factor * r)) val (access_G, suggs) = - peek_state ctxt (fn {access_G, ...} => + peek_state ctxt overlord (fn {access_G, ...} => if Graph.is_empty access_G then (access_G, []) else @@ -974,7 +974,7 @@ |> rpair [] |-> fold (union (op = o pairself fst)) val extra_feats = facts - |> take (num_extra_feature_facts - length chained) + |> take (Int.max (0, num_extra_feature_facts - length chained)) |> weight_facts_steeply |> map (chained_or_extra_features_of extra_feature_factor) |> rpair [] |-> fold (union (op = o pairself fst)) @@ -1036,7 +1036,7 @@ features_of ctxt prover thy 0 Symtab.empty (Local, General) [t] |> map fst in - peek_state ctxt (fn {access_G, ...} => + peek_state ctxt overlord (fn {access_G, ...} => let val parents = maximal_wrt_access_graph access_G facts val deps = @@ -1060,7 +1060,7 @@ val timer = Timer.startRealTimer () fun next_commit_time () = Time.+ (Timer.checkRealTimer timer, commit_timeout) - val {access_G, ...} = peek_state ctxt I + val {access_G, ...} = peek_state ctxt overlord I val is_in_access_G = is_fact_in_graph access_G o snd val no_new_facts = forall is_in_access_G facts in @@ -1114,7 +1114,7 @@ Output.urgent_message "Committing..." else (); - map_state ctxt (do_commit (rev learns) relearns flops); + map_state ctxt overlord (do_commit (rev learns) relearns flops); if not last andalso auto_level = 0 then let val num_proofs = length learns + length relearns in "Learned " ^ string_of_int num_proofs ^ " " ^ @@ -1250,8 +1250,8 @@ end fun is_mash_enabled () = (getenv "MASH" = "yes") -fun mash_can_suggest_facts ctxt = - not (Graph.is_empty (#access_G (peek_state ctxt I))) +fun mash_can_suggest_facts ctxt overlord = + not (Graph.is_empty (#access_G (peek_state ctxt overlord I))) (* Generate more suggestions than requested, because some might be thrown out later for various reasons. *) @@ -1264,8 +1264,9 @@ Sledgehammer and Try. *) val min_secs_for_learning = 15 -fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover - max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts = +fun relevant_facts ctxt (params as {overlord, learn, fact_filter, timeout, ...}) + prover max_facts ({add, only, ...} : fact_override) hyp_ts concl_t + facts = if not (subset (op =) (the_list fact_filter, fact_filters)) then error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".") else if only then @@ -1295,7 +1296,7 @@ | NONE => if is_mash_enabled () then (maybe_learn (); - if mash_can_suggest_facts ctxt then meshN else mepoN) + if mash_can_suggest_facts ctxt overlord then meshN else mepoN) else mepoN val add_ths = Attrib.eval_thms ctxt add @@ -1335,8 +1336,8 @@ | _ => [("", mesh)] end -fun kill_learners ctxt = - (Async_Manager.kill_threads MaShN "learner"; MaSh.shutdown ctxt) +fun kill_learners ctxt ({overlord, ...} : params) = + (Async_Manager.kill_threads MaShN "learner"; MaSh.shutdown ctxt overlord) fun running_learners () = Async_Manager.running_threads MaShN "learner" end;