Merge branch 'v8.5'

6 files changed, 52 insertions, 35 deletions

diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index c9018c9ee9..5dedb0d0ac 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -42,6 +42,8 @@ module M = Map.Make(String)
 type data = string M.t
 type aux_file = data H.t
 
+let contents x = x
+
 let empty_aux_file = H.empty
 
 let get aux loc key = M.find key (H.find (Loc.unloc loc) aux)
diff --git a/lib/aux_file.mli b/lib/aux_file.mli
index e340fc6547..b672d3db28 100644
--- a/lib/aux_file.mli
+++ b/lib/aux_file.mli
@@ -13,6 +13,10 @@ val get : aux_file -> Loc.t -> string -> string
 val empty_aux_file : aux_file
 val set : aux_file -> Loc.t -> string -> string -> aux_file
 
+module H : Map.S with type key = int * int
+module M : Map.S with type key = string
+val contents : aux_file -> string M.t H.t
+
 val start_aux_file_for : string -> unit
 val stop_aux_file : unit -> unit 
 val recording : unit -> bool
diff --git a/lib/cThread.ml b/lib/cThread.ml
index 2d1f10bf39..9cbdf5a9ea 100644
--- a/lib/cThread.ml
+++ b/lib/cThread.ml
@@ -8,22 +8,12 @@
 
 type thread_ic = in_channel
 
-let prepare_in_channel_for_thread_friendly_io ic =
-  Unix.set_nonblock (Unix.descr_of_in_channel ic); ic
-
-let safe_wait_timed_read fd time =
-  try Thread.wait_timed_read fd time
-  with Unix.Unix_error (Unix.EINTR, _, _) ->
-    (** On Unix, the above function may raise this exception when it is
-        interrupted by a signal. (It uses Unix.select internally.) *)
-    false
+let prepare_in_channel_for_thread_friendly_io ic = ic
 
 let thread_friendly_read_fd fd s ~off ~len =
   let rec loop () =
     try Unix.read fd s off len
-    with Unix.Unix_error((Unix.EWOULDBLOCK|Unix.EAGAIN|Unix.EINTR),_,_) ->
-      while not (safe_wait_timed_read fd 0.05) do Thread.yield () done;
-      loop ()
+    with Unix.Unix_error(Unix.EINTR,_,_) -> loop ()
   in 
     loop ()
 
diff --git a/lib/future.ml b/lib/future.ml
index 02d3702d77..78a158264b 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -11,21 +11,27 @@ let freeze = ref (fun () -> assert false : unit -> Dyn.t)
 let unfreeze = ref (fun _ -> () : Dyn.t -> unit)
 let set_freeze f g = freeze := f; unfreeze := g
 
-exception NotReady of string
-exception NotHere of string
-let _ = Errors.register_handler (function
-  | NotReady name ->
+let not_ready_msg = ref (fun name ->
       Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^
                 "Please wait or pass "^
                 "the \"-async-proofs off\" option to CoqIDE to disable "^
                 "asynchronous script processing and don't pass \"-quick\" to "^
-                "coqc.")
-  | NotHere name ->
+                "coqc."))
+let not_here_msg = ref (fun name ->
       Pp.strbrk("The value you are asking for ("^name^") is not available "^
                 "in this process. If you really need this, pass "^
                 "the \"-async-proofs off\" option to CoqIDE to disable "^
                 "asynchronous script processing and don't pass \"-quick\" to "^
-                "coqc.")
+                "coqc."))
+
+let customize_not_ready_msg f = not_ready_msg := f
+let customize_not_here_msg f = not_here_msg := f
+
+exception NotReady of string
+exception NotHere of string
+let _ = Errors.register_handler (function
+  | NotReady name -> !not_ready_msg name
+  | NotHere name -> !not_here_msg name
   | _ -> raise Errors.Unhandled)
 
 type fix_exn = Exninfo.iexn -> Exninfo.iexn
