# HG changeset patch # User blanchet # Date 1342815586 -7200 # Node ID 83dc102041e621a0f88d0e8c2d5951adf1db2eb7 # Parent df75b2d7e26ad14fcbf6c7780c4e0fbd3c804b59 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds diff -r df75b2d7e26a -r 83dc102041e6 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:46 2012 +0200 @@ -372,10 +372,16 @@ |> K () end else if subcommand = minN then - run_minimize (get_params Minimize ctxt - (("provers", [default_minimize_prover]) :: - override_params)) - (K ()) (the_default 1 opt_i) (#add fact_override) state + let + val i = the_default 1 opt_i + val params as {provers, ...} = + get_params Minimize ctxt (("provers", [default_minimize_prover]) :: + override_params) + val goal = prop_of (#goal (Proof.goal state)) + val facts = nearly_all_facts ctxt false fact_override Symtab.empty + Termtab.empty [] [] goal + val do_learn = mash_learn_proof ctxt params (hd provers) goal facts + in run_minimize params do_learn i (#add fact_override) state end else if subcommand = messagesN then messages opt_i else if subcommand = supported_proversN then @@ -389,7 +395,7 @@ else if subcommand = learnN orelse subcommand = relearnN then (if subcommand = relearnN then mash_unlearn ctxt else (); mash_learn ctxt (get_params Normal ctxt - (("verbose", ["true"]) :: override_params))) + (override_params @ [("verbose", ["true"])]))) else if subcommand = kill_learnersN then kill_learners () else if subcommand = running_learnersN then diff -r df75b2d7e26a -r 83dc102041e6 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200 @@ -54,7 +54,8 @@ Proof.context -> params -> string -> int -> term list -> term -> ('a * thm) list -> ('a * thm) list * ('a * thm) list val mash_learn_proof : - Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit + Proof.context -> params -> string -> term -> ('a * thm) list -> thm list + -> unit val mash_learn_thy : Proof.context -> params -> theory -> Time.time -> fact list -> string val mash_learn : Proof.context -> params -> unit @@ -547,31 +548,46 @@ val (deps, graph) = ([], graph) |> fold maybe_add_from deps in ((name, parents, feats, deps) :: upds, graph) end -val pass1_learn_timeout_factor = 0.5 +val learn_timeout_slack = 2.0 -fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths = +fun launch_thread timeout task = let - val thy = Proof_Context.theory_of ctxt - val prover = hd provers - val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *) - val feats = features_of ctxt prover thy General [t] - val deps = used_ths |> map nickname_of - in - mash_map ctxt (fn {thys, fact_graph} => - let - val parents = parents_wrt_facts facts fact_graph - val upds = [(name, parents, feats, deps)] - val (upds, fact_graph) = - ([], fact_graph) |> fold (update_fact_graph ctxt) upds - in - mash_ADD ctxt overlord upds; - {thys = thys, fact_graph = fact_graph} - end) - end + val hard_timeout = time_mult learn_timeout_slack timeout + val birth_time = Time.now () + val death_time = Time.+ (birth_time, hard_timeout) + val desc = ("machine learner for Sledgehammer", "") + in Async_Manager.launch MaShN birth_time death_time desc task end + +fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) prover t facts + used_ths = + if is_smt_prover ctxt prover then + () + else + launch_thread timeout + (fn () => + let + val thy = Proof_Context.theory_of ctxt + val name = timestamp () ^ " " ^ serial_string () (* freshish *) + val feats = features_of ctxt prover thy General [t] + val deps = used_ths |> map nickname_of + in + mash_map ctxt (fn {thys, fact_graph} => + let + val parents = parents_wrt_facts facts fact_graph + val upds = [(name, parents, feats, deps)] + val (upds, fact_graph) = + ([], fact_graph) |> fold (update_fact_graph ctxt) upds + in + mash_ADD ctxt overlord upds; + {thys = thys, fact_graph = fact_graph} + end); + (true, "") + end) (* Too many dependencies is a sign that a decision procedure is at work. There isn't much too learn from such proofs. *) val max_dependencies = 10 +val pass1_learn_timeout_factor = 0.75 (* The timeout is understood in a very slack fashion. *) fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy timeout @@ -647,7 +663,6 @@ (* The threshold should be large enough so that MaSh doesn't kick in for Auto Sledgehammer and Try. *) val min_secs_for_learning = 15 -val learn_timeout_factor = 2.0 fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts = @@ -661,19 +676,11 @@ let val thy = Proof_Context.theory_of ctxt fun maybe_learn () = - if not learn orelse Async_Manager.has_running_threads MaShN then - () - else if Time.toSeconds timeout >= min_secs_for_learning then - let - val soft_timeout = time_mult learn_timeout_factor timeout - val hard_timeout = time_mult 4.0 soft_timeout - val birth_time = Time.now () - val death_time = Time.+ (birth_time, hard_timeout) - val desc = ("machine learner for Sledgehammer", "") - in - Async_Manager.launch MaShN birth_time death_time desc - (fn () => - (true, mash_learn_thy ctxt params thy soft_timeout facts)) + if learn andalso not (Async_Manager.has_running_threads MaShN) andalso + Time.toSeconds timeout >= min_secs_for_learning then + let val timeout = time_mult learn_timeout_slack timeout in + launch_thread timeout + (fn () => (true, mash_learn_thy ctxt params thy timeout facts)) end else () diff -r df75b2d7e26a -r 83dc102041e6 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 20 22:19:46 2012 +0200 @@ -255,11 +255,11 @@ expect = expect} end -fun minimize ctxt mode do_learn name - (params as {debug, verbose, isar_proof, minimize, ...}) - ({state, subgoal, subgoal_count, facts, ...} : prover_problem) - (result as {outcome, used_facts, run_time, preplay, message, - message_tail} : prover_result) = +fun maybe_minimize ctxt mode do_learn name + (params as {debug, verbose, isar_proof, minimize, ...}) + ({state, subgoal, subgoal_count, facts, ...} : prover_problem) + (result as {outcome, used_facts, run_time, preplay, message, + message_tail} : prover_result) = if is_some outcome orelse null used_facts then result else @@ -328,7 +328,7 @@ fun get_minimizing_prover ctxt mode do_learn name params minimize_command problem = get_prover ctxt mode name params minimize_command problem - |> minimize ctxt mode do_learn name params problem + |> maybe_minimize ctxt mode do_learn name params problem fun run_minimize (params as {provers, ...}) do_learn i refs state = let diff -r df75b2d7e26a -r 83dc102041e6 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:46 2012 +0200 @@ -87,7 +87,7 @@ fun really_go () = problem |> get_minimizing_prover ctxt mode - (mash_learn_proof ctxt params (prop_of goal) + (mash_learn_proof ctxt params name (prop_of goal) (map untranslated_fact facts)) name params minimize_command |> (fn {outcome, preplay, message, message_tail, ...} =>