Merge pull request #604 from ejgallego/error_in_doc

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

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
@@ -785,9 +843,9 @@ let process_and_parse ~io ~target ~uri ~version doc last_tok doc_handle =
     else doc
   in
   (* Set the document to "internal" mode, stm expects the node list to be in
-     reveresed order *)
+     reversed order *)
   let doc = { doc with nodes = List.rev doc.nodes } in
-  (* Note that nodes and diags in reversed order here *)
+  (* Note that nodes and diags are in reversed order here *)
   (match doc.nodes with
   | [] -> ()
   | n :: _ ->
@@ -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