1.1 --- a/src/HOL/Tools/Sledgehammer/async_manager.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -8,12 +8,12 @@
     1.4  
     1.5  signature ASYNC_MANAGER =
     1.6  sig
     1.7 -  val implode_desc : string * string -> string
     1.8    val break_into_chunks : string -> string list
     1.9    val launch :
    1.10      string -> Time.time -> Time.time -> string * string
    1.11      -> (unit -> bool * string) -> unit
    1.12    val kill_threads : string -> string -> unit
    1.13 +  val has_running_threads : string -> bool
    1.14    val running_threads : string -> string -> unit
    1.15    val thread_messages : string -> string -> int option -> unit
    1.16  end;
    1.17 @@ -23,29 +23,27 @@
    1.18  
    1.19  (** preferences **)
    1.20  
    1.21 -val message_store_limit = 20;
    1.22 -val message_display_limit = 10;
    1.23 +val message_store_limit = 20
    1.24 +val message_display_limit = 10
    1.25  
    1.26  
    1.27  (** thread management **)
    1.28  
    1.29 -val implode_desc = op ^ o apfst quote
    1.30 -
    1.31  fun implode_message (workers, work) =
    1.32 -  space_implode " " (Try.serial_commas "and" (map quote workers)) ^ work
    1.33 +  space_implode " " (Try.serial_commas "and" workers) ^ work
    1.34  
    1.35  
    1.36  (* data structures over threads *)
    1.37  
    1.38  structure Thread_Heap = Heap
    1.39  (
    1.40 -  type elem = Time.time * Thread.thread;
    1.41 -  fun ord ((a, _), (b, _)) = Time.compare (a, b);
    1.42 -);
    1.43 +  type elem = Time.time * Thread.thread
    1.44 +  fun ord ((a, _), (b, _)) = Time.compare (a, b)
    1.45 +)
    1.46  
    1.47 -fun lookup_thread xs = AList.lookup Thread.equal xs;
    1.48 -fun delete_thread xs = AList.delete Thread.equal xs;
    1.49 -fun update_thread xs = AList.update Thread.equal xs;
    1.50 +fun lookup_thread xs = AList.lookup Thread.equal xs
    1.51 +fun delete_thread xs = AList.delete Thread.equal xs
    1.52 +fun update_thread xs = AList.update Thread.equal xs
    1.53  
    1.54  
    1.55  (* state of thread manager *)
    1.56 @@ -65,7 +63,7 @@
    1.57     canceling = canceling, messages = messages, store = store}
    1.58  
    1.59  val global_state = Synchronized.var "async_manager"
    1.60 -  (make_state NONE Thread_Heap.empty [] [] [] []);
    1.61 +  (make_state NONE Thread_Heap.empty [] [] [] [])
    1.62  
    1.63  
    1.64  (* unregister thread *)
    1.65 @@ -76,22 +74,23 @@
    1.66      (case lookup_thread active thread of
    1.67        SOME (tool, _, _, desc as (worker, its_desc)) =>
    1.68          let
    1.69 -          val active' = delete_thread thread active;
    1.70 +          val active' = delete_thread thread active
    1.71            val now = Time.now ()
    1.72            val canceling' = (thread, (tool, now, desc)) :: canceling
    1.73 -          val message' = (worker, its_desc ^ "\n" ^ message)
    1.74 +          val message' =
    1.75 +            (worker, its_desc ^ (if message = "" then "" else "\n" ^ message))
    1.76            val messages' = (urgent, (tool, message')) :: messages
    1.77            val store' = (tool, message') ::
    1.78              (if length store <= message_store_limit then store
    1.79 -             else #1 (chop message_store_limit store));
    1.80 +             else #1 (chop message_store_limit store))
    1.81          in make_state manager timeout_heap active' canceling' messages' store' end
    1.82 -    | NONE => state));
    1.83 +    | NONE => state))
    1.84  
    1.85  
    1.86  (* main manager thread -- only one may exist *)
    1.87  
    1.88 -val min_wait_time = seconds 0.3;
    1.89 -val max_wait_time = seconds 10.0;
    1.90 +val min_wait_time = seconds 0.3
    1.91 +val max_wait_time = seconds 10.0
    1.92  
    1.93  fun replace_all bef aft =
    1.94    let
    1.95 @@ -119,7 +118,8 @@
    1.96                                       postponed_messages store))
    1.97    |> map (fn (_, (tool, (worker, work))) => ((tool, work), worker))
    1.98    |> AList.group (op =)
    1.99 -  |> List.app (fn ((tool, work), workers) =>
   1.100 +  |> List.app (fn ((_, ""), _) => ()
   1.101 +                | ((tool, work), workers) =>
   1.102                    tool ^ ": " ^
   1.103                    implode_message (workers |> sort_distinct string_ord, work)
   1.104                    |> break_into_chunks
   1.105 @@ -133,12 +133,12 @@
   1.106          fun time_limit timeout_heap =
   1.107            (case try Thread_Heap.min timeout_heap of
   1.108              NONE => Time.+ (Time.now (), max_wait_time)
   1.109 -          | SOME (time, _) => time);
   1.110 +          | SOME (time, _) => time)
   1.111  
   1.112          (*action: find threads whose timeout is reached, and interrupt canceling threads*)
   1.113          fun action {manager, timeout_heap, active, canceling, messages, store} =
   1.114            let val (timeout_threads, timeout_heap') =
   1.115 -            Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
   1.116 +            Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap
   1.117            in
   1.118              if null timeout_threads andalso null canceling then
   1.119                NONE
   1.120 @@ -146,9 +146,9 @@
   1.121                let
   1.122                  val _ = List.app (Simple_Thread.interrupt_unsynchronized o #1) canceling
   1.123                  val canceling' = filter (Thread.isActive o #1) canceling
   1.124 -                val state' = make_state manager timeout_heap' active canceling' messages store;
   1.125 +                val state' = make_state manager timeout_heap' active canceling' messages store
   1.126                in SOME (map #2 timeout_threads, state') end
   1.127 -          end;
   1.128 +          end
   1.129        in
   1.130          while Synchronized.change_result global_state
   1.131            (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
   1.132 @@ -156,12 +156,13 @@
   1.133              then (false, make_state NONE timeout_heap active canceling messages store)
   1.134              else (true, state))
   1.135          do
   1.136 -          (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
   1.137 -            |> these
   1.138 -            |> List.app (unregister (false, "Timed out."));
   1.139 -            print_new_messages ();
   1.140 -            (*give threads some time to respond to interrupt*)
   1.141 -            OS.Process.sleep min_wait_time)
   1.142 +          (Synchronized.timed_access global_state
   1.143 +               (SOME o time_limit o #timeout_heap) action
   1.144 +           |> these
   1.145 +           |> List.app (unregister (false, "Timed out."));
   1.146 +           print_new_messages ();
   1.147 +           (* give threads some time to respond to interrupt *)
   1.148 +           OS.Process.sleep min_wait_time)
   1.149        end))
   1.150      in make_state manager timeout_heap active canceling messages store end)
   1.151  
   1.152 @@ -172,9 +173,9 @@
   1.153   (Synchronized.change global_state
   1.154      (fn {manager, timeout_heap, active, canceling, messages, store} =>
   1.155        let
   1.156 -        val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
   1.157 -        val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
   1.158 -        val state' = make_state manager timeout_heap' active' canceling messages store;
   1.159 +        val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap
   1.160 +        val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active
   1.161 +        val state' = make_state manager timeout_heap' active' canceling messages store
   1.162        in state' end);
   1.163    check_thread_manager ())
   1.164  
   1.165 @@ -200,33 +201,36 @@
   1.166          map_filter (fn (th, (tool', _, _, desc)) =>
   1.167                         if tool' = tool then SOME (th, (tool', Time.now (), desc))
   1.168                         else NONE) active
   1.169 -      val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
   1.170 +      val state' = make_state manager timeout_heap [] (killing @ canceling) messages store
   1.171        val _ =
   1.172          if null killing then ()
   1.173          else Output.urgent_message ("Interrupted active " ^ das_wort_worker ^ "s.")
   1.174 -    in state' end);
   1.175 +    in state' end)
   1.176  
   1.177  
   1.178  (* running threads *)
   1.179  
   1.180  fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
   1.181  
   1.182 +fun has_running_threads tool =
   1.183 +  exists (fn (_, (tool', _, _, _)) => tool' = tool)
   1.184 +         (#active (Synchronized.value global_state))
   1.185 +
   1.186  fun running_threads tool das_wort_worker =
   1.187    let
   1.188 -    val {active, canceling, ...} = Synchronized.value global_state;
   1.189 -
   1.190 -    val now = Time.now ();
   1.191 +    val {active, canceling, ...} = Synchronized.value global_state
   1.192 +    val now = Time.now ()
   1.193      fun running_info (_, (tool', birth_time, death_time, desc)) =
   1.194        if tool' = tool then
   1.195          SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
   1.196                seconds (Time.- (death_time, now)) ^ " to live:\n" ^
   1.197 -              implode_desc desc)
   1.198 +              op ^ desc)
   1.199        else
   1.200          NONE
   1.201      fun canceling_info (_, (tool', death_time, desc)) =
   1.202        if tool' = tool then
   1.203          SOME ("Trying to interrupt " ^ das_wort_worker ^ " since " ^
   1.204 -              seconds (Time.- (now, death_time)) ^ ":\n" ^ implode_desc desc)
   1.205 +              seconds (Time.- (now, death_time)) ^ ":\n" ^ op ^ desc)
   1.206        else
   1.207          NONE
   1.208      val running =
   1.209 @@ -241,14 +245,14 @@
   1.210  
   1.211  fun thread_messages tool das_wort_worker opt_limit =
   1.212    let
   1.213 -    val limit = the_default message_display_limit opt_limit;
   1.214 +    val limit = the_default message_display_limit opt_limit
   1.215      val tool_store = Synchronized.value global_state
   1.216                       |> #store |> filter (curry (op =) tool o fst)
   1.217      val header =
   1.218        "Recent " ^ das_wort_worker ^ " messages" ^
   1.219          (if length tool_store <= limit then ":"
   1.220 -         else " (" ^ string_of_int limit ^ " displayed):");
   1.221 -    val ss = tool_store |> chop limit |> #1 |> map (implode_desc o snd)
   1.222 +         else " (" ^ string_of_int limit ^ " displayed):")
   1.223 +    val ss = tool_store |> chop limit |> #1 |> map (op ^ o snd)
   1.224    in List.app Output.urgent_message (header :: maps break_into_chunks ss) end
   1.225  
   1.226  end;

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     2.3 @@ -15,6 +15,7 @@
     2.4    type prover_result = Sledgehammer_Provers.prover_result
     2.5  
     2.6    val trace : bool Config.T
     2.7 +  val MaShN : string
     2.8    val meshN : string
     2.9    val iterN : string
    2.10    val mashN : string
    2.11 @@ -51,12 +52,15 @@
    2.12    val mash_suggest_facts :
    2.13      Proof.context -> params -> string -> int -> term list -> term -> fact list
    2.14      -> fact list
    2.15 -  val mash_learn_thy : Proof.context -> params -> theory -> Time.time -> unit
    2.16 +  val mash_learn_thy :
    2.17 +    Proof.context -> params -> theory -> Time.time -> fact list -> string
    2.18    val mash_learn_proof :
    2.19      Proof.context -> params -> term -> thm list -> fact list -> unit
    2.20    val relevant_facts :
    2.21      Proof.context -> params -> string -> int -> fact_override -> term list
    2.22      -> term -> fact list -> fact list
    2.23 +  val kill_learners : unit -> unit
    2.24 +  val running_learners : unit -> unit
    2.25  end;
    2.26  
    2.27  structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
    2.28 @@ -74,6 +78,8 @@
    2.29    Attrib.setup_config_bool @{binding sledgehammer_filter_mash_trace} (K false)
    2.30  fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    2.31  
    2.32 +val MaShN = "MaSh"
    2.33 +
    2.34  val meshN = "mesh"
    2.35  val iterN = "iter"
    2.36  val mashN = "mash"
    2.37 @@ -481,8 +487,6 @@
    2.38    let
    2.39      val thy = Proof_Context.theory_of ctxt
    2.40      val fact_graph = #fact_graph (mash_get ())
    2.41 -val _ = warning (PolyML.makestring (length (fact_graph |> Graph.keys), length (fact_graph |> Graph.maximals),
    2.42 -length (fact_graph |> Graph.minimals))) (*###*)
    2.43      val parents = parents_wrt_facts facts fact_graph
    2.44      val feats = features_of ctxt prover thy General (concl_t :: hyp_ts)
    2.45      val suggs =
    2.46 @@ -509,34 +513,23 @@
    2.47    in ((name, parents, feats, deps) :: upds, graph) end
    2.48  
    2.49  val pass1_learn_timeout_factor = 0.5
    2.50 -val pass2_learn_timeout_factor = 10.0
    2.51  
    2.52  (* The timeout is understood in a very slack fashion. *)
    2.53 -fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy
    2.54 -                   timeout =
    2.55 +fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy timeout
    2.56 +                   facts =
    2.57    let
    2.58      val timer = Timer.startRealTimer ()
    2.59      val prover = hd provers
    2.60      fun timed_out frac =
    2.61        Time.> (Timer.checkRealTimer timer, time_mult frac timeout)
    2.62 -    val css_table = clasimpset_rule_table_of ctxt
    2.63 -    val facts = all_facts_of thy css_table
    2.64      val {fact_graph, ...} = mash_get ()
    2.65      fun is_old (_, th) = can (Graph.get_node fact_graph) (Thm.get_name_hint th)
    2.66      val new_facts = facts |> filter_out is_old |> sort (thm_ord o pairself snd)
    2.67    in
    2.68      if null new_facts then
    2.69 -      ()
    2.70 +      ""
    2.71      else
    2.72        let
    2.73 -        val n = length new_facts
    2.74 -        val _ =
    2.75 -          if verbose then
    2.76 -            "MaShing " ^ string_of_int n ^ " fact" ^ plural_s n ^
    2.77 -            " (advisory timeout: " ^ string_from_time timeout ^ ")..."
    2.78 -            |> Output.urgent_message
    2.79 -          else
    2.80 -            ()
    2.81          val ths = facts |> map snd
    2.82          val all_names =
    2.83            ths |> filter_out (is_likely_tautology ctxt prover orf is_too_meta)
    2.84 @@ -566,22 +559,15 @@
    2.85                fact_graph = fact_graph})
    2.86            end
    2.87        in
    2.88 -        TimeLimit.timeLimit (time_mult pass2_learn_timeout_factor timeout)
    2.89 -                            mash_map trans
    2.90 -        handle TimeLimit.TimeOut =>
    2.91 -               (if verbose then
    2.92 -                  "MaSh timed out trying to learn " ^ string_of_int n ^
    2.93 -                  " fact" ^ plural_s n ^ " in " ^
    2.94 -                  string_from_time (Timer.checkRealTimer timer) ^ "."
    2.95 -                  |> Output.urgent_message
    2.96 -                else
    2.97 -                  ());
    2.98 -        (if verbose then
    2.99 -           "MaSh learned " ^ string_of_int n ^ " fact" ^ plural_s n ^ " in " ^
   2.100 -           string_from_time (Timer.checkRealTimer timer) ^ "."
   2.101 -           |> Output.urgent_message
   2.102 -         else
   2.103 -           ())
   2.104 +        mash_map trans;
   2.105 +        if verbose then
   2.106 +          "Processed " ^ string_of_int n ^ " proof" ^ plural_s n ^
   2.107 +          (if verbose then
   2.108 +             " in " ^ string_from_time (Timer.checkRealTimer timer)
   2.109 +           else
   2.110 +             "") ^ "."
   2.111 +        else
   2.112 +          ""
   2.113        end
   2.114    end
   2.115  
   2.116 @@ -623,19 +609,23 @@
   2.117      let
   2.118        val thy = Proof_Context.theory_of ctxt
   2.119        fun maybe_learn can_suggest =
   2.120 -        if Time.toSeconds timeout >= min_secs_for_learning then
   2.121 -          if Multithreading.enabled () then
   2.122 -            let
   2.123 -              val factor =
   2.124 -                if can_suggest then short_learn_timeout_factor
   2.125 -                else long_learn_timeout_factor
   2.126 -            in
   2.127 -              Future.fork (fn () => mash_learn_thy ctxt params thy
   2.128 -                                        (time_mult factor timeout)); ()
   2.129 -            end
   2.130 -          else
   2.131 -            mash_learn_thy ctxt params thy
   2.132 -                           (time_mult short_learn_timeout_factor timeout)
   2.133 +        if Async_Manager.has_running_threads MaShN orelse null facts then
   2.134 +          ()
   2.135 +        else if Time.toSeconds timeout >= min_secs_for_learning then
   2.136 +          let
   2.137 +            val factor =
   2.138 +              if can_suggest then short_learn_timeout_factor
   2.139 +              else long_learn_timeout_factor
   2.140 +            val soft_timeout = time_mult factor timeout
   2.141 +            val hard_timeout = time_mult 2.0 soft_timeout
   2.142 +            val birth_time = Time.now ()
   2.143 +            val death_time = Time.+ (birth_time, hard_timeout)
   2.144 +            val desc = ("machine learner for Sledgehammer", "")
   2.145 +          in
   2.146 +            Async_Manager.launch MaShN birth_time death_time desc
   2.147 +                (fn () =>
   2.148 +                    (true, mash_learn_thy ctxt params thy soft_timeout facts))
   2.149 +          end
   2.150          else
   2.151            ()
   2.152        val fact_filter =
   2.153 @@ -667,4 +657,7 @@
   2.154        |> not (null add_ths) ? prepend_facts add_ths
   2.155      end
   2.156  
   2.157 +fun kill_learners () = Async_Manager.kill_threads MaShN "learner"
   2.158 +fun running_learners () = Async_Manager.running_threads MaShN "learner"
   2.159 +
   2.160  end;

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:04 2012 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:04 2012 +0200
     3.3 @@ -33,10 +33,12 @@
     3.4  val minN = "min"
     3.5  val messagesN = "messages"
     3.6  val supported_proversN = "supported_provers"
     3.7 +val kill_proversN = "kill_provers"
     3.8  val running_proversN = "running_provers"
     3.9 -val kill_proversN = "kill_provers"
    3.10 +val kill_learnersN = "kill_learners"
    3.11 +val running_learnersN = "running_learners"
    3.12 +val unlearnN = "unlearn"
    3.13  val refresh_tptpN = "refresh_tptp"
    3.14 -val reset_mashN = "reset_mash"
    3.15  
    3.16  val auto = Unsynchronized.ref false
    3.17  
    3.18 @@ -374,14 +376,18 @@
    3.19        messages opt_i
    3.20      else if subcommand = supported_proversN then
    3.21        supported_provers ctxt
    3.22 +    else if subcommand = kill_proversN then
    3.23 +      kill_provers ()
    3.24      else if subcommand = running_proversN then
    3.25        running_provers ()
    3.26 -    else if subcommand = kill_proversN then
    3.27 -      kill_provers ()
    3.28 +    else if subcommand = kill_learnersN then
    3.29 +      kill_learners ()
    3.30 +    else if subcommand = running_learnersN then
    3.31 +      running_learners ()
    3.32 +    else if subcommand = unlearnN then
    3.33 +      mash_reset ctxt
    3.34      else if subcommand = refresh_tptpN then
    3.35        refresh_systems_on_tptp ()
    3.36 -    else if subcommand = reset_mashN then
    3.37 -      mash_reset ctxt
    3.38      else
    3.39        error ("Unknown subcommand: " ^ quote subcommand ^ ".")
    3.40    end

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 18 08:44:04 2012 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 18 08:44:04 2012 +0200
     4.3 @@ -99,7 +99,7 @@
     4.4    val smt_slice_fact_frac : real Config.T
     4.5    val smt_slice_time_frac : real Config.T
     4.6    val smt_slice_min_secs : int Config.T
     4.7 -  val das_tool : string
     4.8 +  val SledgehammerN : string
     4.9    val plain_metis : reconstructor
    4.10    val select_smt_solver : string -> Proof.context -> Proof.context
    4.11    val extract_reconstructor :
    4.12 @@ -153,7 +153,7 @@
    4.13  
    4.14  (* Identifier that distinguishes Sledgehammer from other tools that could use
    4.15     "Async_Manager". *)
    4.16 -val das_tool = "Sledgehammer"
    4.17 +val SledgehammerN = "Sledgehammer"
    4.18  
    4.19  val reconstructor_names = [metisN, smtN]
    4.20  val plain_metis = Metis (hd partial_type_encs, combsN)
    4.21 @@ -298,9 +298,9 @@
    4.22                             commas (local_provers @ remote_provers) ^ ".")
    4.23    end
    4.24  
    4.25 -fun kill_provers () = Async_Manager.kill_threads das_tool "prover"
    4.26 -fun running_provers () = Async_Manager.running_threads das_tool "prover"
    4.27 -val messages = Async_Manager.thread_messages das_tool "prover"
    4.28 +fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
    4.29 +fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
    4.30 +val messages = Async_Manager.thread_messages SledgehammerN "prover"
    4.31  
    4.32  
    4.33  (** problems, results, ATPs, etc. **)

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 18 08:44:04 2012 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 18 08:44:04 2012 +0200
     5.3 @@ -53,7 +53,7 @@
     5.4  
     5.5  fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
     5.6                         n goal =
     5.7 -  (name,
     5.8 +  (quote name,
     5.9     (if verbose then
    5.10        " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
    5.11      else
    5.12 @@ -141,7 +141,7 @@
    5.13          (outcome_code, state)
    5.14        end
    5.15      else
    5.16 -      (Async_Manager.launch das_tool birth_time death_time (desc ())
    5.17 +      (Async_Manager.launch SledgehammerN birth_time death_time (desc ())
    5.18                              ((fn (outcome_code, message) =>
    5.19                                   (verbose orelse outcome_code = someN,
    5.20                                    message ())) o go);