Imported Upstream version 8.5~beta1+dfsg

1 files changed, 364 insertions, 98 deletions

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     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Ideutils
+open Preferences
 
 (** * Version and date *)
 
@@ -53,7 +54,7 @@ let rec read_all_lines in_chan =
     let arg = input_line in_chan in
     let len = String.length arg  in
     let arg =
-      if arg.[len - 1] = '\r' then
+      if len > 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)