src/HOL/Tools/Sledgehammer/async_manager.ML
author blanchet
Tue, 15 Jul 2014 00:21:32 +0200
changeset 57556 6180d81be977
parent 56303 4cc3f4db3447
child 58843 521cea5fa777
permissions -rw-r--r--
tuned whitespace (also in strings)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41042
8275f52ac991 load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents: 40301
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/async_manager.ML
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
     2
    Author:     Fabian Immler, TU Muenchen
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
     3
    Author:     Makarius
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
     4
    Author:     Jasmin Blanchette, TU Muenchen
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
     5
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
     6
Central manager for asynchronous diagnosis tool threads.
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
     7
*)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
     8
53403
c09f4005d6bd some explicit indication of Proof General legacy;
wenzelm
parents: 52048
diff changeset
     9
(*Proof General legacy*)
c09f4005d6bd some explicit indication of Proof General legacy;
wenzelm
parents: 52048
diff changeset
    10
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    11
signature ASYNC_MANAGER =
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    12
sig
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
    13
  val break_into_chunks : string -> string list
57556
6180d81be977 tuned whitespace (also in strings)
blanchet
parents: 56303
diff changeset
    14
  val thread : string -> Time.time -> Time.time -> string * string -> (unit -> bool * string) ->
6180d81be977 tuned whitespace (also in strings)
blanchet
parents: 56303
diff changeset
    15
    unit
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    16
  val kill_threads : string -> string -> unit
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
    17
  val has_running_threads : string -> bool
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    18
  val running_threads : string -> string -> unit
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    19
  val thread_messages : string -> string -> int option -> unit
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    20
end;
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    21
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    22
structure Async_Manager : ASYNC_MANAGER =
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    23
struct
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    24
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
    25
val message_store_limit = 20
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
    26
val message_display_limit = 10
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    27
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
    28
fun implode_message (workers, work) =
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
    29
  space_implode " " (Try.serial_commas "and" workers) ^ work
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
    30
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    31
structure Thread_Heap = Heap
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    32
(
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
    33
  type elem = Time.time * Thread.thread
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
    34
  fun ord ((a, _), (b, _)) = Time.compare (a, b)
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
    35
)
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    36
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
    37
fun lookup_thread xs = AList.lookup Thread.equal xs
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
    38
fun delete_thread xs = AList.delete Thread.equal xs
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
    39
fun update_thread xs = AList.update Thread.equal xs
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    40
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    41
type state =
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    42
  {manager: Thread.thread option,
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    43
   timeout_heap: Thread_Heap.T,
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
    44
   active:
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
    45
     (Thread.thread
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
    46
      * (string * Time.time * Time.time * (string * string))) list,
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
    47
   canceling:  (Thread.thread * (string * Time.time * (string * string))) list,
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
    48
   messages: (bool * (string * (string * string))) list,
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
    49
   store: (string * (string * string)) list}
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    50
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    51
fun make_state manager timeout_heap active canceling messages store : state =
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    52
  {manager = manager, timeout_heap = timeout_heap, active = active,
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    53
   canceling = canceling, messages = messages, store = store}
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    54
57556
6180d81be977 tuned whitespace (also in strings)
blanchet
parents: 56303
diff changeset
    55
val global_state = Synchronized.var "async_manager" (make_state NONE Thread_Heap.empty [] [] [] [])
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    56
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
    57
fun unregister (urgent, message) thread =
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    58
  Synchronized.change global_state
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    59
  (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    60
    (case lookup_thread active thread of
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
    61
      SOME (tool, _, _, desc as (worker, its_desc)) =>
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    62
        let
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
    63
          val active' = delete_thread thread active
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    64
          val now = Time.now ()
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    65
          val canceling' = (thread, (tool, now, desc)) :: canceling
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
    66
          val message' =
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
    67
            (worker, its_desc ^ (if message = "" then "" else "\n" ^ message))
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
    68
          val messages' = (urgent, (tool, message')) :: messages
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    69
          val store' = (tool, message') ::
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    70
            (if length store <= message_store_limit then store
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
    71
             else #1 (chop message_store_limit store))
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    72
        in make_state manager timeout_heap active' canceling' messages' store' end
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
    73
    | NONE => state))
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    74
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
    75
val min_wait_time = seconds 0.3
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
    76
val max_wait_time = seconds 10.0
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    77
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    78
fun replace_all bef aft =
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    79
  let
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    80
    fun aux seen "" = String.implode (rev seen)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    81
      | aux seen s =
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    82
        if String.isPrefix bef s then
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    83
          aux seen "" ^ aft ^ aux [] (unprefix bef s)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    84
        else
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    85
          aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    86
  in aux [] end
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    87
57556
6180d81be977 tuned whitespace (also in strings)
blanchet
parents: 56303
diff changeset
    88
