From 3609de8c1f3e46110e7c208dcf8eb75c0207e217 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 10 Nov 2023 20:43:02 +0100 Subject: [PATCH] [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 | 5 ++ fleche/contents.ml | 5 ++ fleche/contents.mli | 5 ++ fleche/doc.ml | 157 +++++++++++++++++++++++++++++++------------- fleche/doc.mli | 20 ++++-- fleche/theory.ml | 58 +++++----------- test/server/todo.md | 12 ++++ 7 files changed, 168 insertions(+), 94 deletions(-) create mode 100644 test/server/todo.md diff --git a/CHANGES.md b/CHANGES.md index 5a4bfded5..eee5b96bc 100644 --- a/CHANGES.md +++ b/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 ------------------------------- diff --git a/fleche/contents.ml b/fleche/contents.ml index ab490192b..83db85107 100644 --- a/fleche/contents.ml +++ b/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 } diff --git a/fleche/contents.mli b/fleche/contents.mli index bc305f592..453ab9862 100644 --- a/fleche/contents.mli +++ b/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 diff --git a/fleche/doc.ml b/fleche/doc.ml index 54bcad2cd..c623e8e53 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -245,64 +245,125 @@ 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 root_state workspace uri = Memo.Init.eval (root_state, workspace, uri) +(* Create empty doc, in state [~completed] *) +let empty_doc ~uri ~contents ~version ~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; root; nodes; diags_dirty; completed } + +let error_doc ~loc ~message ~uri ~contents ~version ~root ~nodes ~completed = + let feedback = [ (loc, 1, Pp.str message) ] in + (empty_doc ~uri ~version ~contents ~root ~nodes ~completed, feedback) + +let conv_error_doc ~raw ~uri ~version ~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 ~root ~nodes ~completed ~contents + let create ~state ~workspace ~uri ~version ~contents = let () = Stats.reset () in - let { Coq.Protect.E.r; feedback } = mk_doc state workspace 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 state workspace 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 ~root ~nodes ~completed) + +(** Create a permanently failed doc, to be removed when we drop 8.16 support *) +let handle_failed_permanent ~io:_ ~state ~workspace:_ ~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 ~root:state ~nodes:[] + ~completed + in + let stats = Stats.dump () in + let nodes = + let lines = contents.Contents.lines in + process_init_feedback ~lines ~stats state 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 ~io ~state ~workspace ~uri ~version ~contents = + let completed range = Completion.Failed range in + let { Coq.Protect.E.r; feedback } = + create ~state ~workspace ~uri ~version ~contents + in + let doc, extra_feedback = + match r with + | Interrupted -> + let message = "Document Creation Interrupted!" in + Io.Report.message ~io ~lvl:1 ~message; + error_doc ~loc:None ~message ~uri ~version ~contents ~root:state ~nodes:[] + ~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 - ; root - ; nodes - ; diags_dirty - ; completed = Stopped init_range - }) - -let create ~state ~workspace ~uri ~version ~raw = + Io.Report.message ~io ~lvl:1 ~message; + error_doc ~loc ~message ~uri ~version ~contents ~root:state ~nodes:[] + ~completed + | Completed (Ok doc) -> (doc, []) + 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 handle_contents_creation ~io ~state ~workspace ~uri ~version ~raw ~completed + f = match Contents.make ~uri ~raw with - | Error e -> Coq.Protect.R.error (Pp.str e) - | Ok contents -> create ~state ~workspace ~uri ~version ~contents - -let create_failed_permanent ~state ~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 = state - ; nodes = [] - ; diags_dirty = true - ; completed = FailedPermanent range - }) + | Contents.R.Error err -> + conv_error_doc ~raw ~uri ~version ~root:state ~completed err + | Contents.R.Ok contents -> f ~io ~state ~workspace ~uri ~version ~contents + +let create ~io ~state ~workspace ~uri ~version ~raw = + let completed range = Completion.Failed range in + handle_contents_creation ~io ~state ~workspace ~uri ~version ~raw ~completed + handle_doc_creation_exec + +let create_failed_permanent ~io ~state ~workspace ~uri ~version ~raw = + let completed range = Completion.FailedPermanent range in + handle_contents_creation ~io ~state ~workspace ~uri ~version ~raw ~completed + handle_failed_permanent let recover_up_to_offset ~init_range doc offset = Io.Log.trace "prefix" @@ -370,10 +431,12 @@ let bump_version ~version ~(contents : Contents.t) doc = | 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 ~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 @@ -864,6 +927,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 = [] } diff --git a/fleche/doc.mli b/fleche/doc.mli index 887114227..7d5dd2731 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -78,18 +78,22 @@ 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! *) +(** 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 : - state:Coq.State.t + io:Io.CallBack.t + -> state:Coq.State.t -> workspace:Coq.Workspace.t -> uri:Lang.LUri.File.t -> version:int -> raw:string - -> (t, Loc.t) Coq.Protect.R.t + -> 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 @@ -113,8 +117,10 @@ 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 : - state:Coq.State.t + io:Io.CallBack.t + -> state:Coq.State.t + -> workspace:Coq.Workspace.t -> uri:Lang.LUri.File.t -> version:int -> raw:string - -> t Contents.R.t + -> t diff --git a/fleche/theory.ml b/fleche/theory.ml index 6a267c30f..3ea8f345a 100644 --- a/fleche/theory.ml +++ b/fleche/theory.ml @@ -224,31 +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 create ~io ~root_state ~workspace ~uri ~raw ~version = - let r = Doc.create ~state:root_state ~workspace ~uri ~raw ~version in - match r with - | 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 doc = Doc.create ~io ~state:root_state ~workspace ~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 @@ -276,32 +255,31 @@ let create ~io ~root_state ~workspace ~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 ~state:root_state ~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 ~io ~state:root_state ~workspace ~uri ~raw + ~version + in + Handle.create ~uri ~doc; + Check.schedule ~uri) else ( tainted := true; create ~io ~root_state ~workspace ~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 diff --git a/test/server/todo.md b/test/server/todo.md new file mode 100644 index 000000000..0caf4524f --- /dev/null +++ b/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