learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds

--- 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

--- 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
           ()

--- 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

--- 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, ...} =>