[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:

- calls to admit (this is tricky due to error recovery needing rework
  to fully account for execution)
- calls to `Printer`

controller/coq_lsp.ml

@@ -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/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 (User (loc, msg)))
+    else R.Completed (Error (Anomaly (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,6 @@ 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 *)
+(* let admit ~st = Protect.eval ~f:(admit ~st) () *)

coq/state.mli

@@ -10,10 +10,16 @@ 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
 
-(** Admit an ongoing proof *)
+(* TODO *)
+(* val admit : st:t -> t Protect.R.t *)
+
+(** Admit an ongoing proof, can produce errors *)
 val admit : st:t -> t

fleche/doc.ml

@@ -27,6 +27,7 @@ module Completion = struct
   type t =
     | Yes of Loc.t  (** Location of the last token in the document *)
     | Stopped of Loc.t  (** Location of the last valid token *)
+    | Failed of Loc.t  (** Critical failure, like an anomaly *)
 end
 
 (* Private. A doc is a list of nodes for now. The first element in the list is
@@ -46,8 +47,7 @@ type t =
 let mk_doc root_state workspace =
   (* XXX This shouldn't be foo *)
   let libname = Names.(DirPath.make [ Id.of_string "foo" ]) in
-  let f () = Coq.Init.doc_init ~root_state ~workspace ~libname in
-  Coq.Protect.eval ~f ()
+  Coq.Init.doc_init ~root_state ~workspace ~libname
 
 let init_loc ~uri = Loc.initial (InFile { dirpath = None; file = uri })
 
@@ -164,16 +164,8 @@ let report_progress ~doc last_tok =
 (* let close_doc _modname = () *)
 
 let parse_stm ~st ps =
-  let mode = Coq.State.mode ~st in
-  let st = Coq.State.parsing ~st in
-  let parse ps =
-    (* 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 Coq.Ast.of_coq
-  in
-  Stats.record ~kind:Stats.Kind.Parsing ~f:(Coq.Protect.eval ~f:parse) ps
+  let f ps = Coq.Parsing.parse ~st ps in
+  Stats.record ~kind:Stats.Kind.Parsing ~f ps
 
 (* Read the input stream until a dot or a "end of proof" token is encountered *)
 let parse_to_terminator : unit Pcoq.Entry.t =
@@ -318,8 +310,14 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle =
         | Ok (Some ast) ->
           let () = if Debug.parsing then debug_parsed_sentence ~ast in
           (Process ast, [], time)
-        | Error (loc, msg) ->
-          let err_loc = Option.get loc in
+        | Error (Anomaly (_, msg))
+        | Error (User (None, msg)) ->
+          (* We don't have a better altenative :(, usually missing error loc
+             here means an anomaly, so we stop *)
+          let err_loc = last_tok in
+          let diags = [ mk_diag err_loc 1 msg ] in
+          (EOF (Stopped last_tok), diags, time)
+        | Error (User (Some err_loc, msg)) ->
           let diags = [ mk_diag err_loc 1 msg ] in
           discard_to_dot doc_handle;
           let last_tok = Pcoq.Parsable.loc doc_handle in
@@ -370,7 +368,8 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle =
           in
           let doc = add_node ~node doc in
           stm doc state last_tok_new
-        | Error (err_loc, msg) ->
+        | Error (Anomaly (err_loc, msg) as coq_err)
+        | Error (User (err_loc, msg) as coq_err) ->
           let err_loc = Option.default ast_loc err_loc in
           let diags = [ mk_error_diagnostic ~loc:err_loc ~msg ~ast ] in
           (* FB should be handled by Coq.Protect.eval XXX *)
@@ -390,7 +389,11 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle =
             }
           in
           let doc = add_node ~node doc in
-          stm doc st last_tok_new))
+          match coq_err with
+          | Anomaly _ ->
+            set_completion ~completed:(Failed last_tok_new) doc
+          | User _ ->
+            stm doc st last_tok_new))
   in
   (* Note that nodes and diags in reversed order here *)
   (match doc.nodes with
@@ -439,11 +442,21 @@ let log_resume last_tok =
       asprintf "resuming, from: %d l: %d" last_tok.Loc.ep
         last_tok.Loc.line_nb_last)
 
