STM + CoqIDE: stop_worker message and UI

11 files changed, 87 insertions, 23 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index c8ba8549b..fe17c20a4 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -509,6 +509,7 @@ let status ?logger force = eval_call ?logger (Serialize.status force)
 let hints x = eval_call (Serialize.hints x)
 let search flags = eval_call (Serialize.search flags)
 let init x = eval_call (Serialize.init x)
+let stop_worker x = eval_call (Serialize.stop_worker x)
 
 module PrintOpt =
 struct
diff --git a/ide/coq.mli b/ide/coq.mli
index f6f92a9a9..0b246b842 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -131,6 +131,8 @@ val mkcases    : Interface.mkcases_sty    -> Interface.mkcases_rty query
 val search     : Interface.search_sty     -> Interface.search_rty query
 val init       : Interface.init_sty       -> Interface.init_rty query
 
+val stop_worker: Interface.stop_worker_sty-> Interface.stop_worker_rty query
+
 (** A specialized version of [raw_interp] dedicated to set/unset options. *)
 
 module PrintOpt :
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 347459a65..a43a7989a 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -121,6 +121,7 @@ object
   method backtrack_last_phrase : unit task
   method initialize : unit task
   method join_document : unit task
+  method stop_worker : int -> unit task
 
   method get_n_errors : int
   method get_errors : (int * string) list
