Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg

1 files changed, 19 insertions, 1 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 8b1fa0a3..07f0ece8 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -191,11 +191,29 @@ let coqtop_zombies () =
 
     Note: we use Unix.stderr in Unix.create_process to get debug
     messages from the coqtop's Ide_slave loop.
+
+    NB: it's important to close coqide's descriptors (ide2top_w and top2ide_r)
+    in coqtop. We do this indirectly via [Unix.set_close_on_exec].
+    This way, coqide has the only remaining copies of these descriptors,
+    and closing them later will have visible effects in coqtop. Cf man 7 pipe :
+
+    - If  all file descriptors referring to the write end of a pipe have been
+      closed, then an attempt to read(2) from the pipe will see end-of-file
+      (read(2) will return 0).
+    - If all file descriptors referring to the read end of a pipe have been
+      closed, then a write(2) will cause a SIGPIPE signal to be generated for
+      the calling process. If the calling process is ignoring this signal,
+      then write(2) fails with the error EPIPE.
+
+    Symmetrically, coqtop's descriptors (ide2top_r and top2ide_w) should be
+    closed in coqide.
 *)
 
 let open_process_pid prog args =
   let (ide2top_r,ide2top_w) = Unix.pipe () in
   let (top2ide_r,top2ide_w) = Unix.pipe () in
+  Unix.set_close_on_exec ide2top_w;
+  Unix.set_close_on_exec top2ide_r;
   let pid = Unix.create_process prog args ide2top_r top2ide_w Unix.stderr in
   assert (pid <> 0);
   Unix.close ide2top_r;
@@ -250,7 +268,7 @@ let eval_call coqtop (c:'a Ide_intf.call) =
   Xml_utils.print_xml coqtop.cin (Ide_intf.of_call c);
   flush coqtop.cin;
   let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in
-  (Ide_intf.to_answer xml : 'a Interface.value)
+  (Ide_intf.to_answer xml c : 'a Interface.value)
 
 let interp coqtop ?(raw=false) ?(verbose=true) s =
   eval_call coqtop (Ide_intf.interp (raw,verbose,s))