From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- ide/coq.ml | 462 ++++++++++++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 364 insertions(+), 98 deletions(-) (limited to 'ide/coq.ml') diff --git a/ide/coq.ml b/ide/coq.ml index 1d1a7dd0..b7753e6e 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -1,12 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 0 && arg.[len - 1] = '\r' then String.sub arg 0 (len - 1) else arg in @@ -112,8 +113,7 @@ let rec filter_coq_opts args = filtered_args := read_all_lines oc; errlines := read_all_lines ec; match Unix.close_process_full (oc,ic,ec) with - | Unix.WEXITED 0 -> - List.iter check_remaining_opt !filtered_args; !filtered_args + | Unix.WEXITED 0 -> !filtered_args | Unix.WEXITED 127 -> asks_for_coqtop args | _ -> display_coqtop_answer cmd (!filtered_args @ !errlines) with Sys_error _ -> asks_for_coqtop args @@ -125,7 +125,7 @@ and asks_for_coqtop args = ~message_type:`QUESTION ~buttons:GWindow.Buttons.yes_no () in match pb_mes#run () with | `YES -> - let () = !Preferences.current.Preferences.cmd_coqtop <- None in + let () = current.cmd_coqtop <- None in let () = custom_coqtop := None in let () = pb_mes#destroy () in filter_coq_opts args @@ -151,37 +151,106 @@ let print_status = function let check_connection args = let lines = ref [] in let argstr = String.concat " " (List.map Filename.quote args) in - let cmd = Filename.quote (coqtop_path ()) ^ " -batch " ^ argstr in + let cmd = Filename.quote (coqtop_path ()) ^ " -batch -ideslave " ^ argstr in let cmd = requote cmd in try - let ic = Unix.open_process_in cmd in - lines := read_all_lines ic; - match Unix.close_process_in ic with + let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in + lines := read_all_lines oc @ read_all_lines ec; + match Unix.close_process_full (oc,ic,ec) with | Unix.WEXITED 0 -> () (* coqtop seems ok *) | st -> raise (WrongExitStatus (print_status st)) with e -> connection_error cmd !lines e +(** Useful stuff *) + +let ignore_error f arg = + try ignore (f arg) with _ -> () + +(** An abstract copy of unit. + This will help ensuring that we do not forget to finally call + continuations when building tasks in other modules. *) + +type void = Void + +(** ccb : existential type for a (call + callback) type. + + Reference: http://alan.petitepomme.net/cwn/2004.01.13.html + To rewrite someday with GADT. *) + +type 'a poly_ccb = 'a Xmlprotocol.call * ('a Interface.value -> void) +type 't scoped_ccb = { bind_ccb : 'a. 'a poly_ccb -> 't } +type ccb = { open_ccb : 't. 't scoped_ccb -> 't } + +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) + (** * The structure describing a coqtop sub-process *) -type coqtop = { - pid : int; (* Unix process id *) - cout : in_channel ; - cin : out_channel ; - sup_args : string list; +let gio_channel_of_descr_socket = ref Glib.Io.channel_of_descr + +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 x = try Glib.Io.remove x with Glib.GError _ -> () + 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 + +module CoqTop = Spawn.Async(GlibMainLoop) + +type handle = { + proc : CoqTop.process; + xml_oc : Xml_printer.t; + mutable alive : bool; + mutable waiting_for : (ccb * logger) option; (* last call + callback + log *) } -(** * Count of all active coqtops *) +(** Coqtop process status : + - New : a process has been spawned, but not initialized via [init_coqtop]. + It will reject tasks given via [try_grab]. + - Ready : no current task, accepts new tasks via [try_grab]. + - Busy : has accepted a task via [init_coqtop] or [try_grab], + It will reject other tasks for the moment + - Closed : the coqide buffer has been closed, we discard any further task. +*) -let toplvl_ctr = ref 0 +type status = New | Ready | Busy | Closed -let toplvl_ctr_mtx = Mutex.create () +type 'a task = handle -> ('a -> void) -> void -let coqtop_zombies () = - Mutex.lock toplvl_ctr_mtx; - let res = !toplvl_ctr in - Mutex.unlock toplvl_ctr_mtx; - res +type reset_kind = Planned | Unexpected + +type coqtop = { + (* non quoted command-line arguments of coqtop *) + mutable sup_args : string list; + (* called whenever coqtop dies *) + mutable reset_handler : reset_kind -> unit task; + (* called whenever coqtop sends a feedback message *) + mutable feedback_handler : Feedback.feedback -> unit; + (* actual coqtop process and its status *) + mutable handle : handle; + mutable status : status; +} +let return (x : 'a) : 'a task = + (); fun _ k -> k x + +let bind (m : 'a task) (f : 'a -> 'b task) : 'b task = + (); fun h k -> m h (fun x -> f x h k) + +let seq (m : unit task) (n : 'a task) : 'a task = + (); fun h k -> m h (fun () -> n h k) + +let lift (f : unit -> 'a) : 'a task = + (); fun _ k -> k (f ()) (** * Starting / signaling / ending a real coqtop sub-process *) @@ -215,107 +284,304 @@ let coqtop_zombies () = 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; - Unix.close top2ide_w; - let oc = Unix.out_channel_of_descr ide2top_w in - let ic = Unix.in_channel_of_descr top2ide_r in - set_binary_mode_out oc true; - set_binary_mode_in ic true; - (pid,ic,oc) +exception TubeError of string +exception AnswerWithoutRequest of string + +let rec check_errors = function +| [] -> () +| (`IN | `PRI) :: conds -> check_errors conds +| `ERR :: _ -> raise (TubeError "ERR") +| `HUP :: _ -> raise (TubeError "HUP") +| `NVAL :: _ -> raise (TubeError "NVAL") +| `OUT :: _ -> raise (TubeError "OUT") + +let handle_intermediate_message handle xml = + let message = Pp.to_message xml in + let level = message.Pp.message_level in + let content = message.Pp.message_content in + let logger = match handle.waiting_for with + | Some (_, l) -> l + | None -> function + | Pp.Error -> Minilib.log ~level:`ERROR + | Pp.Info -> Minilib.log ~level:`INFO + | Pp.Notice -> Minilib.log ~level:`NOTICE + | Pp.Warning -> Minilib.log ~level:`WARNING + | Pp.Debug _ -> Minilib.log ~level:`DEBUG + in + logger level content + +let handle_feedback feedback_processor xml = + let feedback = Feedback.to_feedback xml in + feedback_processor feedback + +let handle_final_answer handle xml = + let () = Minilib.log "Handling coqtop answer" in + let ccb = match handle.waiting_for with + | None -> raise (AnswerWithoutRequest (Xml_printer.to_string_fmt xml)) + | Some (c, _) -> c in + let () = handle.waiting_for <- None in + with_ccb ccb { bind_ccb = fun (c, f) -> f (Xmlprotocol.to_answer c xml) } + +type input_state = { + mutable fragment : string; + mutable lexerror : int option; +} + +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 + state.fragment <- s; + let lex = Lexing.from_string s in + let p = Xml_parser.make (Xml_parser.SLexbuf lex) in + let rec loop () = + let xml = Xml_parser.parse p in + let l_end = Lexing.lexeme_end lex in + state.fragment <- String.sub s l_end (String.length s - l_end); + state.lexerror <- None; + if Pp.is_message xml then begin + handle_intermediate_message handle xml; + loop () + end else if Feedback.is_feedback xml then begin + handle_feedback feedback_processor xml; + loop () + end else begin + ignore (handle_final_answer handle xml) + end + in + try loop () + with Xml_parser.Error _ as e -> + (* Parsing error at the end of s : we have only received a part of + an xml answer. We store the current fragment for later *) + 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 *) + 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 + +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 unsafe_handle_input h feedback_processor state conds ~read_all; true + with e -> + 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 respawner feedback_processor = + let prog = coqtop_path () in + let args = Array.of_list ("-async-proofs" :: "on" :: "-ideslave" :: args) in + let env = + match !Flags.ideslave_coqtop_flags with + | None -> None + | Some s -> + let open Str in + let open Array in + let opts = split_delim (regexp ",") s in + begin try + let erex = regexp "^extra-env=" in + let echunk = List.find (fun s -> string_match erex s 0) opts in + Some (append + (of_list (split_delim (regexp ";") (replace_first erex "" echunk))) + (Unix.environment ())) + with Not_found -> None end in + bind_self_as (fun handle -> + let proc, oc = + CoqTop.spawn ?env prog args (input_watch handle respawner feedback_processor) in + { + proc; + xml_oc = Xml_printer.make (Xml_printer.TChannel oc); + alive = true; + waiting_for = None; + }) + +(** This clears any potentially remaining open garbage. *) +let clear_handle h = + if h.alive then begin + (* invalidate the old handle *) + CoqTop.kill h.proc; + ignore(CoqTop.wait h.proc); + h.alive <- false; + end + +let mkready coqtop = + fun () -> coqtop.status <- Ready; Void + +let rec respawn_coqtop ?(why=Unexpected) coqtop = + clear_handle coqtop.handle; + 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; + ignore (coqtop.reset_handler why coqtop.handle (mkready coqtop)) let spawn_coqtop sup_args = - Mutex.lock toplvl_ctr_mtx; - try - let prog = coqtop_path () in - let args = Array.of_list (prog :: "-ideslave" :: sup_args) in - let (pid,ic,oc) = open_process_pid prog args in - incr toplvl_ctr; - Mutex.unlock toplvl_ctr_mtx; - { pid = pid; cin = oc; cout = ic ; sup_args = sup_args } - with e -> - Mutex.unlock toplvl_ctr_mtx; - raise e + 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; + }) -let respawn_coqtop coqtop = spawn_coqtop coqtop.sup_args +let set_reset_handler coqtop hook = coqtop.reset_handler <- hook -let interrupter = ref (fun pid -> Unix.kill pid Sys.sigint) -let killer = ref (fun pid -> Unix.kill pid Sys.sigkill) +let set_feedback_handler coqtop hook = coqtop.feedback_handler <- hook + +let is_computing coqtop = (coqtop.status = Busy) + +(* For closing a coqtop, we don't try to send it a Quit call anymore, + but rather close its channels: + - a listening coqtop will handle this just as a Quit call + - a busy coqtop will anyway have to be killed *) + +let close_coqtop coqtop = + coqtop.status <- Closed; + clear_handle coqtop.handle + +let reset_coqtop coqtop = respawn_coqtop ~why:Planned coqtop let break_coqtop coqtop = - try !interrupter coqtop.pid - with _ -> prerr_endline "Error while sending Ctrl-C" - -let kill_coqtop coqtop = - let pid = coqtop.pid in - begin - try !killer pid - with _ -> prerr_endline "Kill -9 failed. Process already terminated ?" - end; - try - ignore (Unix.waitpid [] pid); - Mutex.lock toplvl_ctr_mtx; decr toplvl_ctr; Mutex.unlock toplvl_ctr_mtx - with _ -> prerr_endline "Error while waiting for child" + try !interrupter (CoqTop.unixpid coqtop.handle.proc) + with _ -> Minilib.log "Error while sending Ctrl-C" -(** * Calls to coqtop *) +let get_arguments coqtop = coqtop.sup_args -(** Cf [Ide_intf] for more details *) +let set_arguments coqtop args = + coqtop.sup_args <- args; + reset_coqtop coqtop + +let process_task coqtop task = + assert (coqtop.status = Ready || coqtop.status = New); + coqtop.status <- Busy; + try ignore (task coqtop.handle (mkready coqtop)) + with e -> + Minilib.log ("Coqtop writer failed, resetting: " ^ Printexc.to_string e); + if coqtop.status <> Closed then respawn_coqtop coqtop -let p = Xml_parser.make () -let () = Xml_parser.check_eof p false +let try_grab coqtop task abort = + match coqtop.status with + |Closed -> () + |Busy|New -> abort () + |Ready -> process_task coqtop task -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 c : 'a Interface.value) +let init_coqtop coqtop task = + assert (coqtop.status = New); + process_task coqtop task -let interp coqtop ?(raw=false) ?(verbose=true) i s = - eval_call coqtop (Ide_intf.interp (i,raw,verbose,s)) -let rewind coqtop i = eval_call coqtop (Ide_intf.rewind i) -let inloadpath coqtop s = eval_call coqtop (Ide_intf.inloadpath s) -let mkcases coqtop s = eval_call coqtop (Ide_intf.mkcases s) -let status coqtop = eval_call coqtop (Ide_intf.status ()) -let hints coqtop = eval_call coqtop (Ide_intf.hints ()) +(** * Calls to coqtop *) + +(** Cf [Ide_intf] for more details *) + +type 'a query = 'a Interface.value task + +let eval_call ?(logger=default_logger) call handle k = + (** Send messages to coqtop and prepare the decoding of the answer *) + Minilib.log ("Start eval_call " ^ Xmlprotocol.pr_call call); + assert (handle.alive && handle.waiting_for = None); + handle.waiting_for <- Some (mk_ccb (call,k), logger); + Xml_printer.print handle.xml_oc (Xmlprotocol.of_call call); + Minilib.log "End eval_call"; + Void + +let add ?(logger=default_logger) x = eval_call ~logger (Xmlprotocol.add x) +let edit_at i = eval_call (Xmlprotocol.edit_at i) +let query ?(logger=default_logger) x = eval_call ~logger (Xmlprotocol.query x) +let mkcases s = eval_call (Xmlprotocol.mkcases s) +let status ?logger force = eval_call ?logger (Xmlprotocol.status force) +let hints x = eval_call (Xmlprotocol.hints x) +let search flags = eval_call (Xmlprotocol.search flags) +let init x = eval_call (Xmlprotocol.init x) +let stop_worker x = eval_call (Xmlprotocol.stop_worker x) module PrintOpt = struct type t = string list + + (* Boolean options *) + let implicit = ["Printing"; "Implicit"] let coercions = ["Printing"; "Coercions"] - let raw_matching = ["Printing"; "Matching"; "Synth"] + let raw_matching = ["Printing"; "Matching"] let notations = ["Printing"; "Notations"] let all_basic = ["Printing"; "All"] let existential = ["Printing"; "Existential"; "Instances"] let universes = ["Printing"; "Universes"] - let state_hack = Hashtbl.create 11 - let _ = List.iter (fun opt -> Hashtbl.add state_hack opt false) - [ implicit; coercions; raw_matching; notations; all_basic; existential; universes ] + type bool_descr = { opts : t list; init : bool; label : string } + + let bool_items = [ + { opts = [implicit]; init = false; label = "Display _implicit arguments" }; + { opts = [coercions]; init = false; label = "Display _coercions" }; + { opts = [raw_matching]; init = true; + label = "Display raw _matching expressions" }; + { opts = [notations]; init = true; label = "Display _notations" }; + { opts = [all_basic]; init = false; + label = "Display _all basic low-level contents" }; + { opts = [existential]; init = false; + label = "Display _existential variable instances" }; + { opts = [universes]; init = false; label = "Display _universe levels" }; + { opts = [all_basic;existential;universes]; init = false; + label = "Display all _low-level contents" } + ] + + (** The current status of the boolean options *) + + let current_state = Hashtbl.create 11 + + let set opt v = Hashtbl.replace current_state opt v + + let reset () = + let init_descr d = List.iter (fun o -> set o d.init) d.opts in + List.iter init_descr bool_items + + let _ = reset () + + (** Integer option *) + + let width = ["Printing"; "Width"] + let width_state = ref None + let set_printing_width w = width_state := Some w - let set coqtop options = - let () = List.iter (fun (name, v) -> Hashtbl.replace state_hack name v) options in - let options = List.map (fun (name, v) -> (name, Interface.BoolValue v)) options in - match eval_call coqtop (Ide_intf.set_options options) with - | Interface.Good () -> () - | _ -> raise (Failure "Cannot set options.") + (** Transmitting options to coqtop *) - let enforce_hack coqtop = - let elements = Hashtbl.fold (fun opt v acc -> (opt, v) :: acc) state_hack [] in - set coqtop elements + let enforce h k = + let mkopt o v acc = (o, Interface.BoolValue v) :: acc in + let opts = Hashtbl.fold mkopt current_state [] in + let opts = (width, Interface.IntValue !width_state) :: opts in + eval_call (Xmlprotocol.set_options opts) h + (function + | Interface.Good () -> k () + | _ -> failwith "Cannot set options. Resetting coqtop") end -let goals coqtop = - let () = PrintOpt.enforce_hack coqtop in - eval_call coqtop (Ide_intf.goals ()) +let goals ?logger x h k = + PrintOpt.enforce h (fun () -> eval_call ?logger (Xmlprotocol.goals x) h k) -let evars coqtop = - let () = PrintOpt.enforce_hack coqtop in - eval_call coqtop (Ide_intf.evars ()) +let evars x h k = + PrintOpt.enforce h (fun () -> eval_call (Xmlprotocol.evars x) h k) -- cgit v1.2.3