@@ -544,6 +545,9 @@ object(self)
      | Fail x -> self#handle_failure x in
    Coq.bind (Coq.status ~logger:messages#push true) next
 
+  method stop_worker n =
+    Coq.bind (Coq.stop_worker n) (fun _ -> Coq.return ())
+
   method get_slaves_status = processed, to_process, slaves_status
 
   method get_n_errors =
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index cde6f3d00..4669f016d 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -21,6 +21,7 @@ object
   method backtrack_last_phrase : unit task
   method initialize : unit task
   method join_document : unit task
+  method stop_worker : int -> unit task
 
   method get_n_errors : int
   method get_errors : (int * string) list
diff --git a/ide/coqide.ml b/ide/coqide.ml
index ab832b4e4..0f2102727 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -517,12 +517,12 @@ let find_next_occurrence ~backward sn =
     |None -> ()
     |Some(where, _) -> b#place_cursor ~where; sn.script#recenter_insert
 
-let send_to_coq f sn =
+let send_to_coq_aux f sn =
   let info () = Minilib.log ("Coq busy, discarding query") in
   let f = Coq.seq (f sn) (update_status sn) in
   Coq.try_grab sn.coqtop f info
 
-let send_to_coq f = on_current_term (send_to_coq f)
+let send_to_coq f = on_current_term (send_to_coq_aux f)
 
 module Nav = struct
   let forward_one _ = send_to_coq (fun sn -> sn.coqops#process_next_phrase)
@@ -1312,7 +1312,13 @@ let build_ui () =
     let table_jobs, access_jobs =
       make_table_widget
         [`Int,"Worker",true; `String,"Job name",true; `Int,"Tab no",false]
-        (fun columns store tp vc -> ()) in
+        (fun columns store tp vc -> 
+          let row = store#get_iter tp in
+          let w = store#get ~row ~column:(int_assoc "Worker" columns) in
+          let tabno = store#get ~row ~column:(int_assoc "Tab no" columns) in
+          let sn = notebook#get_nth_term tabno in
+          send_to_coq_aux (fun sn -> sn.coqops#stop_worker w) sn
+        ) in
     let tip = GMisc.label ~text:"Double click to jump to error line" () in
     let nb = GPack.notebook ~packing:obj#add () in
     let vb = GPack.vbox ~homogeneous:false () in
@@ -1321,7 +1327,11 @@ let build_ui () =
     let add_page text w =
       nb#append_page ~tab_label:(GMisc.label ~text ())#coerce w#coerce in
     let _ = add_page "Errors" vb in
-    let _ = add_page "Workers" table_jobs in
+    let vb = GPack.vbox ~homogeneous:false () in
+    let tip = GMisc.label ~text:"Double click to interrupt worker" () in
+    let () = vb#pack ~expand:true table_jobs#coerce in
+    let () = vb#pack ~expand:false ~padding:2 tip#coerce in
+    let _ = add_page "Workers" vb in
     obj, (let last_update = ref (0,[],Int.Map.empty) in
           fun tabno errs jobs ->
             if !last_update = (tabno,errs,jobs) then ()
diff --git a/lib/interface.mli b/lib/interface.mli
index da09593ba..a089eb574 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -241,6 +241,9 @@ type interp_sty = (raw * verbose) * string
 (* spiwack: [Inl] for safe and [Inr] for unsafe. *)
 type interp_rty = state_id * (string,string) Util.union
 
+type stop_worker_sty = int
+type stop_worker_rty = unit
+
 
 type handler = {
   add         : add_sty         -> add_rty;
@@ -256,6 +259,7 @@ type handler = {
   inloadpath  : inloadpath_sty  -> inloadpath_rty;
   mkcases     : mkcases_sty     -> mkcases_rty;
   about       : about_sty       -> about_rty;
+  stop_worker : stop_worker_sty -> stop_worker_rty;
   handle_exn  : handle_exn_sty  -> handle_exn_rty;
   init        : init_sty        -> init_rty;
   quit        : quit_sty        -> quit_rty;
diff --git a/lib/serialize.ml b/lib/serialize.ml
index cfaa40fce..92dcca2c5 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -636,6 +636,7 @@ let quit_sty_t : quit_sty val_t = unit_t
 let about_sty_t : about_sty val_t = unit_t
 let init_sty_t : init_sty val_t = unit_t
 let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t
+let stop_worker_sty_t : stop_worker_sty val_t = int_t
 
 let add_rty_t : add_rty val_t =
   pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t)
@@ -658,6 +659,7 @@ let quit_rty_t : quit_rty val_t = unit_t
 let about_rty_t : about_rty val_t = coq_info_t
 let init_rty_t : init_rty val_t = state_id_t
 let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string_t)
+let stop_worker_rty_t : stop_worker_rty val_t = unit_t
 
 let ($) x = erase x
 let calls = [|  
@@ -677,6 +679,7 @@ let calls = [|
   "About",      ($)about_sty_t,       ($)about_rty_t;
   "Init",       ($)init_sty_t,        ($)init_rty_t;
   "Interp",     ($)interp_sty_t,      ($)interp_rty_t;
+  "StopWorker", ($)stop_worker_sty_t, ($)stop_worker_rty_t;
 |]
 
 type 'a call =
@@ -695,6 +698,7 @@ type 'a call =
   | Quit       of quit_sty
   | About      of about_sty
   | Init       of init_sty
+  | StopWorker of stop_worker_sty
   (* retrocompatibility *)
   | Interp     of interp_sty
 
@@ -715,6 +719,7 @@ let id_of_call = function
   | About _      -> 13
   | Init _       -> 14
   | Interp _     -> 15
+  | StopWorker _ -> 16
 
 let str_of_call c = pi1 calls.(id_of_call c)
 
@@ -736,6 +741,7 @@ let search x      : search_rty call      = Search x
 let quit x        : quit_rty call        = Quit x
 let init x        : init_rty call        = Init x
 let interp x      : interp_rty call      = Interp x
+let stop_worker x : stop_worker_rty call = StopWorker x
 
 let abstract_eval_call handler (c : 'a call) : 'a value =
   let mkGood x : 'a value = Good (Obj.magic x) in
@@ -757,6 +763,7 @@ let abstract_eval_call handler (c : 'a call) : 'a value =
     | About x      -> mkGood (handler.about x)
     | Init x       -> mkGood (handler.init x)
     | Interp x     -> mkGood (handler.interp x)
+    | StopWorker x -> mkGood (handler.stop_worker x)
   with any ->
     Fail (handler.handle_exn any)
 
@@ -778,6 +785,7 @@ let of_answer (q : 'a call) (v : 'a value) : xml = match q with
   | About _      -> of_value (of_value_type about_rty_t      ) (Obj.magic v)
   | Init _       -> of_value (of_value_type init_rty_t       ) (Obj.magic v)
   | Interp _     -> of_value (of_value_type interp_rty_t     ) (Obj.magic v)
+  | StopWorker _ -> of_value (of_value_type stop_worker_rty_t) (Obj.magic v)
 
 let to_answer (q : 'a call) (x : xml) : 'a value = match q with
   | Add _        -> Obj.magic (to_value (to_value_type add_rty_t        ) x)
@@ -796,6 +804,7 @@ let to_answer (q : 'a call) (x : xml) : 'a value = match q with
   | About _      -> Obj.magic (to_value (to_value_type about_rty_t      ) x)
   | Init _       -> Obj.magic (to_value (to_value_type init_rty_t       ) x)
   | Interp _     -> Obj.magic (to_value (to_value_type interp_rty_t     ) x)
+  | StopWorker _ -> Obj.magic (to_value (to_value_type stop_worker_rty_t) x)
 
 let of_call (q : 'a call) : xml =
   let mkCall x = constructor "call" (str_of_call q) [x] in
@@ -816,6 +825,7 @@ let of_call (q : 'a call) : xml =
   | About x      -> mkCall (of_value_type about_sty_t       x) 
   | Init x       -> mkCall (of_value_type init_sty_t        x)
   | Interp x     -> mkCall (of_value_type interp_sty_t      x)
+  | StopWorker x -> mkCall (of_value_type stop_worker_sty_t x)
 
 let to_call : xml -> unknown call =
   do_match "call" (fun s a ->
@@ -837,6 +847,7 @@ let to_call : xml -> unknown call =
     | "About"      -> About      (mkCallArg about_sty_t       a)
     | "Init"       -> Init       (mkCallArg init_sty_t        a)
     | "Interp"     -> Interp     (mkCallArg interp_sty_t      a)
+    | "StopWorker" -> StopWorker (mkCallArg stop_worker_sty_t a)
     | _ -> raise Marshal_error)
 (* }}} *)
 
@@ -872,6 +883,7 @@ let pr_full_value call value = match call with
   | About _      -> pr_value_gen (print about_rty_t      ) (Obj.magic value) 
   | Init _       -> pr_value_gen (print init_rty_t       ) (Obj.magic value)
   | Interp _     -> pr_value_gen (print interp_rty_t     ) (Obj.magic value)
+  | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) (Obj.magic value)
 let pr_call call = match call with
   | Add x        -> str_of_call call ^ " " ^ print add_sty_t         x
   | Edit_at x    -> str_of_call call ^ " " ^ print edit_at_sty_t     x
@@ -889,6 +901,7 @@ let pr_call call = match call with
   | About x      -> str_of_call call ^ " " ^ print about_sty_t       x
   | Init x       -> str_of_call call ^ " " ^ print init_sty_t        x
   | Interp x     -> str_of_call call ^ " " ^ print interp_sty_t      x
+  | StopWorker x -> str_of_call call ^ " " ^ print stop_worker_sty_t x
 
 (* }}} *)
 
diff --git a/lib/serialize.mli b/lib/serialize.mli
index 4e5cb2d15..db92dc9ea 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -29,6 +29,7 @@ val get_options : get_options_sty -> get_options_rty call
 val set_options : set_options_sty -> set_options_rty call
 val quit        : quit_sty        -> quit_rty call
 val init        : init_sty        -> init_rty call
+val stop_worker : stop_worker_sty -> stop_worker_rty call
 (* retrocompatibility *)
 val interp      : interp_sty      -> interp_rty call
 
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index af58f8eb2..70410fc40 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -354,8 +354,9 @@ let eval_call xml_oc log c =
     Interface.init = interruptible init;
     Interface.about = interruptible about;
     Interface.interp = interruptible interp;
-    Interface.handle_exn = handle_exn; }
-  in
+    Interface.handle_exn = handle_exn;
+    Interface.stop_worker = Stm.stop_worker;
+  } in
   Serialize.abstract_eval_call handler c
 
 (** Message dispatching.
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 927cd0b81..ed420ebbe 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -639,6 +639,8 @@ module Slaves : sig
   val check_task : string -> tasks -> int -> bool
   val info_tasks : tasks -> (string * float * int) list
 
+  val cancel_worker : int -> unit
+
 end = struct (* {{{ *)
 
   module TQueue : sig
@@ -695,9 +697,11 @@ end = struct (* {{{ *)
 
   module SlavesPool : sig
   
-    val init : int -> ((unit -> in_channel * out_channel * Worker.process * int) -> unit) -> unit
+    val init : int -> (bool ref -> (unit -> in_channel * out_channel * Worker.process * int) -> unit) -> unit
     val is_empty : unit -> bool
     val n_slaves : unit -> int
+
+    val cancel : int -> unit
   
   end = struct (* {{{ *)
   
@@ -739,10 +743,22 @@ end = struct (* {{{ *)
 
     let init n manage_slave =
       slave_managers := Some
-        (Array.init n (fun x -> Thread.create manage_slave (respawn (x+1))));
+        (Array.init n (fun x ->
+           let calcel_req = ref false in
+           calcel_req,
+           Thread.create (manage_slave calcel_req) (respawn (x+1))))
+
+    let cancel n =
+      match !slave_managers with
+      | None -> ()
+      | Some a ->
+          let switch, _ = a.(n) in
+          switch := true
 
   end (* }}} *)
-  
+ 
+  let cancel_worker n = SlavesPool.cancel (n-1)
+
   let reach_known_state = ref (fun ?redefine_qed ~cache id -> ())
   let set_reach_known_state f = reach_known_state := f
 
@@ -894,10 +910,10 @@ end = struct (* {{{ *)
       marshal_err ("marshal_response: "^s)
   
   let unmarshal_response ic =
-    try (Marshal.from_channel ic : response)
+    try (CThread.thread_friendly_input_value ic : response)
     with Failure s | Invalid_argument s | Sys_error s ->
       marshal_err ("unmarshal_response: "^s)
-  
+
   let marshal_more_data oc (res : more_data) =
     try marshal_to_channel oc res
     with Failure s | Invalid_argument s | Sys_error s ->
@@ -951,10 +967,12 @@ end = struct (* {{{ *)
           | _ -> assert false in
     Pp.feedback ~state_id:Stateid.initial (Interface.SlaveStatus(id, s))
 
-  let rec manage_slave respawn =
+  let rec manage_slave cancel_user_req respawn =
     let ic, oc, proc, id_slave = respawn () in
     let last_task = ref None in
-    let cancelled = ref false in
+    let task_expired = ref false in
+    let task_cancelled = ref false in
+    CThread.prepare_in_channel_for_thread_friendly_io ic;
     try
       while true do
         prerr_endline "waiting for a task";
@@ -966,7 +984,10 @@ end = struct (* {{{ *)
           marshal_request oc (request_of_task task);
           let cancel_switch = cancel_switch_of_task task in
           Worker.kill_if proc ~sec:1 (fun () ->
-            cancelled := !cancel_switch; !cancelled);
+            task_expired := !cancel_switch;
+            task_cancelled := !cancel_user_req;
+            if !cancel_user_req then cancel_user_req := false;
+            !task_expired || !task_cancelled);
           let rec loop () =
             let response = unmarshal_response ic in
             match task, response with
@@ -1015,23 +1036,25 @@ end = struct (* {{{ *)
             pr_err ("Fatal marshal error: " ^ s);
             flush_all (); exit 1
         | e ->
-            prerr_endline ("Uncaught exception in worker manager: "^
-              string_of_ppcmds (print e))
-            (* XXX do something sensible *)
+            pr_err ("Uncaught exception in worker manager: "^
+              string_of_ppcmds (print e));
+            flush_all ()
       done
     with
     | KillRespawn ->
         Pp.feedback (Interface.InProgress ~-1);
         Worker.kill proc;
         ignore(Worker.wait proc);
-        manage_slave respawn
-    | Sys_error _ | Invalid_argument _ | End_of_file when !cancelled ->
+        manage_slave cancel_user_req respawn
+    | Sys_error _ | Invalid_argument _ | End_of_file
+      when !task_expired ->
         Pp.feedback (Interface.InProgress ~-1);
         ignore(Worker.wait proc);
-        manage_slave respawn
+        manage_slave cancel_user_req respawn
     | Sys_error _ | Invalid_argument _ | End_of_file
-      when !fallback_to_lazy_if_slave_dies ->
-        msg_warning(strbrk "The worker process died badly.");
+      when !fallback_to_lazy_if_slave_dies || !task_cancelled ->
+        if not !task_cancelled then
+          msg_warning(strbrk "The worker process died badly.");
         (match !last_task with
         | Some task ->
             msg_warning(strbrk "Falling back to local, lazy, evaluation.");
@@ -1041,7 +1064,7 @@ end = struct (* {{{ *)
         | None -> ());
         Worker.kill proc;
         ignore(Worker.wait proc);
-        manage_slave respawn
+        manage_slave cancel_user_req respawn
     | Sys_error _ | Invalid_argument _ | End_of_file ->
         Worker.kill proc;
         let exit_status proc = match Worker.wait proc with
@@ -1755,6 +1778,8 @@ let process_transaction ~tty verbose c (loc, expr) =
 
 (** STM interface {{{******************************************************* **)
 
+let stop_worker n = Slaves.cancel_worker n
+
 let query ~at s =
   Future.purify (fun s ->
     if Stateid.equal at Stateid.dummy then finish ()
diff --git a/toplevel/stm.mli b/toplevel/stm.mli
index 158f8820e..0a7473792 100644
--- a/toplevel/stm.mli
+++ b/toplevel/stm.mli
@@ -38,6 +38,8 @@ val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ]
 (* Evaluates the tip of the current branch *)
 val finish : unit -> unit
 
+val stop_worker : int -> unit
+
 (* Joins the entire document.  Implies finish, but also checks proofs *)
 val join : unit -> unit
 (* To save to disk an incomplete document *)