+let safe_sub s pos len =
+  if pos < 0 || len < 0 || pos > String.length s - len then (
+    Io.Log.trace "string_sub"
+      (Format.asprintf "error for pos: %d len: %d str: %s" pos len s);
+    s)
+  else String.sub s pos len
+
 let check ~ofmt:_ ~doc ~fb_queue =
   match doc.completed with
   | Yes _ ->
     Io.Log.trace "check" "resuming, completed=yes, nothing to do";
     doc
+  | Failed _ ->
+    Io.Log.trace "check" "can't resume, failed=yes, nothing to do";
+    doc
   | Stopped last_tok ->
     log_resume last_tok;
     let uri, version, contents = (doc.uri, doc.version, doc.contents) in
@@ -453,7 +466,8 @@ let check ~ofmt:_ ~doc ~fb_queue =
     let resume_loc = CLexer.after last_tok in
     let offset = resume_loc.bp in
     let processed_content =
-      String.(sub processed_content offset (length processed_content - offset))
+      safe_sub processed_content offset
+        (String.length processed_content - offset)
     in
     let handle =
       Pcoq.Parsable.make ~loc:resume_loc
@@ -473,8 +487,9 @@ let check ~ofmt:_ ~doc ~fb_queue =
         match doc.completed with
         | Yes loc -> loc
         | Stopped loc -> loc
+        | Failed loc -> loc
       in
-      Format.asprintf "done [%.2f]: document fully checked %s" timestamp
+      Format.asprintf "done [%.2f]: document fully checked up to %s" timestamp
         (Coq.Ast.pr_loc loc)
     in
     Io.Log.trace "check" end_msg;

fleche/doc.mli

@@ -31,6 +31,7 @@ module Completion : sig
   type t =
     | Yes of Loc.t  (** Location of the last token in the document *)
     | Stopped of Loc.t  (** Location of the last valid token *)
+    | Failed of Loc.t  (** Critical failure, like an anomaly *)
 end
 
 type t = private

fleche/info.ml

@@ -181,10 +181,15 @@ module Make (P : Point) : S with module P := P = struct
     let node = find ~doc ~point approx in
     Option.bind node (fun node -> node.Doc.ast)
 
+  let in_state ~st ~f node =
+    match Coq.State.in_state ~st ~f node with
+    | Coq.Protect.R.Completed (Result.Ok res) -> res
+    | Coq.Protect.R.Completed (Result.Error _) | Coq.Protect.R.Interrupted ->
+      None
+
   let goals ~doc ~point approx =
     find ~doc ~point approx
-    |> obind (fun node ->
-           Coq.State.in_state ~st:node.Doc.state ~f:pr_goal node.Doc.state)
+    |> obind (fun node -> in_state ~st:node.Doc.state ~f:pr_goal node.Doc.state)
 
   let messages ~doc ~point approx =
     find ~doc ~point approx |> Option.map (fun node -> node.Doc.messages)
@@ -205,7 +210,7 @@ module Make (P : Point) : S with module P := P = struct
   let completion ~doc ~point prefix =
     find ~doc ~point Exact
     |> obind (fun node ->
-           Coq.State.in_state ~st:node.Doc.state prefix ~f:(fun prefix ->
+           in_state ~st:node.Doc.state prefix ~f:(fun prefix ->
                to_qualid prefix
                |> obind (fun p ->
                       Nametab.completion_canditates p

fleche/memo.mli

@@ -17,6 +17,9 @@ val interp_command :
   -> Coq.State.t Coq.Interp.interp_result Stats.t
 
 val interp_admitted : st:Coq.State.t -> Coq.State.t
+(* TODO *)
+(* val interp_admitted : st:Coq.State.t -> Coq.State.t Coq.Protect.R.t *)
+
 val mem_stats : unit -> int
 val load_from_disk : file:string -> unit
 val save_to_disk : file:string -> unit