From 2b024a9fffc4755ddebe7e8a01be4d2de8797f34 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 5 Apr 2024 17:09:59 +0200 Subject: [PATCH] [diagnostics] Add sentence's range to errors extra `data` field. - We change diagnostics `extra` field to `data`, so we now conform to the LSP spec - we include the data only when the `send_diags_extra_data` server-side option is enabled - we now include range of full sentence in error diagnostic extra data Thanks to @driverag22 for the idea, cc #663 --- CHANGES.md | 5 +++++ editor/code/package.json | 5 +++++ etc/doc/PROTOCOL.md | 12 ++++++++++++ fleche/config.ml | 4 ++++ fleche/doc.ml | 42 ++++++++++++++++++++++++++-------------- lang/diagnostic.ml | 5 +++-- lang/diagnostic.mli | 5 +++-- lsp/jLang.ml | 14 ++++++++++++-- 8 files changed, 72 insertions(+), 20 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index c42406bc..8a7d2f27 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -70,6 +70,11 @@ - new VSCode commands to allow to move one sentence backwards / forward, this is particularly useful when combined with lazy checking mode (@ejgallego, #671, fixes #263, fixes #580) + - change diagnostic `extra` field to `data`, so we now conform to the + LSP spec, include the data only when the `send_diags_extra_data` + server-side option is enabled (@ejgallego, #670) + - include range of full sentence in error diagnostic extra data + (@ejgallego, #670 , thanks to @driverag22 for the idea, cc: #663). # coq-lsp 0.1.8.1: Spring fix ----------------------------- diff --git a/editor/code/package.json b/editor/code/package.json index 659f7cf1..2c8b7522 100644 --- a/editor/code/package.json +++ b/editor/code/package.json @@ -165,6 +165,11 @@ "type": "number", "default": 150, "description": "Maximum number of errors per file, after that, coq-lsp will stop checking the file." + }, + "coq-lsp.send_diags_extra_data": { + "type": "boolean", + "default": false, + "description": "Send extra diagnostics data, usually on error" } } }, diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md index a0b1a894..5391da39 100644 --- a/etc/doc/PROTOCOL.md +++ b/etc/doc/PROTOCOL.md @@ -72,6 +72,18 @@ to determine the content type. Supported extensions are: As of today, `coq-lsp` implements two extensions to the LSP spec. Note that none of them are stable yet: +### Extra diagnostics data + +This is enabled if the server-side option `send_diags_extra_data` is +set to `true`. In this case, some diagnostics may come with extra data +in the optional `data` field. + +This field is experimental, and it can change without warning. As of +today we offer two kinds of extra information on errors: + +- range of the full sentence that displayed the error, +- if the error was on a Require, information about the library that failed. + ### Goal Display In order to display proof goals and information at point, `coq-lsp` supports the `proof/goals` request, parameters are: diff --git a/fleche/config.ml b/fleche/config.ml index 2828dc02..e8ee723e 100644 --- a/fleche/config.ml +++ b/fleche/config.ml @@ -49,6 +49,9 @@ type t = (** Verbosity, 1 = reduced, 2 = default. As of today reduced will disable all logging, and the diagnostics and perf_data notification *) ; check_only_on_request : bool [@default false] + (** Experimental setting to check document lazily *) + ; send_diags_extra_data : bool [@default false] + (** Send extra diagnostic data on the `data` diagnostic field. *) } let default = @@ -71,6 +74,7 @@ let default = ; send_perf_data = true ; send_diags = true ; check_only_on_request = false + ; send_diags_extra_data = false } let v = ref default diff --git a/fleche/doc.ml b/fleche/doc.ml index 0a881526..250ac07a 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -132,7 +132,7 @@ module Diags : sig (** Build simple diagnostic *) val make : - ?extra:Lang.Diagnostic.Extra.t list + ?data:Lang.Diagnostic.Data.t list -> Lang.Range.t -> Lang.Diagnostic.Severity.t -> Pp.t @@ -140,7 +140,11 @@ module Diags : sig (** Build advanced diagnostic with AST analysis *) val error : - range:Lang.Range.t -> msg:Pp.t -> ast:Node.Ast.t -> Lang.Diagnostic.t + lines:string array + -> range:Lang.Range.t + -> msg:Pp.t + -> ast:Node.Ast.t + -> Lang.Diagnostic.t (** [of_messages drange msgs] process feedback messages, and convert some to diagnostics based on user-config. Default range [drange] is used for @@ -152,20 +156,30 @@ module Diags : sig end = struct let err = Lang.Diagnostic.Severity.error - let make ?extra range severity message = - Lang.Diagnostic.{ range; severity; message; extra } + let make ?data range severity message = + Lang.Diagnostic.{ range; severity; message; data } (* ast-dependent error diagnostic generation *) - let extra_diagnostics_of_ast ast = + let extra_diagnostics_of_ast ~lines ast = + let stm_range = ast.Node.Ast.v |> Coq.Ast.loc |> Option.get in + let stm_range = Coq.Utils.to_range ~lines stm_range in + let stm_range = Lang.Diagnostic.Data.SentenceRange stm_range in match Coq.Ast.Require.extract ast.Node.Ast.v with | Some { Coq.Ast.Require.from; mods; _ } -> let refs = List.map fst mods in - Some [ Lang.Diagnostic.Extra.FailedRequire { prefix = from; refs } ] - | _ -> None + Some + [ stm_range + ; Lang.Diagnostic.Data.FailedRequire { prefix = from; refs } + ] + | _ -> Some [ stm_range ] + + let extra_diagnostics_of_ast ~lines ast = + if !Config.v.send_diags_extra_data then extra_diagnostics_of_ast ~lines ast + else None - let error ~range ~msg ~ast = - let extra = extra_diagnostics_of_ast ast in - make ?extra range Lang.Diagnostic.Severity.error msg + let error ~lines ~range ~msg ~ast = + let data = extra_diagnostics_of_ast ~lines ast in + make ?data range Lang.Diagnostic.Severity.error msg let of_feed ~drange (range, severity, message) = let range = Option.default drange range in @@ -736,7 +750,7 @@ let strategy_of_coq_err ~node ~state ~last_tok = function | Coq.Protect.Error.Anomaly _ -> Stop (Failed last_tok, node) | User _ -> Continue { state; last_tok; node } -let node_of_coq_result ~token ~doc ~range ~ast ~st ~parsing_diags +let node_of_coq_result ~lines ~token ~doc ~range ~ast ~st ~parsing_diags ~parsing_feedback ~feedback ~info last_tok res = match res with | Ok state -> @@ -748,7 +762,7 @@ let node_of_coq_result ~token ~doc ~range ~ast ~st ~parsing_diags | Error (Coq.Protect.Error.Anomaly (err_range, msg) as coq_err) | Error (User (err_range, msg) as coq_err) -> let err_range = Option.default range err_range in - let err_diags = [ Diags.error ~range:err_range ~msg ~ast ] in + let err_diags = [ Diags.error ~lines ~range:err_range ~msg ~ast ] in let contents, nodes = (doc.contents, doc.nodes) in let context = Recovery_context.make ~contents ~last_tok ~nodes ~ast:ast.v () @@ -805,8 +819,8 @@ let document_action ~token ~st ~parsing_diags ~parsing_feedback ~parsing_time this point then, hence the new last valid token last_tok_new *) let last_tok_new = Coq.Parsing.Parsable.loc doc_handle in let last_tok_new = Coq.Utils.to_range ~lines last_tok_new in - node_of_coq_result ~token ~doc ~range:ast_range ~ast ~st ~parsing_diags - ~parsing_feedback ~feedback ~info last_tok_new res) + node_of_coq_result ~lines ~token ~doc ~range:ast_range ~ast ~st + ~parsing_diags ~parsing_feedback ~feedback ~info last_tok_new res) module Target = struct type t = diff --git a/lang/diagnostic.ml b/lang/diagnostic.ml index cd4521ec..582cbd7e 100644 --- a/lang/diagnostic.ml +++ b/lang/diagnostic.ml @@ -4,8 +4,9 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -module Extra = struct +module Data = struct type t = + | SentenceRange of Range.t | FailedRequire of { prefix : Libnames.qualid option ; refs : Libnames.qualid list @@ -26,7 +27,7 @@ type t = { range : Range.t ; severity : Severity.t ; message : Pp.t - ; extra : Extra.t list option + ; data : Data.t list option [@default None] } let is_error { severity; _ } = severity = 1 diff --git a/lang/diagnostic.mli b/lang/diagnostic.mli index f18425e9..273b766b 100644 --- a/lang/diagnostic.mli +++ b/lang/diagnostic.mli @@ -4,8 +4,9 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -module Extra : sig +module Data : sig type t = + | SentenceRange of Range.t | FailedRequire of { prefix : Libnames.qualid option ; refs : Libnames.qualid list @@ -28,7 +29,7 @@ type t = { range : Range.t ; severity : Severity.t ; message : Pp.t - ; extra : Extra.t list option + ; data : Data.t list option [@default None] } val is_error : t -> bool diff --git a/lsp/jLang.ml b/lsp/jLang.ml index b1245292..166db692 100644 --- a/lsp/jLang.ml +++ b/lsp/jLang.ml @@ -37,6 +37,15 @@ end module Diagnostic = struct module Libnames = Serlib.Ser_libnames + module Data = struct + module Lang = struct + module Range = Range + module Diagnostic = Lang.Diagnostic + end + + type t = [%import: Lang.Diagnostic.Data.t] [@@deriving yojson] + end + (* LSP Ranges, a bit different from Fleche's ranges as points don't include offsets *) module Point = struct @@ -69,14 +78,15 @@ module Diagnostic = struct { range : Range.t ; severity : int ; message : string + ; data : Data.t list option [@default None] } [@@deriving yojson] - let to_yojson { Lang.Diagnostic.range; severity; message; extra = _ } = + let to_yojson { Lang.Diagnostic.range; severity; message; data } = let range = Range.conv range in let severity = Lang.Diagnostic.Severity.to_int severity in let message = Pp.to_string message in - _t_to_yojson { range; severity; message } + _t_to_yojson { range; severity; message; data } end let mk_diagnostics ~uri ~version ld : Yojson.Safe.t =