[coq] Protect all base API calls

Indeed I didn't realize that goal printing could raise an anomaly, due
to setting state; thus #91 is not fully fixed.

So we go full principled and make `Protect` mandatory on the exported
APIs.

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

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/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/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

@@ -46,8 +46,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 +163,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 =
@@ -319,7 +310,9 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle =
           let () = if Debug.parsing then debug_parsed_sentence ~ast in
           (Process ast, [], time)
         | Error (loc, msg) ->
-          let err_loc = Option.get loc in
+          (* We don't have a better altenative :(, usually missing
+             error loc here means an anomaly *)
+          let err_loc = Option.default last_tok loc in
           let diags = [ mk_diag err_loc 1 msg ] in
           discard_to_dot doc_handle;
           let last_tok = Pcoq.Parsable.loc doc_handle in
@@ -439,6 +432,13 @@ 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 > 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 _ ->
@@ -453,7 +453,7 @@ 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

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