diff options
| -rw-r--r-- | ide/coq.ml | 244 | ||||
| -rw-r--r-- | ide/coq.mli | 10 | ||||
| -rw-r--r-- | ide/coqide.ml | 5 | ||||
| -rw-r--r-- | ide/coqide_main.ml4 | 3 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 13 | ||||
| -rw-r--r-- | toplevel/ide_slave.ml | 23 |
6 files changed, 89 insertions, 209 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 7d1267c3a..bb0fdc089 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -179,81 +179,32 @@ let mk_ccb poly = { open_ccb = fun scope -> scope.bind_ccb poly } let with_ccb ccb e = ccb.open_ccb e let interrupter = ref (fun pid -> Unix.kill pid Sys.sigint) -let soft_killer = ref (fun pid -> Unix.kill pid Sys.sigterm) -let killer = ref (fun pid -> Unix.kill pid Sys.sigkill) -(** Handling old processes *) - -type unix_process_id = int -type retry = int - -let zombies = ref ([] : (unix_process_id * retry) list) - -let pr_zombies ?(full=false) l = - let pr (pid,retries) = - string_of_int pid ^ - if full then "["^string_of_int retries^"]" else "" - in - String.concat ", " (List.map pr l) - -let is_buried pid = - try fst (Unix.waitpid [Unix.WNOHANG] pid) <> 0 - with Unix.Unix_error _ -> false - -let max_retry = 3 (* one soft then two hard kill attempts *) +(** * The structure describing a coqtop sub-process *) -let countdown = ref None -let final_countdown () = (countdown := Some max_retry) +let gio_channel_of_descr_socket = ref Glib.Io.channel_of_descr -let check_zombies () = - (* First, do [waitpid] on our zombies and try to kill the survivors *) - let handle_zombie others (pid,retries) = - if is_buried pid then others - else - let () = match retries with - | 0 -> () (* freshly closed coqtop, leave it some time *) - | 1 -> ignore_error !soft_killer pid - | _ -> ignore_error !killer pid - in (pid,retries+1) :: others - in - let zs = List.fold_left handle_zombie [] !zombies - in - if zs <> [] then - Minilib.log ("Remaining zombies: "^ pr_zombies ~full:true zs); - (* Second, we warn the user about old zombies that refuses to die - (except in the middle of the final countdown) *) - let chk_old = !countdown = None || !countdown = Some 0 in - let old_zombies, new_zombies = - List.partition (fun (_,n) -> chk_old && n >= max_retry) zs - in - if old_zombies <> [] then begin - let msg1 = "Some coqtop processes are still running.\n" in - let msg2 = "You may have to kill them manually.\nPids: " in - let msg3 = pr_zombies old_zombies in - let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.close - ~message_type:`ERROR ~message:(msg1 ^ msg2 ^ msg3) () - in - ignore (popup#run ()); - ignore (popup#destroy ()) - end; - zombies := new_zombies; - (* Finally, we might end coqide if the final countdown has started *) - if !countdown = Some 0 || (!countdown <> None && zs = []) then exit 0; - countdown := Option.map pred !countdown; - true +module GlibMainLoop = struct + type async_chan = Glib.Io.channel + type watch_id = Glib.Io.id + type condition = Glib.Io.condition + let add_watch ~callback chan = + Glib.Io.add_watch ~cond:[`ERR; `HUP; `IN; `NVAL; `PRI] ~callback chan + let remove_watch = Glib.Io.remove + let read_all = Ideutils.io_read_all + let async_chan_of_file fd = Glib.Io.channel_of_descr fd + let async_chan_of_socket s = !gio_channel_of_descr_socket s + let add_timeout ~sec callback = + ignore(Glib.Timeout.add ~ms:(sec * 1000) ~callback) +end -let _ = Glib.Timeout.add ~ms:300 ~callback:check_zombies - -(** * The structure describing a coqtop sub-process *) +module CoqTop = Spawn.Async(GlibMainLoop) type handle = { - pid : unix_process_id; + proc : CoqTop.process; + xml_oc : Xml_printer.t; mutable alive : bool; mutable waiting_for : (ccb * logger) option; (* last call + callback + log *) - xml_oc : Xml_printer.t; - xml_ic : Xml_parser.t; - glib_ic : Glib.Io.channel; - close_xml_channels : unit -> unit } (** Coqtop process status : @@ -327,59 +278,16 @@ let lift (f : unit -> 'a) : 'a task = closed in coqide. *) -let open_coqtop_pipe 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; - Unix.close top2ide_w; - Unix.set_nonblock top2ide_r; - pid, - Unix.in_channel_of_descr top2ide_r, - Glib.Io.channel_of_descr top2ide_r, - Unix.out_channel_of_descr ide2top_w, - (fun () -> Unix.close top2ide_r; Unix.close ide2top_w) - -let gio_channel_of_descr_socket = ref Glib.Io.channel_of_descr - -let open_coqtop_socket prog args = - let s = Unix.socket Unix.PF_INET Unix.SOCK_STREAM 0 in - Unix.bind s (Unix.ADDR_INET (Unix.inet_addr_loopback,0)); - Unix.listen s 1; - let host, port = - match Unix.getsockname s with - | Unix.ADDR_INET(host, port) -> - Unix.string_of_inet_addr host, string_of_int port - | _ -> assert false in - let pid = - Unix.create_process prog - (Array.append args [|"-ideslave-socket";host^":"^port|]) - (Unix.openfile "slave.in" [Unix.O_CREAT;Unix.O_RDONLY] 0o660) - (Unix.openfile "slave.out" [Unix.O_CREAT;Unix.O_WRONLY] 0o660) - (Unix.openfile "slave.err" [Unix.O_CREAT;Unix.O_WRONLY] 0o660) in - assert (pid <> 0); - let cs, _ = Unix.accept s in - Unix.set_nonblock cs; - pid, - Unix.in_channel_of_descr cs, - !gio_channel_of_descr_socket cs, - Unix.out_channel_of_descr cs, - (fun () -> Unix.close cs; Unix.close s) - -let open_process_pid prog args = - if Sys.os_type = "Unix" then open_coqtop_pipe prog args - else open_coqtop_socket prog args - -exception TubeError +exception TubeError of string exception AnswerWithoutRequest of string let rec check_errors = function | [] -> () | (`IN | `PRI) :: conds -> check_errors conds -| e :: _ -> raise TubeError +| `ERR :: _ -> raise (TubeError "ERR") +| `HUP :: _ -> raise (TubeError "HUP") +| `NVAL :: _ -> raise (TubeError "NVAL") +| `OUT :: _ -> raise (TubeError "OUT") let handle_intermediate_message handle xml = let message = Serialize.to_message xml in @@ -413,13 +321,12 @@ type input_state = { mutable lexerror : int option; } -let unsafe_handle_input handle feedback_processor state conds = - let chan = handle.glib_ic in - let () = check_errors conds in - let s = io_read_all chan in - let () = if String.length s = 0 then raise TubeError in +let unsafe_handle_input handle feedback_processor state conds ~read_all = + check_errors conds; + let s = read_all () in + if String.length s = 0 then raise (TubeError "EMPTY"); let s = state.fragment ^ s in - let () = state.fragment <- s in + state.fragment <- s; let lex = Lexing.from_string s in let p = Xml_parser.make (Xml_parser.SLexbuf lex) in let rec loop () = @@ -444,65 +351,51 @@ let unsafe_handle_input handle feedback_processor state conds = let l_end = Lexing.lexeme_end lex in (** Heuristic hack not to reimplement the lexer: if ever the lexer dies twice at the same place, then this is a non-recoverable error *) - let () = match state.lexerror with - | None -> () - | Some loc -> if loc = l_end then raise e - in - let () = state.lexerror <- Some l_end in - () - -let install_input_watch handle respawner feedback_processor = - let io_chan = handle.glib_ic in - let all_conds = [`ERR; `HUP; `IN; `NVAL; `PRI] in (* all except `OUT *) - let state = { - fragment = ""; - lexerror = None; - } in - let print_exception = function + if state.lexerror = Some l_end then raise e; + state.lexerror <- Some l_end + +let print_exception = function | Xml_parser.Error e -> Xml_parser.error e | Serialize.Marshal_error -> "Protocol violation" | e -> Printexc.to_string e - in - let handle_input conds = - if not handle.alive then false (* coqtop already terminated *) + +let input_watch handle respawner feedback_processor = + let state = { fragment = ""; lexerror = None; } in + (fun conds ~read_all -> + let h = handle () in + if not h.alive then false else - try - let () = unsafe_handle_input handle feedback_processor state conds in - true + try unsafe_handle_input h feedback_processor state conds ~read_all; true with e -> - let () = Minilib.log ("Coqtop reader failed, resetting: "^print_exception e) in - let () = respawner () in - false - in - ignore (Glib.Io.add_watch ~cond:all_conds ~callback:handle_input io_chan) + Minilib.log ("Coqtop reader failed, resetting: "^print_exception e); + respawner (); + false) + +let bind_self_as f = + let me = ref None in + let get_me () = Option.get !me in + me := Some(f get_me); + Option.get !me (** This launches a fresh handle from its command line arguments. *) -let spawn_handle args = +let spawn_handle args respawner feedback_processor = let prog = coqtop_path () in - let args = Array.of_list ( - prog :: "-async-proofs" :: "on" :: "-ideslave" :: args) in - let pid, ic, gic, oc, close_channels = open_process_pid prog args in - let xml_ic = Xml_parser.make (Xml_parser.SChannel ic) in - let xml_oc = Xml_printer.make (Xml_printer.TChannel oc) in - Xml_parser.check_eof xml_ic false; + let args = Array.of_list ("-async-proofs" :: "on" :: "-ideslave" :: args) in + bind_self_as (fun handle -> + let proc, oc = + CoqTop.spawn ?env prog args (input_watch handle respawner feedback_processor) in { - pid = pid; + proc; + xml_oc = Xml_printer.make (Xml_printer.TChannel oc); alive = true; waiting_for = None; - xml_oc = xml_oc; - xml_ic = xml_ic; - glib_ic = gic; - close_xml_channels = close_channels - } + }) (** This clears any potentially remaining open garbage. *) let clear_handle h = if h.alive then begin (* invalidate the old handle *) h.alive <- false; - h.close_xml_channels (); - (* we monitor the death of the old process *) - zombies := (h.pid,0) :: !zombies end let mkready coqtop = @@ -510,29 +403,28 @@ let mkready coqtop = let rec respawn_coqtop ?(why=Unexpected) coqtop = clear_handle coqtop.handle; - ignore_error (fun () -> coqtop.handle <- spawn_handle coqtop.sup_args) (); + ignore_error (fun () -> + coqtop.handle <- + spawn_handle + coqtop.sup_args + (fun () -> respawn_coqtop coqtop) + coqtop.feedback_handler) (); (* Normally, the handle is now a fresh one. If not, there isn't much we can do ... *) assert (coqtop.handle.alive = true); coqtop.status <- New; - install_input_watch coqtop.handle - (fun () -> respawn_coqtop coqtop) - (fun msg -> coqtop.feedback_handler msg); ignore (coqtop.reset_handler why coqtop.handle (mkready coqtop)) let spawn_coqtop sup_args = - let ct = - { - handle = spawn_handle sup_args; + bind_self_as (fun this -> { + handle = spawn_handle sup_args + (fun () -> respawn_coqtop (this ())) + (fun msg -> (this ()).feedback_handler msg); sup_args = sup_args; reset_handler = (fun _ _ k -> k ()); feedback_handler = (fun _ -> ()); status = New; - } - in - install_input_watch ct.handle - (fun () -> respawn_coqtop ct) (fun msg -> ct.feedback_handler msg); - ct + }) let set_reset_handler coqtop hook = coqtop.reset_handler <- hook @@ -552,7 +444,7 @@ let close_coqtop coqtop = let reset_coqtop coqtop = respawn_coqtop ~why:Planned coqtop let break_coqtop coqtop = - try !interrupter coqtop.handle.pid + try !interrupter (CoqTop.unixpid coqtop.handle.proc) with _ -> Minilib.log "Error while sending Ctrl-C" let get_arguments coqtop = coqtop.sup_args diff --git a/ide/coq.mli b/ide/coq.mli index aa8346348..f6f92a9a9 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -86,19 +86,9 @@ val get_arguments : coqtop -> string list val set_arguments : coqtop -> string list -> unit (** Set process arguments. This also forces a planned reset. *) -(** In win32, we'll use a different kill function than Unix.kill *) - -val killer : (int -> unit) ref -val soft_killer : (int -> unit) ref -val interrupter : (int -> unit) ref - (** In win32, sockets are not like regular files *) val gio_channel_of_descr_socket : (Unix.file_descr -> Glib.Io.channel) ref -val final_countdown : unit -> unit -(** [final_countdown] triggers an exit of coqide after - some last cycles for closing remaining coqtop zombies *) - (** {5 Task processing} *) val try_grab : coqtop -> unit task -> (unit -> unit) -> unit diff --git a/ide/coqide.ml b/ide/coqide.ml index 9da46d2e6..1a6685b38 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -184,7 +184,7 @@ let check_quit saveall = (* For MacOS, just to be sure, we close all coqtops (again?) *) let close_and_quit () = List.iter (fun sn -> Coq.close_coqtop sn.coqtop) notebook#pages; - Coq.final_countdown () + exit 0 let crash_save exitcode = Minilib.log "Starting emergency save of buffers in .crashcoqide files"; @@ -247,7 +247,7 @@ let revert_all _ = notebook#pages let quit _ = - try FileAux.check_quit saveall; Coq.final_countdown () + try FileAux.check_quit saveall; exit 0 with FileAux.DontQuit -> () let close_buffer sn = @@ -1469,6 +1469,7 @@ let read_coqide_args argv = output_string stderr "Error: missing argument after -coqtop"; exit 1 |"-debug"::args -> Minilib.debug := true; + Flags.debug := true; Backtrace.record_backtrace true; filter_coqtop coqtop project_files ("-debug"::out) args |arg::args -> filter_coqtop coqtop project_files (arg::out) args diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index 5c960c444..1e9f0b9ab 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -88,9 +88,6 @@ IFDEF WIN32 THEN external win32_kill : int -> unit = "win32_kill" external win32_interrupt : int -> unit = "win32_interrupt" let () = - Coq.killer := win32_kill; - Coq.soft_killer := win32_kill; - Coq.interrupter := win32_interrupt; Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket; set_win32_path (); reroute_stdout_stderr () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 840ba3e4c..72db18ef0 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -239,8 +239,11 @@ let get_int opt n = let get_host_port opt s = match CString.split ':' s with - | [host; port] -> Some (host, int_of_string port) - | _ -> prerr_endline ("Error: host:port expected after option "^opt); exit 1 + | [host; port] -> Some (Spawned.Socket(host, int_of_string port)) + | ["stdfds"] -> Some Spawned.AnonPipe + | _ -> + prerr_endline ("Error: host:port or stdfds expected after option "^opt); + exit 1 let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s) @@ -326,7 +329,6 @@ let parse_args arglist = |"-compile-verbose" -> add_compile true (next ()) |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true |"-exclude-dir" -> exclude_search_in_dirname (next ()) - |"-ideslave-socket" -> Flags.ide_slave_socket := get_host_port opt (next()) |"-init-file" -> set_rcfile (next ()) |"-inputstate"|"-is" -> set_inputstate (next ()) |"-load-ml-object" -> Mltop.dir_ml_load (next ()) @@ -340,6 +342,8 @@ let parse_args arglist = |"-top" -> set_toplevel_name (dirpath_of_string (next ())) |"-unsafe" -> add_unsafe (next ()) |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ()) + |"-main-channel" -> Spawned.main_channel := get_host_port opt (next()) + |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) (* Options with zero arg *) |"-batch" -> set_batch_mode () @@ -415,6 +419,9 @@ let init arglist = prerr_endline "See --help for the list of supported options"; exit 1 end; + (* If we have been spawned by the Spawn module, this has to be done + * early since the master waits us to connect back *) + Spawned.init_channels (); Envars.set_coqlib Errors.error; if !print_where then (print_endline (Envars.coqlib ()); exit (exitcode ())); if !print_config then (Usage.print_config (); exit (exitcode ())); diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 98386c69e..e93d16720 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -30,22 +30,16 @@ let init_signal_handler () = (** Redirection of standard output to a printable buffer *) -let orig_stdout = ref stdout - -let init_stdout,read_stdout = +let init_stdout, read_stdout = let out_buff = Buffer.create 100 in let out_ft = Format.formatter_of_buffer out_buff in let deep_out_ft = Format.formatter_of_buffer out_buff in let _ = Pp_control.set_gp deep_out_ft Pp_control.deep_gp in (fun () -> flush_all (); - orig_stdout := Unix.out_channel_of_descr (Unix.dup Unix.stdout); - Unix.dup2 Unix.stderr Unix.stdout; Pp_control.std_ft := out_ft; Pp_control.err_ft := out_ft; Pp_control.deep_ft := deep_out_ft; - set_binary_mode_out !orig_stdout true; - set_binary_mode_in stdin true; ), (fun () -> Format.pp_print_flush out_ft (); let r = Buffer.contents out_buff in @@ -365,7 +359,7 @@ let eval_call xml_oc log c = Serialize.abstract_eval_call handler c (** Message dispatching. - Since coqtop -ideslave -coq-slaves on starts 1 thread per slave, and each + Since coqtop -ideslave starts 1 thread per slave, and each thread forwards feedback messages from the slave to the GUI on the same xml channel, we need mutual exclusion. The mutex should be per-channel, but here we only use 1 channel. *) @@ -401,13 +395,12 @@ let slave_feeder xml_oc msg = let loop () = init_signal_handler (); catch_break := false; - let in_ch, out_ch = - match !Flags.ide_slave_socket with - | None -> stdin, !orig_stdout - | Some(h,p) -> - Unix.open_connection (Unix.ADDR_INET(Unix.inet_addr_of_string h,p)) in + let in_ch, out_ch = Spawned.get_channels () in let xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in - let xml_ic = Xml_parser.make (Xml_parser.SChannel in_ch) in + Spawned.prepare_in_channel_for_thread_friendly_blocking_input in_ch; + let in_lb = + Lexing.from_function (Spawned.thread_friendly_blocking_input in_ch) in + let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in let () = Xml_parser.check_eof xml_ic false in set_logger (slave_logger xml_oc); set_feeder (slave_feeder xml_oc); @@ -425,7 +418,7 @@ let loop () = let () = pr_debug_answer q r in (* pr_with_pid (Xml_printer.to_string_fmt (Serialize.of_answer q r)); *) print_xml xml_oc (Serialize.of_answer q r); - flush !orig_stdout + flush out_ch with | Xml_parser.Error (Xml_parser.Empty, _) -> pr_debug "End of input, exiting gracefully."; |