Ide: experimentally allow coqide to interrupt or kill coqtop

 - We now use create_process instead of open_process, and stores
   the answered pid.
 - The "Stop" button now sends a Sigint signal to this coqtop pid.
 - The "Goto Start" button now works even if a computation is ongoing,
   a new process is spawned and the previous one is killed -9, and
   then a waitpid is done to avoid having zombies around.

 Note that currently a vm_compute won't be stopped by a "Stop",
 but only by a "Goto Start". This can be quite confusing. How to
 properly document that "Goto Start" has the side effect of being
 a kill ? Maybe we could check someday if the Ctrl-C has been
 successful, and kill -9 if not ? Or maybe make coqide aware
 of a flag "we_are_vm_computing" and then kill -9 instead of Ctrl-C
 in this case ?

 TODO:
  - for the moment a forced "Goto Start" displays an unfriendly anomaly
  - check if all this works under Windows (probably but not sure).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13926 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 50 insertions, 46 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 285133d48..89040aa5f 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -26,19 +26,13 @@ open Ideutils
 open Compat
 
 type coqtop = {
+  mutable pid : int;
   mutable cout : in_channel ;
   mutable cin : out_channel ;
-  sup_args : string ;
+  sup_args : string list;
   mutable version : int ;
 }
 
-let dummy_coqtop = {
-  cout = stdin ;
-  cin = stdout ;
-  sup_args = "" ;
-  version = 0 ;
-}
-
 let prerr_endline s = if !debug then prerr_endline s else ()
 
 let output = ref (Format.formatter_of_out_channel stdout)
@@ -109,7 +103,8 @@ exception Coqtop_output of string list
 
 let check_connection args =
   try
-    let ic = Unix.open_process_in (coqtop_path () ^ " -batch "^args) in
+    let args = String.concat " " ("-batch"::args) in
+    let ic = Unix.open_process_in (coqtop_path () ^ " " ^ args) in
     let lines = read_all_lines ic in
     match (Unix.close_process_in ic) with
     | Unix.WEXITED 0 -> prerr_endline "coqtop seems ok"
@@ -142,27 +137,42 @@ let toplvl_ctr_mtx = Mutex.create ()
 
 let spawn_coqtop sup_args =
   Mutex.lock toplvl_ctr_mtx;
-  try 
-    let oc,ic = Unix.open_process (coqtop_path ()^" -ideslave "^sup_args) in
-    set_binary_mode_out ic true;
-    set_binary_mode_in oc true;
+  try
+    let (in_read,in_write) = Unix.pipe () in
+    let (out_read,out_write) = Unix.pipe () in
+    let prog = coqtop_path () in
+    let args = Array.of_list (prog :: "-ideslave" :: sup_args) in
+    let pid = Unix.create_process prog args out_read in_write Unix.stderr in
+    assert (pid <> 0);
+    Unix.close out_read;
+    Unix.close in_write;
+    let ic = Unix.in_channel_of_descr in_read in
+    let oc = Unix.out_channel_of_descr out_write in
+    set_binary_mode_out oc true;
+    set_binary_mode_in ic true;
     incr toplvl_ctr;
     Mutex.unlock toplvl_ctr_mtx;
-    { cin = ic; cout = oc ; sup_args = sup_args ; version = 0 }
+    { pid = pid; cin = oc; cout = ic ; sup_args = sup_args ; version = 0 }
   with e ->
     Mutex.unlock toplvl_ctr_mtx;
     raise e
 
+let break_coqtop coqtop =
+  try Unix.kill coqtop.pid Sys.sigint
+  with _ -> prerr_endline "Error while sending Ctrl-C"
+
+let blocking_kill pid =
+  begin
+    try Unix.kill pid Sys.sigkill;
+    with _ -> prerr_endline "Kill -9 failed. Process already terminated ?"
+  end;
+  try
+    ignore (Unix.waitpid [] pid);
+    Mutex.lock toplvl_ctr_mtx; decr toplvl_ctr; Mutex.unlock toplvl_ctr_mtx
+  with _ -> prerr_endline "Error while waiting for child"
+
 let kill_coqtop coqtop =
