[coq] Protect all base API calls, stop checking on anomaly

Work on tricky issues made me realize that we don't handle anomalies
and Coq errors still in the best way, thus #91 is not really solved.

There are 2 issues this PR solves:
- goal printing can raise an anomalies and errors, due
  to setting state and printing,
- it is safer to stop checking and set the document to failed when an
  anomaly happens (tho we could make this configurable).

Thus, we go full principled in terms of API and make `Protect`
mandatory on the exported APIs from `coq` library.

We also introduce a `Failed` state that prevents further checking of
that document without having finished it.

Really fixes #91, and a step towards #153

TODO: protect calls to admit, but we leave this for a further PR as it
is quite tricky due to error recovery needing rework to fully account
for `Protect.R` results.

CHANGES.md

@@ -1,3 +1,9 @@
+# coq-lsp 0.1.3: 
+------------------------
+
+ - Much improved handling of Coq fatal errors, the server is now
+   hardened against them (@ejgallego, #155, #157, #160, fixes #91)
+
 # coq-lsp 0.1.2: Message
 ------------------------
 

controller/coq_lsp.ml

@@ -210,8 +210,8 @@ module Check = struct
   let completed uri =
     let doc = DocHandle.find_doc ~uri in
     match doc.completed with
-    | Yes _ -> true
-    | _ -> false
+    | Yes _ | Failed _ -> true
+    | Stopped _ -> false
 
   let schedule ~uri = pending := Some uri
 end
@@ -231,7 +231,8 @@ let do_open ~state params =
     DocHandle.create ~uri ~doc;
     Check.schedule ~uri
   (* Maybe send some diagnostics in this case? *)
-  | Coq.Protect.R.Completed (Result.Error (_, msg)) ->
+  | Coq.Protect.R.Completed (Result.Error (Anomaly (_, msg)))
+  | Coq.Protect.R.Completed (Result.Error (User (_, msg))) ->
     let msg = Pp.string_of_ppcmds msg in
     LIO.trace "Fleche.Doc.create" ("internal error" ^ msg)
   | Coq.Protect.R.Interrupted -> ()
@@ -306,7 +307,7 @@ let do_symbols ofmt ~id params =
     let slist = Coq.Ast.grab_definitions f ast in
     let msg = LSP.mk_reply ~id ~result:(`List slist) in
     LIO.send_json ofmt msg
-  | Stopped _ ->
+  | Stopped _ | Failed _ ->
     (* -32802 = RequestFailed | -32803 = ServerCancelled ; *)
     let code = -32802 in
     let message = "Document is not ready" in
@@ -319,7 +320,7 @@ let do_position_request ofmt ~id params ~handler =
   let in_range =
     match doc.completed with
     | Yes _ -> true
-    | Stopped loc ->
+    | Failed loc | Stopped loc ->
       line < loc.line_nb_last
       || (line = loc.line_nb_last && col <= loc.ep - loc.bol_pos_last)
   in

coq/init.ml

@@ -72,7 +72,7 @@ let coq_init opts =
 (**************************************************************************)
 
 (* Inits the context for a document *)
-let doc_init ~root_state ~workspace ~libname =
+let doc_init ~root_state ~workspace ~libname () =
   (* Lsp.Io.log_error "init" "starting"; *)
   Vernacstate.unfreeze_interp_state (State.to_coq root_state);
 
@@ -83,3 +83,6 @@ let doc_init ~root_state ~workspace ~libname =
 
   (* We return the state at this point! *)
   Vernacstate.freeze_interp_state ~marshallable:false |> State.of_coq
+
+let doc_init ~root_state ~workspace ~libname =
+  Protect.eval ~f:(doc_init ~root_state ~workspace ~libname) ()

coq/init.mli

@@ -33,4 +33,4 @@ val doc_init :
      root_state:State.t
   -> workspace:Workspace.t
   -> libname:Names.DirPath.t
-  -> State.t
+  -> State.t Protect.R.t

coq/interp.ml

@@ -50,18 +50,15 @@ let marshal_out f oc res =
     | Ok res ->
       Marshal.to_channel oc 0 [];
       f oc res.Info.res
-    | Error (loc, msg) ->
+    | Error _err ->
       Marshal.to_channel oc 1 [];
-      Marshal.to_channel oc loc [];
-      Marshal.to_channel oc msg [];
+      (* Marshal.to_channel oc loc []; *)
+      (* Marshal.to_channel oc msg []; *)
       ())
 
-let marshal_in f ic =
-  let tag : int = Marshal.from_channel ic in
-  if tag = 0 then
-    let res = f ic in
-    Protect.R.Completed (Ok { Info.res; feedback = [] })
-  else
-    let loc : Loc.t option = Marshal.from_channel ic in
-    let msg : Pp.t = Marshal.from_channel ic in
-    Protect.R.Completed (Error (loc, msg))
+(* Needs to be implemeted by Protect.marshal_in *)
+let marshal_in _f _ic = Obj.magic 0
+(* let tag : int = Marshal.from_channel ic in if tag = 0 then let res = f ic in
+   Protect.R.Completed (Ok { Info.res; feedback = [] }) else let loc : Loc.t
+   option = Marshal.from_channel ic in let msg : Pp.t = Marshal.from_channel ic
+   in Protect.R.Completed (Error (User (loc, msg))) *)

coq/parsing.ml

@@ -0,0 +1,10 @@
+let parse ~st ps =
+  let mode = State.mode ~st in
+  let st = State.parsing ~st in
+  (* Coq is missing this, so we add it here. Note that this MUST run inside
+     coq_protect *)
+  Control.check_for_interrupt ();
+  Vernacstate.Parser.parse st Pvernac.(main_entry mode) ps
+  |> Option.map Ast.of_coq
+
+let parse ~st ps = Protect.eval ~f:(parse ~st) ps

coq/parsing.mli

@@ -0,0 +1 @@
+val parse : st:State.t -> Pcoq.Parsable.t -> Ast.t option Protect.R.t

coq/print.ml

@@ -0,0 +1,8 @@
+let pr_ltype_env ~goal_concl_style env sigma x =
+  Printer.pr_ltype_env ~goal_concl_style env sigma x
+
+let pr_ltype_env ~goal_concl_style env sigma x =
+  let f = pr_ltype_env ~goal_concl_style env sigma in
+  match Protect.eval ~f x with
+  | Protect.R.Completed (Ok pr) -> pr
+  | _ -> Pp.str "printer failed!"

coq/print.mli

@@ -0,0 +1,2 @@
+val pr_ltype_env :
+  goal_concl_style:bool -> Environ.env -> Evd.evar_map -> Constr.t -> Pp.t

coq/protect.ml

@@ -1,5 +1,13 @@
 module Error = struct
-  type t = Loc.t option * Pp.t
+  type payload = Loc.t option * Pp.t
+
+  type t =
+    | User of payload
+    | Anomaly of payload
+
+  let map ~f = function
+    | User e -> User (f e)
+    | Anomaly e -> Anomaly (f e)
 end
 
 module R = struct
@@ -13,7 +21,7 @@ module R = struct
     | Interrupted -> Interrupted
 
   let map_error ~f = function
-    | Completed (Error (loc, msg)) -> Completed (Error (f (loc, msg)))
+    | Completed (Error e) -> Completed (Error (Error.map ~f e))
     | res -> res
 
   let map_loc ~f =
@@ -31,4 +39,5 @@ let eval ~f x =
     let e, info = Exninfo.capture exn in
     let loc = Loc.(get_loc info) in
     let msg = CErrors.iprint (e, info) in
-    R.Completed (Error (loc, msg))
+    if CErrors.is_anomaly e then R.Completed (Error (Anomaly (loc, msg)))
+    else R.Completed (Error (User (loc, msg)))

coq/protect.mli

@@ -1,14 +1,18 @@
 module Error : sig
-  type t = Loc.t option * Pp.t
+  type payload = Loc.t option * Pp.t
+
+  type t = private
+    | User of payload
+    | Anomaly of payload
 end
 
 module R : sig
-  type 'a t =
+  type 'a t = private
     | 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
+  val map_error : f:(Error.payload -> Error.payload) -> 'a t -> 'a t
 
   (** Update the loc stored in the result, this is used by our cache-aware
       location *)

coq/state.ml

@@ -77,17 +77,20 @@ let mode ~st =
 let parsing ~st = st.Vernacstate.parsing
 let lemmas ~st = st.Vernacstate.lemmas
 
-let in_state ~st ~f a =
-  Vernacstate.unfreeze_interp_state st;
-  f a
-
 let drop_proofs ~st =
   let open Vernacstate in
   { st with
     lemmas =
       Option.cata (fun s -> snd @@ Vernacstate.LemmaStack.pop s) None st.lemmas
   }
 
+let in_state ~st ~f a =
+  let f a =
+    Vernacstate.unfreeze_interp_state st;
+    f a
+  in
+  Protect.eval ~f a
+
 let admit ~st =
   let () = Vernacstate.unfreeze_interp_state st in
   match st.Vernacstate.lemmas with
@@ -99,3 +102,7 @@ let admit ~st =
     let program = NeList.map_head (fun _ -> pm) st.Vernacstate.program in
     let st = Vernacstate.freeze_interp_state ~marshallable:false in
     { st with lemmas; program }
+
+(* TODO: implement protect once error recovery supports a failing recovery
+   execution *)
+(* let admit ~st = Protect.eval ~f:(admit ~st) () *)

coq/state.mli

@@ -10,7 +10,10 @@ val hash : t -> int
 val mode : st:t -> Pvernac.proof_mode option
 val parsing : st:t -> Vernacstate.Parser.t
 val lemmas : st:t -> Vernacstate.LemmaStack.t option
-val in_state : st:t -> f:('a -> 'b) -> 'a -> 'b
+
+(** Execute a command in state [st]. Unfortunately this can produce anomalies as
+    Coq state setting is imperative, so we need to wrap it in protect. *)
+val in_state : st:t -> f:('a -> 'b) -> 'a -> 'b Protect.R.t
 
 (** Drop the proofs from the state *)
 val drop_proofs : st:t -> t