(* This is a workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in
6180d81be977 tuned whitespace (also in strings)
blanchet
parents: 56303
diff changeset
    89
   "proof" is not highlighted. *)
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
    90
val break_into_chunks = space_explode "\000" o replace_all "\n\n" "\000"
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    91
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    92
fun print_new_messages () =
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
    93
  Synchronized.change_result global_state
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
    94
      (fn {manager, timeout_heap, active, canceling, messages, store} =>
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
    95
          messages
43055
6e0cb8044734 better merging of similar outputs
blanchet
parents: 43029
diff changeset
    96
          |> List.partition
6e0cb8044734 better merging of similar outputs
blanchet
parents: 43029
diff changeset
    97
                 (fn (urgent, _) =>
6e0cb8044734 better merging of similar outputs
blanchet
parents: 43029
diff changeset
    98
                     (null active andalso null canceling) orelse urgent)
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
    99
          ||> (fn postponed_messages =>
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
   100
                  make_state manager timeout_heap active canceling
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
   101
                                     postponed_messages store))
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
   102
  |> map (fn (_, (tool, (worker, work))) => ((tool, work), worker))
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
   103
  |> AList.group (op =)
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   104
  |> List.app (fn ((_, ""), _) => ()
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   105
                | ((tool, work), workers) =>
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
   106
                  tool ^ ": " ^
47945
blanchet
parents: 47529
diff changeset
   107
                  implode_message (workers |> sort_distinct string_ord, work)
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
   108
                  |> break_into_chunks
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
   109
                  |> List.app Output.urgent_message)
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   110
39006
a02cb5717677 remove time information in output, since it's confusing anyway
blanchet
parents: 38990
diff changeset
   111
