[internal] [fleche] Absorb errors on document creation and update.

`Doc.t` API has changed: a document that fails to create or update is
still valid, but will be set to the right failed state, instead of
having the caller handle that case.

This is an important API change in order to implement the upcoming
ability to re-check documents on environment changes, which is
necessary for jsCoq style hotload, auto-build, to name a few.

CHANGES.md

@@ -21,6 +21,11 @@
    provide official support for speculative execution (@ejgallego, #600)
  - fix some cases where interrupted computations where memoized
    (@ejgallego, #603)
+ - [internal] Flèche [Doc.t] API will now absorb errors on document
+   update and creation into the document itself. Thus, a document that
+   failed to create or update is still valid, but in the right failed
+   state. This is a much needed API change for a lot of use cases
+   (@ejgallego, #604)
 
 # coq-lsp 0.1.8: Trick-or-treat
 -------------------------------

fleche/contents.ml

@@ -139,3 +139,8 @@ let make ~uri ~raw =
   | R.Ok text ->
     let last, lines = get_last_text text in
     R.Ok { raw; text; last; lines }
+
+let make_raw ~raw =
+  let text = raw in
+  let last, lines = get_last_text text in
+  { raw; text; last; lines }

fleche/contents.mli

@@ -25,4 +25,9 @@ module R : sig
   val map : f:('a -> 'b) -> 'a t -> 'b t
 end
 
+(** Process contents *)
 val make : uri:Lang.LUri.File.t -> raw:string -> t R.t
+
+(** Make an object of type [t] but don't process the text, this is only used
+    internally to still provide some contents when [make] fails. *)
+val make_raw : raw:string -> t

fleche/doc.ml

@@ -262,66 +262,127 @@ let init_fname ~uri =
 
 let init_loc ~uri = Loc.initial (init_fname ~uri)
 
-let process_init_feedback ~stats range state messages =
+(* default range for the node that contains the init feedback errors *)
+let drange =
+  let open Lang in
+  let start = Point.{ line = 0; character = 0; offset = 0 } in
+  let end_ = Point.{ line = 0; character = 1; offset = 1 } in
+  Range.{ start; end_ }
+
+let process_init_feedback ~lines ~stats state feedback =
+  let messages = List.map (Node.Message.feedback_to_message ~lines) feedback in
   if not (CList.is_empty messages) then
-    let diags, messages = Diags.of_messages ~drange:range messages in
+    let diags, messages = Diags.of_messages ~drange messages in
     let parsing_time = 0.0 in
     let { Gc.major_words = mw_prev; _ } = Gc.quick_stat () in
     let info =
       Node.Info.make ~parsing_time ~mw_prev ~mw_after:mw_prev ~stats ()
     in
+    let range = drange in
     [ { Node.range; ast = None; state; diags; messages; info } ]
   else []
 
 (* Memoized call to [Coq.Init.doc_init] *)
 let mk_doc ~env ~uri = Memo.Init.eval (env.Env.init, env.workspace, uri)
 
+(* Create empty doc, in state [~completed] *)
+let empty_doc ~uri ~contents ~version ~env ~root ~nodes ~completed =
+  let lines = contents.Contents.lines in
+  let init_loc = init_loc ~uri in
+  let init_range = Coq.Utils.to_range ~lines init_loc in
+  let toc = CString.Map.empty in
+  let diags_dirty = not (CList.is_empty nodes) in
+  let completed = completed init_range in
+  { uri; contents; toc; version; env; root; nodes; diags_dirty; completed }
+
+let error_doc ~loc ~message ~uri ~contents ~version ~env ~completed =
+  let feedback = [ (loc, 1, Pp.str message) ] in
+  let root = env.Env.init in
+  let nodes = [] in
+  (empty_doc ~uri ~version ~contents ~env ~root ~nodes ~completed, feedback)
+
+let conv_error_doc ~raw ~uri ~version ~env ~root ~completed err =
+  let contents = Contents.make_raw ~raw in
+  let lines = contents.lines in
+  let err = (None, 1, Pp.(str "Error in document conversion: " ++ str err)) in
+  let stats = Stats.dump () in
+  let nodes = process_init_feedback ~lines ~stats root [ err ] in
+  empty_doc ~uri ~version ~env ~root ~nodes ~completed ~contents
+
 let create ~env ~uri ~version ~contents =
   let () = Stats.reset () in
-  let { Coq.Protect.E.r; feedback } = mk_doc ~env ~uri in
-  Coq.Protect.R.map r ~f:(fun root ->
-      let init_loc = init_loc ~uri in
-      let lines = contents.Contents.lines in
-      let init_range = Coq.Utils.to_range ~lines init_loc in
-      let feedback =
-        List.map (Node.Message.feedback_to_message ~lines) feedback
+  let root = mk_doc ~env ~uri in
+  Coq.Protect.E.map root ~f:(fun root ->
+      let nodes = [] in
+      let completed range = Completion.Stopped range in
+      empty_doc ~uri ~contents ~version ~env ~root ~nodes ~completed)
+
+(** Create a permanently failed doc, to be removed when we drop 8.16 support *)
+let handle_failed_permanent ~env ~uri ~version ~contents =
+  let completed range = Completion.FailedPermanent range in
+  let loc, message = (None, "Document Failed Permanently due to Coq bugs") in
+  let doc, feedback =
+    error_doc ~loc ~message ~uri ~contents ~version ~env ~completed
+  in
+  let stats = Stats.dump () in
+  let nodes =
+    let lines = contents.Contents.lines in
+    process_init_feedback ~lines ~stats env.Env.init feedback @ doc.nodes
+  in
+  let diags_dirty = not (CList.is_empty nodes) in
+  { doc with nodes; diags_dirty }
+
+(** Try to create a doc, if Coq execution fails, create a failed doc with the
+    corresponding errors; for now we refine the contents step as to better setup
+    the initial document. *)
+let handle_doc_creation_exec ~env ~uri ~version ~contents =
+  let completed range = Completion.Failed range in
+  let { Coq.Protect.E.r; feedback } = create ~env ~uri ~version ~contents in
+  let doc, extra_feedback =
+    match r with
+    | Interrupted ->
+      let message = "Document Creation Interrupted!" in
+      let loc = None in
+      error_doc ~loc ~message ~uri ~version ~contents ~env ~completed
+    | Completed (Error (User (loc, err_msg)))
+    | Completed (Error (Anomaly (loc, err_msg))) ->
+      let message =
+        Format.asprintf "Doc.create, internal error: @[%a@]" Pp.pp_with err_msg
       in
-      let stats = Stats.dump () in
-      let toc = CString.Map.empty in
-      let nodes = process_init_feedback ~stats init_range root feedback in
-      let diags_dirty = not (CList.is_empty nodes) in
-      { uri
-      ; contents
-      ; toc
-      ; version
-      ; nodes
-      ; completed = Stopped init_range
-      ; root
-      ; env
-      ; diags_dirty
-      })
+      error_doc ~loc ~message ~uri ~version ~contents ~env ~completed
+    | Completed (Ok doc) -> (doc, [])
+  in
+  let state = doc.root in
+  let stats = Stats.dump () in
+  let nodes =
+    let lines = contents.Contents.lines in
+    process_init_feedback ~lines ~stats state (feedback @ extra_feedback)
+    @ doc.nodes
+  in
+  let diags_dirty = not (CList.is_empty nodes) in
+  { doc with nodes; diags_dirty }
 
-let create ~env ~uri ~version ~raw =
+let handle_contents_creation ~env ~uri ~version ~raw ~completed f =
   match Contents.make ~uri ~raw with
-  | Error e -> Coq.Protect.R.error (Pp.str e)
-  | Ok contents -> create ~env ~uri ~version ~contents
+  | Contents.R.Error err ->
+    let root = env.Env.init in
+    conv_error_doc ~raw ~uri ~version ~env ~root ~completed err
+  | Contents.R.Ok contents -> f ~env ~uri ~version ~contents
+
+let create ~env ~uri ~version ~raw =
+  let completed range = Completion.Failed range in
+  handle_contents_creation ~env ~uri ~version ~raw ~completed
+    handle_doc_creation_exec
+
+(* Used in bump, we should consolidate with create *)
+let recreate ~doc ~version ~contents =
+  let env, uri = (doc.env, doc.uri) in
+  handle_doc_creation_exec ~env ~uri ~version ~contents
 
 let create_failed_permanent ~env ~uri ~version ~raw =
-  Contents.make ~uri ~raw
-  |> Contents.R.map ~f:(fun contents ->
-         let lines = contents.Contents.lines in
-         let init_loc = init_loc ~uri in
-         let range = Coq.Utils.to_range ~lines init_loc in
-         { uri
-         ; contents
-         ; toc = CString.Map.empty
-         ; version
-         ; root = env.Env.init
-         ; nodes = []
-         ; diags_dirty = true
-         ; completed = FailedPermanent range
-         ; env
-         })
+  let completed range = Completion.FailedPermanent range in
+  handle_contents_creation ~env ~uri ~version ~raw ~completed
+    handle_failed_permanent
 
 let recover_up_to_offset ~init_range doc offset =
   Io.Log.trace "prefix"
@@ -381,20 +442,17 @@ let bump_version ~version ~(contents : Contents.t) doc =
      restoring / executing the first sentence *)
   | FailedPermanent _ -> doc
   | Failed _ ->
-    { doc with
-      version
-    ; nodes = []
-    ; contents
-    ; diags_dirty = true
-    ; completed = Stopped init_range
-    }
+    (* re-create the document on failed, as the env may have changed *)
+    recreate ~doc ~version ~contents
   | Stopped _ | Yes _ -> bump_version ~init_range ~version ~contents doc
 
 let bump_version ~version ~raw doc =
-  let contents = Contents.make ~uri:doc.uri ~raw in
-  Contents.R.map
-    ~f:(fun contents -> bump_version ~version ~contents doc)
-    contents
+  let uri = doc.uri in
+  match Contents.make ~uri ~raw with
+  | Contents.R.Error e ->
+    let completed range = Completion.Failed range in
+    conv_error_doc ~raw ~uri ~version ~env:doc.env ~root:doc.root ~completed e
+  | Contents.R.Ok contents -> bump_version ~version ~contents doc
 
 let add_node ~node doc =
   let diags_dirty = if node.Node.diags <> [] then true else doc.diags_dirty in
@@ -885,6 +943,6 @@ let save ~doc =
     let in_file = Lang.LUri.File.to_string_file uri in
     Coq.State.in_state ~st ~f:(fun () -> Coq.Save.save_vo ~st ~ldir ~in_file) ()
   | _ ->
-    let error = Pp.(str "Can't save incomplete document") in
+    let error = Pp.(str "Can't save document that failed to check") in
     let r = Coq.Protect.R.error error in
     Coq.Protect.E.{ r; feedback = [] }

fleche/doc.mli

@@ -95,17 +95,15 @@ val asts : t -> Node.Ast.t list
 (** Return the list of all diags in the doc *)
 val diags : t -> Lang.Diagnostic.t list
 
-(** Create a new Coq document, this is cached! *)
-val create :
-     env:Env.t
-  -> uri:Lang.LUri.File.t
-  -> version:int
-  -> raw:string
-  -> (t, Loc.t) Coq.Protect.R.t
+(** Create a new Coq document, this is cached! Note that this operation always
+    suceeds, but the document could be created in a `Failed` state if problems
+    arise. *)
+val create : env:Env.t -> uri:Lang.LUri.File.t -> version:int -> raw:string -> t
 
 (** Update the contents of a document, updating the right structures for
-    incremental checking. *)
-val bump_version : version:int -> raw:string -> t -> t Contents.R.t
+    incremental checking. If the operation fails, the document will be left in
+    `Failed` state. *)
+val bump_version : version:int -> raw:string -> t -> t
 
 (** Checking targets, this specifies what we expect check to reach *)
 module Target : sig
@@ -129,8 +127,4 @@ val save : doc:t -> (unit, Loc.t) Coq.Protect.E.t
 
 (** This is internal, to workaround the Coq multiple-docs problem *)
 val create_failed_permanent :
-     env:Env.t
-  -> uri:Lang.LUri.File.t
-  -> version:int
-  -> raw:string
-  -> t Contents.R.t
+  env:Env.t -> uri:Lang.LUri.File.t -> version:int -> raw:string -> t

fleche/theory.ml

@@ -224,34 +224,10 @@ end = struct
     pending := CList.remove Lang.LUri.File.equal uri !pending
 end
 
-let send_error_permanent_fail ~io ~uri ~version message =
-  let open Lang in
-  let start = Point.{ line = 0; character = 0; offset = 0 } in
-  let end_ = Point.{ line = 0; character = 1; offset = 1 } in
-  let range = Range.{ start; end_ } in
-  let d = Lang.Diagnostic.{ range; severity = 1; message; extra = None } in
-  Io.Report.diagnostics ~io ~uri ~version [ d ]
-
-let handle_create ~io ~uri ~version r =
-  match r with
-  | Coq.Protect.R.Completed (Result.Ok doc) ->
-    Handle.create ~uri ~doc;
-    Check.schedule ~uri
-  | Completed (Result.Error (Anomaly (_, msg)))
-  | Completed (Result.Error (User (_, msg))) ->
-    (* For now we inform the user of the problem, we could be finer and create a
-       ghost node for the implicit import, but we will phase that out in Coq
-       upstream at some point. *)
-    let message =
-      Format.asprintf "Doc.create, internal error: @[%a@]" Pp.pp_with msg
-    in
-    Io.Report.message ~io ~lvl:1 ~message;
-    send_error_permanent_fail ~io ~uri ~version (Pp.str message)
-  | Interrupted -> ()
-
-let create ~io ~env ~uri ~raw ~version =
-  let r = Doc.create ~env ~uri ~raw ~version in
-  handle_create ~io ~uri ~version r
+let create ~env ~uri ~raw ~version =
+  let doc = Doc.create ~env ~uri ~raw ~version in
+  Handle.create ~uri ~doc;
+  Check.schedule ~uri
 
 (* Set this to false for < 8.17, we could parse the version but not worth it. *)
 let sane_coq_base_version = true
@@ -279,32 +255,28 @@ let create ~io ~env ~uri ~raw ~version =
        instructions on how to install a fixed branch for earlier Coq versions."
     in
     Io.Report.message ~io ~lvl:1 ~message;
-    (match Doc.create_failed_permanent ~env ~uri ~raw ~version with
-    | Contents.R.Error _e -> ()
-    | Ok doc -> Handle.create ~uri ~doc);
-    send_error_permanent_fail ~io ~uri ~version (Pp.str message))
+    let doc = Doc.create_failed_permanent ~env ~uri ~raw ~version in
+    Handle.create ~uri ~doc;
+    Check.schedule ~uri)
   else (
     tainted := true;
-    create ~io ~env ~uri ~raw ~version)
+    create ~env ~uri ~raw ~version)
 