-  let ic = coqtop.cin in
-  let oc = coqtop.cout in
-  ignore (Thread.create
-            (fun () ->
-               try 
-                 ignore (Unix.close_process (oc,ic));
-                 Mutex.lock toplvl_ctr_mtx; decr toplvl_ctr; Mutex.unlock toplvl_ctr_mtx
-               with _ -> prerr_endline "Process leak")
-            ())
+  ignore (Thread.create blocking_kill coqtop.pid)
 
 let coqtop_zombies =
   (fun () ->
@@ -176,6 +186,7 @@ let reset_coqtop coqtop =
   let ni = spawn_coqtop coqtop.sup_args in
   coqtop.cin <- ni.cin;
   coqtop.cout <- ni.cout;
+  coqtop.pid <- ni.pid
 
 module PrintOpt =
 struct
diff --git a/ide/coq.mli b/ide/coq.mli
index 6bc593477..c909a559f 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -15,16 +15,16 @@ open Ide_blob
 val short_version : unit -> string
 val version : unit -> string
 val filter_coq_opts : string list -> bool * string list
-val check_connection : string -> unit
+val check_connection : string list -> unit
 
 type coqtop
 
-val dummy_coqtop : coqtop
-
-val spawn_coqtop : string -> coqtop
+val spawn_coqtop : string list -> coqtop
 
 val kill_coqtop : coqtop -> unit
 
+val break_coqtop : coqtop -> unit
+
 val coqtop_zombies : unit -> int
 
 val reset_coqtop : coqtop -> unit
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 5ebea7589..475b8f8a4 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -217,20 +217,12 @@ let coq_computing = Mutex.create ()
 let coq_may_stop = Mutex.create ()
 
 let break () =
-  prerr_endline "User break received:";
-  if not (Mutex.try_lock coq_computing) then
-    begin
-      prerr_endline " trying to stop computation:";
-      if Mutex.try_lock coq_may_stop then begin
-	  Util.interrupt := true;
-	  prerr_endline " interrupt flag set. Computation should stop soon...";
-	  Mutex.unlock coq_may_stop
-	end else prerr_endline " interruption refused (may not stop now)";
-    end
-  else begin
-      Mutex.unlock coq_computing;
-      prerr_endline " ignored (not computing)"
-    end
+  prerr_endline "User break received";
+  Coq.break_coqtop session_notebook#current_term.toplvl
+
+let force_reset_initial () =
+  prerr_endline "Reset Initial";
+  session_notebook#current_term.analyzed_view#reset_initial
 
 let do_if_not_computing text f x =
   let threaded_task () =
@@ -242,7 +234,8 @@ let do_if_not_computing text f x =
            | Sys_error str ->
                elt.analyzed_view#reset_initial;
                elt.analyzed_view#set_message
-                 ("unable to communicate with coqtop, restarting coqtop:\n"^str)
+                 ("Unable to communicate with coqtop, restarting coqtop.\n"^
+		  "Error was: "^str)
            | e ->
                Mutex.unlock coq_computing;
                elt.analyzed_view#set_message
@@ -537,7 +530,7 @@ let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) =
     buffer#apply_tag ~start:decl_start ~stop:decl_end Tags.Script.folded;
     buffer#apply_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden)
 
-let sup_args = ref ""
+let sup_args = ref []
 
 class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs _ct =
 object(self)
@@ -2317,7 +2310,7 @@ let main files =
 				    "_Start"
 				    ~tooltip:"Go to start"
 				    ~key:GdkKeysyms._Home
-				    ~callback:(do_or_activate (fun a -> a#reset_initial))
+				    ~callback:force_reset_initial
 				    `GOTO_TOP;
 				  add_to_menu_toolbar
 				    "_End"
diff --git a/ide/coqide.mli b/ide/coqide.mli
index cac6878cd..dd3995eb9 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -10,7 +10,7 @@
    command line, initialize the load path, load the input
    state, load the files given on the command line, load the ressource file,
    produce the output state if any, and finally will launch the interface. *)
-val sup_args : string ref
+val sup_args : string list ref
 val do_load : string -> unit
 val process_argv : string list -> string list
 val crash_save : int -> unit
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 6e36df6d1..4bb80f4a7 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -14,7 +14,7 @@ let () =
   let argl = Array.to_list Sys.argv in
   let files = Coqide.process_argv argl in
   let args = List.filter (fun x -> not (List.mem x files)) (List.tl argl) in
-  Coqide.sup_args := String.concat " " (List.map Filename.quote args);
+  Coqide.sup_args := List.map Filename.quote args;
   Coq.check_connection !Coqide.sup_args;
   Coqide.ignore_break ();
     GtkMain.Rc.add_default_file (Ideutils.lib_ide_file ".coqide-gtk2rc");