diff options
| -rw-r--r-- | lib/spawn.ml | 44 | ||||
| -rw-r--r-- | stm/spawned.ml | 19 | ||||
| -rw-r--r-- | stm/spawned.mli | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 3 |
4 files changed, 41 insertions, 27 deletions
diff --git a/lib/spawn.ml b/lib/spawn.ml index 9b63be70a..851c6a223 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 ( diff --git a/stm/spawned.ml b/stm/spawned.ml index a8372195d..66fe07dbc 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -11,7 +11,7 @@ open Spawn let pr_err s = Printf.eprintf "(Spawned,%d) %s\n%!" (Unix.getpid ()) s let prerr_endline s = if !Flags.debug then begin pr_err s end else () -type chandescr = AnonPipe | Socket of string * int +type chandescr = AnonPipe | Socket of string * int * int let handshake cin cout = try @@ -26,18 +26,19 @@ let handshake cin cout = | End_of_file -> pr_err "Handshake failed: End_of_file"; raise (Failure "handshake") -let open_bin_connection h p = +let open_bin_connection h pr pw = let open Unix in - let cin, cout = open_connection (ADDR_INET (inet_addr_of_string h,p)) in + let _, cout = open_connection (ADDR_INET (inet_addr_of_string h,pr)) in + let cin, _ = open_connection (ADDR_INET (inet_addr_of_string h,pw)) in set_binary_mode_in cin true; set_binary_mode_out cout true; let cin = CThread.prepare_in_channel_for_thread_friendly_io cin in cin, cout -let controller h p = +let controller h pr pw = prerr_endline "starting controller thread"; let main () = - let ic, oc = open_bin_connection h p in + let ic, oc = open_bin_connection h pr pw in let rec loop () = try match CThread.thread_friendly_input_value ic with @@ -61,8 +62,8 @@ let init_channels () = if !channels <> None then Errors.anomaly(Pp.str "init_channels called twice"); let () = match !main_channel with | None -> () - | Some (Socket(mh,mp)) -> - channels := Some (open_bin_connection mh mp); + | Some (Socket(mh,mpr,mpw)) -> + channels := Some (open_bin_connection mh mpr mpw); | Some AnonPipe -> let stdin = Unix.in_channel_of_descr (Unix.dup Unix.stdin) in let stdout = Unix.out_channel_of_descr (Unix.dup Unix.stdout) in @@ -74,8 +75,8 @@ let init_channels () = in match !control_channel with | None -> () - | Some (Socket (ch, cp)) -> - controller ch cp + | Some (Socket (ch, cpr, cpw)) -> + controller ch cpr cpw | Some AnonPipe -> Errors.anomaly (Pp.str "control channel cannot be a pipe") diff --git a/stm/spawned.mli b/stm/spawned.mli index d9e7baff3..d0183e081 100644 --- a/stm/spawned.mli +++ b/stm/spawned.mli @@ -8,7 +8,7 @@ (* To link this file, threads are needed *) -type chandescr = AnonPipe | Socket of string * int +type chandescr = AnonPipe | Socket of string * int * int (* Argument parsing should set these *) val main_channel : chandescr option ref diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7562c29f7..9b5a09de0 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -359,7 +359,8 @@ let get_int opt n = let get_host_port opt s = match CString.split ':' s with - | [host; port] -> Some (Spawned.Socket(host, int_of_string port)) + | [host; portr; portw] -> + Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) | ["stdfds"] -> Some Spawned.AnonPipe | _ -> prerr_endline ("Error: host:port or stdfds expected after option "^opt); |