-let change ~io ~(doc : Doc.t) ~version ~raw =
+let change ~io:_ ~(doc : Doc.t) ~version ~raw =
   let uri = doc.uri in
   Io.Log.trace "bump file"
     (Lang.LUri.File.to_string_uri uri ^ " / version: " ^ string_of_int version);
   let tb = Unix.gettimeofday () in
   (* The discrepancy here will be solved once we remove the [Protect.*.t] types
      from `doc.mli` *)
-  match Doc.bump_version ~version ~raw doc with
-  | Contents.R.Error e ->
-    (* Send diagnostics for content conversion *)
-    let message = Pp.(str "Error in document conversion: " ++ str e) in
-    send_error_permanent_fail ~io ~uri ~version message;
-    Handle.clear_requests ~uri
-  | Contents.R.Ok doc ->
-    let diff = Unix.gettimeofday () -. tb in
-    Io.Log.trace "bump file took" (Format.asprintf "%f" diff);
-    Check.schedule ~uri;
-    Handle.update_doc_version ~doc
+  let doc = Doc.bump_version ~version ~raw doc in
+  let diff = Unix.gettimeofday () -. tb in
+  Io.Log.trace "bump file took" (Format.asprintf "%f" diff);
+  (* Just in case for the future, we update the document before requesting it to
+     be checked *)
+  let invalid = Handle.update_doc_version ~doc in
+  Check.schedule ~uri;
+  invalid
 
 let change ~io ~uri ~version ~raw =
   match Handle.find_opt ~uri with

test/server/todo.md

@@ -0,0 +1,12 @@
+- Tests on document lifetime:
+
+  Checks to do:
+
+  a) check that the errors / messages are properly relayed to the user
+  b) check that coq-lsp recovers properly
+
+  + create a .v document, fails when importing the prelude for some weird reason
+  + bump a .v document, fails to bump due to having to re-create initial state
+
+  + For .mv / .wpn documents: same as before, we can also fail due to
+    bad markdown parsing