diff options
| -rw-r--r-- | configure.ml | 8 | ||||
| -rw-r--r-- | lib/spawn.ml | 8 | ||||
| -rw-r--r-- | lib/system.ml | 58 | ||||
| -rw-r--r-- | plugins/micromega/mutils.ml | 8 |
4 files changed, 55 insertions, 27 deletions
diff --git a/configure.ml b/configure.ml index f72910d4c..e64c04254 100644 --- a/configure.ml +++ b/configure.ml @@ -38,6 +38,12 @@ let check_exit_code (_,code) = match code with | Unix.WSIGNALED n -> failwith ("killed by signal " ^ i2s n) | Unix.WSTOPPED n -> failwith ("stopped by signal " ^ i2s n) +(** As for Unix.close_process, our Unix.waipid will ignore all EINTR *) + +let rec waitpid_non_intr pid = + try Unix.waitpid [] pid + with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_non_intr pid + (** Below, we'd better read all lines on a channel before closing it, otherwise a SIGPIPE could be encountered by the sub-process *) @@ -76,7 +82,7 @@ let run ?(fatal=true) ?(err=StdErr) prog args = let () = Unix.close nul_w in let line = read_first_line_and_close out_r in let _ = read_first_line_and_close nul_r in - let () = check_exit_code (Unix.waitpid [] pid) in + let () = check_exit_code (waitpid_non_intr pid) in line with | _ when not fatal && not !verbose -> "" diff --git a/lib/spawn.ml b/lib/spawn.ml index e350926b7..f32aa4d62 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -221,9 +221,11 @@ let kill_if p ~sec test = false end else true) -let wait { pid = (unixpid, _) } = - try snd (Unix.waitpid [] unixpid) - with Unix.Unix_error _ -> Unix.WEXITED 0o400 +let rec wait p = + try snd (Unix.waitpid [] (fst p.pid)) + with + | Unix.Unix_error (Unix.EINTR, _, _) -> wait p + | Unix.Unix_error _ -> Unix.WEXITED 0o400 end diff --git a/lib/system.ml b/lib/system.ml index aa6671116..6c357ee36 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -212,37 +212,51 @@ let with_magic_number_check f a = (* Communication through files with another executable *) let connect writefun readfun com = + (* step 0 : prepare temporary files and I/O channels *) let name = Filename.basename com in - let tmp_to = Filename.temp_file ("coq-"^name^"-in") ".xml" in - let tmp_from = Filename.temp_file ("coq-"^name^"-out") ".xml" in - let ch_to_in,ch_to_out = - try open_in tmp_to, open_out tmp_to + let req,req_wr = + try Filename.open_temp_file ("coq-"^name^"-in") ".xml" with Sys_error s -> error ("Cannot set connection to "^com^"("^s^")") in - let ch_from_in,ch_from_out = - try open_in tmp_from, open_out tmp_from + let ans,ans_wr = + try Filename.open_temp_file ("coq-"^name^"-out") ".xml" with Sys_error s -> - close_out ch_to_out; close_in ch_to_in; + close_out req_wr; error ("Cannot set connection from "^com^"("^s^")") in - writefun ch_to_out; - close_out ch_to_out; + let ans_wr' = Unix.descr_of_out_channel ans_wr in + (* step 1 : fill the request file *) + writefun req_wr; + close_out req_wr; + (* step 2a : prepare the request-reading descriptor for the sub-process *) + let req_rd' = + try Unix.openfile req [Unix.O_RDONLY] 0o644 + with Unix.Unix_error (err,_,_) -> + close_out ans_wr; + let msg = Unix.error_message err in + error ("Cannot set connection to "^com^"("^msg^")") + in + (* step 2b : launch the sub-process *) let pid = - let ch_to' = Unix.descr_of_in_channel ch_to_in in - let ch_from' = Unix.descr_of_out_channel ch_from_out in - try Unix.create_process com [|com|] ch_to' ch_from' Unix.stdout + try Unix.create_process com [|com|] req_rd' ans_wr' Unix.stdout with Unix.Unix_error (err,_,_) -> - close_in ch_to_in; close_in ch_from_in; close_out ch_from_out; - unlink tmp_from; unlink tmp_to; - error ("Cannot execute "^com^"("^(Unix.error_message err)^")") in - close_in ch_to_in; - close_out ch_from_out; - (match snd (Unix.waitpid [] pid) with + Unix.close req_rd'; close_out ans_wr; Unix.unlink req; Unix.unlink ans; + let msg = Unix.error_message err in + error ("Cannot execute "^com^"("^msg^")") in + Unix.close req_rd'; + close_out ans_wr; + (* step 2c : wait for termination of the sub-process *) + (match CUnix.waitpid_non_intr pid with | Unix.WEXITED 127 -> error (com^": cannot execute") | Unix.WEXITED 0 -> () | _ -> error (com^" exited abnormally")); - let a = readfun ch_from_in in - close_in ch_from_in; - unlink tmp_from; - unlink tmp_to; + (* step 3 : read the answer and handle it *) + let ans_rd = + try open_in ans + with Sys_error s -> error ("Cannot read output of "^com^"("^s^")") in + let a = readfun ans_rd in + close_in ans_rd; + (* step 4 : cleanup the temporary files *) + unlink req; + unlink ans; a (* Time stamps. *) diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 0b98696c9..ae89364e6 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -403,6 +403,12 @@ end module TagSet = Set.Make(Tag) +(** As for Unix.close_process, our Unix.waipid will ignore all EINTR *) + +let rec waitpid_non_intr pid = + try snd (Unix.waitpid [] pid) + with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_non_intr pid + (** * Forking routine, plumbing the appropriate pipes where needed. *) @@ -422,7 +428,7 @@ let command exe_path args vl = flush outch ; (* Wait for its completion *) - let _pid,status = Unix.waitpid [] pid in + let status = waitpid_non_intr pid in finally (* Recover the result *) |