diff --git a/lib/future.mli b/lib/future.mli
index 324d5f7d10..de2282ae92 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -161,3 +161,6 @@ val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds
    Thy are set for the outermos layer of the system, since they have to
    deal with the whole system state. *)
 val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit
+
+val customize_not_ready_msg : (string -> Pp.std_ppcmds) -> unit
+val customize_not_here_msg : (string -> Pp.std_ppcmds) -> unit
diff --git a/lib/spawn.ml b/lib/spawn.ml
index 9b63be70aa..851c6a2235 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -45,26 +45,38 @@ end
 (* Common code *)
 let assert_ b s = if not b then Errors.anomaly (Pp.str s)
 
+(* According to http://caml.inria.fr/mantis/view.php?id=5325
+ * you can't use the same socket for both writing and reading (may change
+ * in 4.03 *)
 let mk_socket_channel () =
   let open Unix in
-  let s = socket PF_INET SOCK_STREAM 0 in
-  bind s (ADDR_INET (inet_addr_loopback,0));
-  listen s 1;
-  match getsockname s with
-  | ADDR_INET(host, port) ->
-      s, string_of_inet_addr host ^":"^ string_of_int port
+  let sr = socket PF_INET SOCK_STREAM 0 in
+  bind sr (ADDR_INET (inet_addr_loopback,0)); listen sr 1;
+  let sw = socket PF_INET SOCK_STREAM 0 in
+  bind sw (ADDR_INET (inet_addr_loopback,0)); listen sw 1;
+  match getsockname sr, getsockname sw with
+  | ADDR_INET(host, portr), ADDR_INET(_, portw) ->
+      (sr, sw),
+      string_of_inet_addr host
+        ^":"^ string_of_int portr ^":"^ string_of_int portw
   | _ -> assert false
 
-let accept s =
-  let r, _, _ = Unix.select [s] [] [] accept_timeout in
+let accept (sr,sw) =
+  let r, _, _ = Unix.select [sr] [] [] accept_timeout in
   if r = [] then raise (Failure (Printf.sprintf
     "The spawned process did not connect back in %2.1fs" accept_timeout));
-  let cs, _ = Unix.accept s in
-  Unix.close s;
-  let cin, cout = Unix.in_channel_of_descr cs, Unix.out_channel_of_descr cs in
+  let csr, _ = Unix.accept sr in
+  Unix.close sr;
+  let cin = Unix.in_channel_of_descr csr in
   set_binary_mode_in cin true;
+  let w, _, _ = Unix.select [sw] [] [] accept_timeout in
+  if w = [] then raise (Failure (Printf.sprintf
+    "The spawned process did not connect back in %2.1fs" accept_timeout));
+  let csw, _ = Unix.accept sw in
+  Unix.close sw;
+  let cout = Unix.out_channel_of_descr csw in
   set_binary_mode_out cout true;
-  cs, cin, cout
+  (csr, csw), cin, cout
 
 let handshake cin cout =
   try
@@ -116,7 +128,7 @@ let spawn_pipe env prog args =
   let cout = Unix.out_channel_of_descr master2worker_w in
   set_binary_mode_in cin true;
   set_binary_mode_out cout true;
-  pid, cin, cout, worker2master_r
+  pid, cin, cout, (worker2master_r, master2worker_w)
 
 let filter_args args =
   let rec aux = function
@@ -180,10 +192,10 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ())
 =
   let pid, oob_resp, oob_req, cin, cout, main, is_sock =
     spawn_with_control prefer_sock env prog args in
-  Unix.set_nonblock main;
+  Unix.set_nonblock (fst main);
   let gchan =
-    if is_sock then ML.async_chan_of_socket main
-    else ML.async_chan_of_file main in
+    if is_sock then ML.async_chan_of_socket (fst main)
+    else ML.async_chan_of_file (fst main) in
   let alive, watch = true, None in
   let p = { cin; cout; gchan; pid; oob_resp; oob_req; alive; watch } in
   p.watch <- Some (