fun check_thread_manager () = Synchronized.change global_state
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   112
  (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   113
    if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 53403
diff changeset
   114
    else let val manager = SOME (Runtime.thread false (fn () =>
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   115
      let
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   116
        fun time_limit timeout_heap =
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   117
          (case try Thread_Heap.min timeout_heap of
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   118
            NONE => Time.+ (Time.now (), max_wait_time)
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   119
          | SOME (time, _) => time)
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   120
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   121
        (*action: find threads whose timeout is reached, and interrupt canceling threads*)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   122
        fun action {manager, timeout_heap, active, canceling, messages, store} =
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   123
          let val (timeout_threads, timeout_heap') =
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   124
            Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   125
          in
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   126
            if null timeout_threads andalso null canceling then
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   127
              NONE
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   128
            else
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   129
              let
44112
ef876972fdc1 more explicit Simple_Thread.interrupt_unsynchronized, to emphasize its meaning;
wenzelm
parents: 43055
diff changeset
   130
                val _ = List.app (Simple_Thread.interrupt_unsynchronized o #1) canceling
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   131
                val canceling' = filter (Thread.isActive o #1) canceling
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   132
                val state' = make_state manager timeout_heap' active canceling' messages store
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   133
              in SOME (map #2 timeout_threads, state') end
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   134
          end
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   135
      in
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   136
        while Synchronized.change_result global_state
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   137
          (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   138
            if null active andalso null canceling andalso null messages
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   139
            then (false, make_state NONE timeout_heap active canceling messages store)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   140
            else (true, state))
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   141
        do
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   142
          (Synchronized.timed_access global_state
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   143
               (SOME o time_limit o #timeout_heap) action
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   144
           |> these
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   145
           |> List.app (unregister (false, "Timed out."));
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   146
           print_new_messages ();
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   147
           (* give threads some time to respond to interrupt *)
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   148
           OS.Process.sleep min_wait_time)
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   149
      end))
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   150
    in make_state manager timeout_heap active canceling messages store end)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   151
39006
a02cb5717677 remove time information in output, since it's confusing anyway
blanchet
parents: 38990
diff changeset
   152
fun register tool birth_time death_time desc thread =
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   153
 (Synchronized.change global_state
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   154
    (fn {manager, timeout_heap, active, canceling, messages, store} =>
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   155
      let
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   156
        val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   157
        val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   158
        val state' = make_state manager timeout_heap' active' canceling messages store
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   159
      in state' end);
39006
a02cb5717677 remove time information in output, since it's confusing anyway
blanchet
parents: 38990
diff changeset
   160
  check_thread_manager ())
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   161
52048
9003b293e775 tuned signature -- emphasize thread creation here;
wenzelm
parents: 48319
diff changeset
   162
fun thread tool birth_time death_time desc f =
56303
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents: 53403
diff changeset
   163
  (Runtime.thread true
37584
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   164
       (fn () =>
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   165
           let
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   166
             val self = Thread.self ()
39006
a02cb5717677 remove time information in output, since it's confusing anyway
blanchet
parents: 38990
diff changeset
   167
             val _ = register tool birth_time death_time desc self
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
   168
           in unregister (f ()) self end);
37584
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   169
   ())
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   170
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
   171
fun kill_threads tool das_wort_worker = Synchronized.change global_state
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   172
  (fn {manager, timeout_heap, active, canceling, messages, store} =>
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   173
    let
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   174
      val killing =
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   175
        map_filter (fn (th, (tool', _, _, desc)) =>
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   176
                       if tool' = tool then SOME (th, (tool', Time.now (), desc))
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   177
                       else NONE) active
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   178
      val state' = make_state manager timeout_heap [] (killing @ canceling) messages store
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
   179
      val _ =
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
   180
        if null killing then ()
45573
22d003b5b32e less offensive terminology
blanchet
parents: 44112
diff changeset
   181
        else Output.urgent_message ("Interrupted active " ^ das_wort_worker ^ "s.")
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   182
    in state' end)
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   183
57556
6180d81be977 tuned whitespace (also in strings)
blanchet
parents: 56303
diff changeset
   184
fun str_of_time time = string_of_int (Time.toSeconds time) ^ " s"
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   185
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   186
fun has_running_threads tool =
57556
6180d81be977 tuned whitespace (also in strings)
blanchet
parents: 56303
diff changeset
   187
  exists (fn (_, (tool', _, _, _)) => tool' = tool) (#active (Synchronized.value global_state))
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   188
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
   189
fun running_threads tool das_wort_worker =
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   190
  let
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   191
    val {active, canceling, ...} = Synchronized.value global_state
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   192
    val now = Time.now ()
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   193
    fun running_info (_, (tool', birth_time, death_time, desc)) =
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   194
      if tool' = tool then
57556
6180d81be977 tuned whitespace (also in strings)
blanchet
parents: 56303
diff changeset
   195
        SOME ("Running: " ^ str_of_time (Time.- (now, birth_time)) ^ " -- " ^
6180d81be977 tuned whitespace (also in strings)
blanchet
parents: 56303
diff changeset
   196
              str_of_time (Time.- (death_time, now)) ^ " to live:\n" ^ op ^ desc)
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   197
      else
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   198
        NONE
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   199
    fun canceling_info (_, (tool', death_time, desc)) =
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   200
      if tool' = tool then
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
   201
        SOME ("Trying to interrupt " ^ das_wort_worker ^ " since " ^
57556
6180d81be977 tuned whitespace (also in strings)
blanchet
parents: 56303
diff changeset
   202
              str_of_time (Time.- (now, death_time)) ^ ":\n" ^ op ^ desc)
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   203
      else
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   204
        NONE
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   205
    val running =
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   206
      case map_filter running_info active of
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
   207
        [] => ["No " ^ das_wort_worker ^ "s running."]
57556
6180d81be977 tuned whitespace (also in strings)
blanchet
parents: 56303
diff changeset
   208
      | ss => "Running " ^ das_wort_worker ^ "s" :: ss
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   209
    val interrupting =
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   210
      case map_filter canceling_info canceling of
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   211
        [] => []
57556
6180d81be977 tuned whitespace (also in strings)
blanchet
parents: 56303
diff changeset
   212
      | ss => "Interrupting " ^ das_wort_worker ^ "s" :: ss
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 39376
diff changeset
   213
  in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   214
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
   215
fun thread_messages tool das_wort_worker opt_limit =
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   216
  let
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   217
    val limit = the_default message_display_limit opt_limit
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   218
    val tool_store = Synchronized.value global_state
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   219
                     |> #store |> filter (curry (op =) tool o fst)
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   220
    val header =
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
   221
      "Recent " ^ das_wort_worker ^ " messages" ^
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   222
        (if length tool_store <= limit then ":"
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   223
         else " (" ^ string_of_int limit ^ " displayed):")
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 47945
diff changeset
   224
    val ss = tool_store |> chop limit |> #1 |> map (op ^ o snd)
43005
c96f06bffd90 merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents: 41042
diff changeset
   225
  in List.app Output.urgent_message (header :: maps break_into_chunks ss) end
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   226
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   227
end;