Merge pull request #157 from ejgallego/protect_doc_create

[fleche] Protect Coq document creation

controller/coq_lsp.ml

@@ -224,19 +224,17 @@ let do_open ~state params =
     , string_field "text" document )
   in
   let root_state, workspace = State.(state.root_state, state.workspace) in
-  try
-    let doc =
-      Fleche.Doc.create ~state:root_state ~workspace ~uri ~contents ~version
-    in
+  match
+    Fleche.Doc.create ~state:root_state ~workspace ~uri ~contents ~version
+  with
+  | Coq.Protect.R.Completed (Result.Ok doc) ->
     DocHandle.create ~uri ~doc;
     Check.schedule ~uri
-  with
-  (* Fleche.Doc.create failed due to some Coq Internal Error, we need to use
-     Coq.Protect on that call *)
-  | exn ->
-    let iexn = Exninfo.capture exn in
-    LIO.trace "Fleche.Doc.create" "internal error";
-    Exninfo.iraise iexn
+  (* Maybe send some diagnostics in this case? *)
+  | Coq.Protect.R.Completed (Result.Error (_, msg)) ->
+    let msg = Pp.string_of_ppcmds msg in
+    LIO.trace "Fleche.Doc.create" ("internal error" ^ msg)
+  | Coq.Protect.R.Interrupted -> ()
 
 let do_change params =
   let document = dict_field "textDocument" params in
@@ -497,6 +495,9 @@ let dispatch_message ofmt ~state dict =
   | AbortRequest ->
     () (* XXX: Separate requests from notifications, handle this better *)
   | exn ->
+    (* Note: We should never arrive here from Coq, as every call to Coq should
+       be wrapper in Coq.Protect. So hitting this codepath, is effectively a
+       coq-lsp internal error and should be fixed *)
     let bt = Printexc.get_backtrace () in
     let iexn = Exninfo.capture exn in
     LIO.trace "process_queue"

coq/protect.ml

@@ -1,13 +1,25 @@
+module Error = struct
+  type t = Loc.t option * Pp.t
+end
+
 module R = struct
   type 'a t =
-    | Completed of ('a, Loc.t option * Pp.t) result
+    | Completed of ('a, Error.t) result
     | Interrupted (* signal sent, eval didn't complete *)
-end
 
-let map_loc ~f = function
-  | R.Completed (Error (loc, msg)) ->
-    R.Completed (Error (Option.map f loc, msg))
-  | res -> res
+  let map ~f = function
+    | Completed (Result.Ok r) -> Completed (Result.Ok (f r))
+    | Completed (Result.Error r) -> Completed (Result.Error r)
+    | Interrupted -> Interrupted
+
+  let map_error ~f = function
+    | Completed (Error (loc, msg)) -> Completed (Error (f (loc, msg)))
+    | res -> res
+
+  let map_loc ~f =
+    let f (loc, msg) = (Option.map f loc, msg) in
+    map_error ~f
+end
 
 let eval ~f x =
   try

coq/protect.mli

@@ -1,11 +1,20 @@
+module Error : sig
+  type t = Loc.t option * Pp.t
+end
+
 module R : sig
   type 'a t =
-    | Completed of ('a, Loc.t option * Pp.t) result
+    | Completed of ('a, Error.t) result
     | Interrupted (* signal sent, eval didn't complete *)
+
+  val map : f:('a -> 'b) -> 'a t -> 'b t
+  val map_error : f:(Error.t -> Error.t) -> 'a t -> 'a t
+
+  (** Update the loc stored in the result, this is used by our cache-aware
+      location *)
+  val map_loc : f:(Loc.t -> Loc.t) -> 'a t -> 'a t
 end
 
+(** Eval a function and reify the exceptions. Note [f] _must_ be pure, as in
+    case of anomaly [f] may be re-executed with debug options. *)
 val eval : f:('i -> 'o) -> 'i -> 'o R.t
-
-(** Update the loc stored in the result, this is used by our cache-aware
-    location *)
-val map_loc : f:(Loc.t -> Loc.t) -> 'a R.t -> 'a R.t

fleche/doc.ml

@@ -46,7 +46,8 @@ type t =
 let mk_doc root_state workspace =
   (* XXX This shouldn't be foo *)
   let libname = Names.(DirPath.make [ Id.of_string "foo" ]) in
-  Coq.Init.doc_init ~root_state ~workspace ~libname
+  let f () = Coq.Init.doc_init ~root_state ~workspace ~libname in
+  Coq.Protect.eval ~f ()
 
 let init_loc ~uri = Loc.initial (InFile { dirpath = None; file = uri })
 
@@ -56,16 +57,17 @@ let get_last_text text =
   (List.length lines, String.length last_line, String.length text)
 
 let create ~state ~workspace ~uri ~version ~contents =
-  let end_loc = get_last_text contents in
-  { uri
-  ; contents
-  ; end_loc
-  ; version
-  ; root = mk_doc state workspace
-  ; nodes = []
-  ; diags_dirty = false
-  ; completed = Stopped (init_loc ~uri)
-  }
+  Coq.Protect.R.map (mk_doc state workspace) ~f:(fun root ->
+      let end_loc = get_last_text contents in
+      { uri
+      ; contents
+      ; end_loc
+      ; version
+      ; root
+      ; nodes = []
+      ; diags_dirty = false
+      ; completed = Stopped (init_loc ~uri)
+      })
 
 let recover_up_to_offset doc offset =
   Io.Log.trace "prefix"

fleche/doc.mli

@@ -44,13 +44,14 @@ type t = private
   ; completed : Completion.t
   }
 
+(** Note, [create] is not cached in the Memo.t table *)
 val create :
      state:Coq.State.t
   -> workspace:Coq.Workspace.t
   -> uri:string
   -> version:int
   -> contents:string
-  -> t
+  -> t Coq.Protect.R.t
 
 val bump_version : version:int -> contents:string -> t -> t
 

fleche/memo.ml

@@ -120,7 +120,7 @@ let loc_apply_offset
 let adjust_offset ~stm_loc ~cached_loc res =
   let offset = loc_offset cached_loc stm_loc in
   let f = loc_apply_offset offset in
-  Coq.Protect.map_loc ~f res
+  Coq.Protect.R.map_loc ~f res
 
 let interp_command ~st ~fb_queue stm : _ Stats.t =
   let stm_loc = Coq.Ast.loc stm |> Option.get in