From 19ff5cc3ae983d2a398acd19c5af186f56e53e42 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Wed, 4 Dec 2024 15:07:25 +0100 Subject: [PATCH 1/2] feat: adding the possiblity of error codes to reponses Lsp specifies a number of useful error codes, like ServerCancelled which allows to tell the client the server is busy. This implements the possiblity of passing a different error code. --- language-server/dm/documentManager.ml | 29 ++++++++++----- language-server/dm/documentManager.mli | 10 +++--- language-server/dm/types.ml | 5 +++ language-server/vscoqtop/lspManager.ml | 49 +++++++++++++++----------- 4 files changed, 60 insertions(+), 33 deletions(-) diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index c8d1e4c1..4ef80026 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -32,6 +32,12 @@ let to_sentence_id = function | Top -> None | Id id -> Some id +type document_state = +| Parsing +| Parsed +(* | Executing of sentence_id TODO: ADD EXEDCUTING STATE +| Executed of sentence_id *) + type state = { uri : DocumentUri.t; init_vs : Vernacstate.t; @@ -40,6 +46,7 @@ type state = { execution_state : ExecutionManager.state; observe_id : observe_id; cancel_handle : Sel.Event.cancellation_handle option; + document_state: document_state; } type event = @@ -125,6 +132,8 @@ let observe_id_range st = let range = Range.{ start; end_ } in Some range +let is_parsing st = st.document_state = Parsing + let make_diagnostic doc range oloc message severity code = let range = match oloc with @@ -445,7 +454,7 @@ let validate_document state (Document.{unchanged_id; invalid_ids; previous_docum ExecutionManager.invalidate previous_document (Document.schedule previous_document) id st ) state.execution_state (Stateid.Set.elements invalid_ids) in let execution_state = ExecutionManager.reset_overview execution_state previous_document in - { state with execution_state; observe_id } + { state with execution_state; observe_id; document_state = Parsed } [%%if coq = "8.18" || coq = "8.19"] let start_library top opts = Coqinit.start_library ~top opts @@ -470,7 +479,7 @@ let init init_vs ~opts uri ~text = let init_vs = Vernacstate.freeze_full_state () in let document = Document.create_document init_vs.Vernacstate.synterp text in let execution_state, feedback = ExecutionManager.init init_vs in - let state = { uri; opts; init_vs; document; execution_state; observe_id=Top; cancel_handle = None } in + let state = { uri; opts; init_vs; document; execution_state; observe_id=Top; cancel_handle = None; document_state = Parsing } in let priority = Some PriorityManager.launch_parsing in let event = Sel.now ?priority ParseEvent in state, [event] @ [inject_em_event feedback] @@ -482,7 +491,7 @@ let reset { uri; opts; init_vs; document; execution_state; } = ExecutionManager.destroy execution_state; let execution_state, feedback = ExecutionManager.init init_vs in let observe_id = Top in - let state = { uri; opts; init_vs; document; execution_state; observe_id; cancel_handle = None } in + let state = { uri; opts; init_vs; document; execution_state; observe_id; cancel_handle = None ; document_state = Parsing } in let priority = Some PriorityManager.launch_parsing in let event = Sel.now ?priority ParseEvent in state, [event] @ [inject_em_event feedback] @@ -672,7 +681,7 @@ let parse_entry st pos entry pattern = let about st pos ~pattern = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in match get_context st pos with - | None -> Error ("No context found") (*TODO execute *) + | None -> Error ({message="No context found"; code=None}) (*TODO execute *) | Some (sigma, env) -> try let ref_or_by_not = parse_entry st loc (smart_global) pattern in @@ -680,7 +689,8 @@ let about st pos ~pattern = Ok (pp_of_coqpp @@ Prettyp.print_about env sigma ref_or_by_not udecl) with e -> let e, info = Exninfo.capture e in - Error (Pp.string_of_ppcmds @@ CErrors.iprint (e, info)) + let message = Pp.string_of_ppcmds @@ CErrors.iprint (e, info) in + Error ({message; code=None}) let search st ~id pos pattern = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in @@ -742,7 +752,7 @@ let hover st pos = let check st pos ~pattern = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in match get_context st pos with - | None -> Error ("No context found") (*TODO execute *) + | None -> Error ({message="No context found"; code=None}) (*TODO execute *) | Some (sigma,env) -> let rc = parse_entry st loc lconstr pattern in try @@ -750,7 +760,8 @@ let check st pos ~pattern = Ok (pp_of_coqpp @@ Vernacentries.check_may_eval env sigma redexpr rc) with e -> let e, info = Exninfo.capture e in - Error (Pp.string_of_ppcmds @@ CErrors.iprint (e, info)) + let message = Pp.string_of_ppcmds @@ CErrors.iprint (e, info) in + Error ({message; code=None}) [%%if coq = "8.18" || coq = "8.19"] let print_located_qualid _ qid = Prettyp.print_located_qualid qid @@ -761,7 +772,7 @@ let print_located_qualid = Prettyp.print_located_qualid let locate st pos ~pattern = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in match get_context st pos with - | None -> Error ("No context found") (*TODO execute *) + | None -> Error ({message="No context found"; code=None}) (*TODO execute *) | Some (sigma, env) -> match parse_entry st loc (smart_global) pattern with | { v = AN qid } -> Ok (pp_of_coqpp @@ print_located_qualid env qid) @@ -780,7 +791,7 @@ let locate st pos ~pattern = let print st pos ~pattern = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in match get_context st pos with - | None -> Error("No context found") + | None -> Error({message="No context found"; code=None}) | Some (sigma, env) -> let qid = parse_entry st loc (smart_global) pattern in let udecl = None in (*TODO*) diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli index 59b31702..c5ae1b77 100644 --- a/language-server/dm/documentManager.mli +++ b/language-server/dm/documentManager.mli @@ -46,6 +46,8 @@ type handled_event = { notification: Notification.Server.t option; } +val is_parsing : state -> bool + val init : Vernacstate.t -> opts:Coqargs.injection_command list -> DocumentUri.t -> text:string -> state * events (** [init st opts uri text] initializes the document manager with initial vernac state [st] on which command line opts will be set. *) @@ -123,18 +125,18 @@ val handle_event : event -> state -> block:bool -> Settings.Mode.t -> Settings.G val search : state -> id:string -> Position.t -> string -> notification Sel.Event.t list -val about : state -> Position.t -> pattern:string -> (pp,string) Result.t +val about : state -> Position.t -> pattern:string -> (pp,error) Result.t val hover : state -> Position.t -> MarkupContent.t option (** Returns an optional Result: if None, the position did not have a word, if Some, an Ok/Error result is returned. *) -val check : state -> Position.t -> pattern:string -> (pp,string) Result.t +val check : state -> Position.t -> pattern:string -> (pp,error) Result.t -val locate : state -> Position.t -> pattern:string -> (pp, string) Result.t +val locate : state -> Position.t -> pattern:string -> (pp, error) Result.t -val print : state -> Position.t -> pattern:string -> (pp, string) Result.t +val print : state -> Position.t -> pattern:string -> (pp, error) Result.t module Internal : sig diff --git a/language-server/dm/types.ml b/language-server/dm/types.ml index bfe79e4c..44799ef7 100644 --- a/language-server/dm/types.ml +++ b/language-server/dm/types.ml @@ -90,4 +90,9 @@ type link = { read_from: Unix.file_descr; } +type error = { + code: Jsonrpc.Response.Error.Code.t option; + message: string; +} + type 'a log = Log : 'a -> 'a log diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index 2fa11731..c2e0de9f 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -20,6 +20,7 @@ open Lsp.Types open Protocol open Protocol.LspWrapper open Protocol.ExtProtocol +open Dm.Types module CompactedDecl = Context.Compacted.Declaration @@ -150,7 +151,7 @@ let do_initialize id params = end; let textDocumentSync = `TextDocumentSyncKind TextDocumentSyncKind.Incremental in let completionProvider = CompletionOptions.create ~resolveProvider:false () in - let documentSymbolProvider = `Bool true in + let documentSymbolProvider = `DocumentSymbolOptions (DocumentSymbolOptions.create ~workDoneProgress:true ()) in let hoverProvider = `Bool true in let capabilities = ServerCapabilities.create ~textDocumentSync @@ -440,7 +441,7 @@ let textDocumentCompletion id params = else let Lsp.Types.CompletionParams.{ textDocument = { uri }; position } = params in match Hashtbl.find_opt states (DocumentUri.to_path uri) with - | None -> log @@ "[textDocumentCompletion]ignoring event on non existent document"; Error("Document does not exist"), [] + | None -> log @@ "[textDocumentCompletion]ignoring event on non existent document"; Error( {message="Document does not exist"; code=None} ), [] | Some { st } -> match Dm.DocumentManager.get_completions st position with | Ok completionItems -> @@ -448,20 +449,27 @@ let textDocumentCompletion id params = return_completion ~isIncomplete:false ~items, [] | Error e -> let message = e in - Error(message), [] + Error {message; code=None}, [] let documentSymbol id params = - let Lsp.Types.DocumentSymbolParams.{ textDocument = {uri}} = params in + let Lsp.Types.DocumentSymbolParams.{ textDocument = {uri}; partialResultToken; workDoneToken } = params in + begin match workDoneToken with + | Some token -> log "WE HAVE A TOKEN" + | None -> log "No TOKEN :'(" + end; match Hashtbl.find_opt states (DocumentUri.to_path uri) with - | None -> log @@ "[documentSymbol] ignoring event on non existent document"; Error("Document does not exist"), [] + | None -> log @@ "[documentSymbol] ignoring event on non existent document"; Error({message="Document does not exist"; code=None}), [] | Some tab -> log @@ "[documentSymbol] getting symbols"; - let symbols = Dm.DocumentManager.get_document_symbols tab.st in - Ok(Some (`DocumentSymbol symbols)), [] + if Dm.DocumentManager.is_parsing tab.st then + Error {code=(Some Jsonrpc.Response.Error.Code.ServerCancelled); message="Parsing not finished"} , [] + else + let symbols = Dm.DocumentManager.get_document_symbols tab.st in + Ok(Some (`DocumentSymbol symbols)), [] let coqtopResetCoq id params = let Request.Client.ResetParams.{ textDocument = { uri } } = params in match Hashtbl.find_opt states (DocumentUri.to_path uri) with - | None -> log @@ "[resetCoq] ignoring event on non existent document"; Error("Document does not exist"), [] + | None -> log @@ "[resetCoq] ignoring event on non existent document"; Error({message="Document does not exist"; code=None}), [] | Some { st; visible } -> let st, events = Dm.DocumentManager.reset st in replace_state (DocumentUri.to_path uri) st visible; @@ -481,32 +489,32 @@ let coqtopInterpretToEnd params = let coqtopLocate id params = let Request.Client.LocateParams.{ textDocument = { uri }; position; pattern } = params in match Hashtbl.find_opt states (DocumentUri.to_path uri) with - | None -> log @@ "[locate] ignoring event on non existent document"; Error("Document does not exist"), [] + | None -> log @@ "[locate] ignoring event on non existent document"; Error({message="Document does not exist"; code=None}), [] | Some { st } -> Dm.DocumentManager.locate st position ~pattern, [] let coqtopPrint id params = let Request.Client.PrintParams.{ textDocument = { uri }; position; pattern } = params in match Hashtbl.find_opt states (DocumentUri.to_path uri) with - | None -> log @@ "[print] ignoring event on non existent document"; Error("Document does not exist"), [] + | None -> log @@ "[print] ignoring event on non existent document"; Error({message="Document does not exist"; code=None}), [] | Some { st } -> Dm.DocumentManager.print st position ~pattern, [] let coqtopAbout id params = let Request.Client.AboutParams.{ textDocument = { uri }; position; pattern } = params in match Hashtbl.find_opt states (DocumentUri.to_path uri) with - | None -> log @@ "[about] ignoring event on non existent document"; Error("Document does not exist"), [] + | None -> log @@ "[about] ignoring event on non existent document"; Error({message="Document does not exist"; code=None}), [] | Some { st } -> Dm.DocumentManager.about st position ~pattern, [] let coqtopCheck id params = let Request.Client.CheckParams.{ textDocument = { uri }; position; pattern } = params in match Hashtbl.find_opt states (DocumentUri.to_path uri) with - | None -> log @@ "[check] ignoring event on non existent document"; Error("Document does not exist"), [] + | None -> log @@ "[check] ignoring event on non existent document"; Error({message="Document does not exist"; code=None}), [] | Some { st } -> Dm.DocumentManager.check st position ~pattern, [] let coqtopSearch id params = let Request.Client.SearchParams.{ textDocument = { uri }; id; position; pattern } = params in match Hashtbl.find_opt states (DocumentUri.to_path uri) with - | None -> log @@ "[search] ignoring event on non existent document"; Error("Document does not exist"), [] + | None -> log @@ "[search] ignoring event on non existent document"; Error({message="Document does not exist"; code=None}), [] | Some { st } -> try let notifications = Dm.DocumentManager.search st ~id position pattern in @@ -514,13 +522,13 @@ let coqtopSearch id params = with e -> let e, info = Exninfo.capture e in let message = Pp.string_of_ppcmds @@ CErrors.iprint (e, info) in - Error(message), [] + Error({message; code=None}), [] let sendDocumentState id params = let Request.Client.DocumentStateParams.{ textDocument } = params in let uri = textDocument.uri in match Hashtbl.find_opt states (DocumentUri.to_path uri) with - | None -> log @@ "[documentState] ignoring event on non existent document"; Error("Document does not exist"), [] + | None -> log @@ "[documentState] ignoring event on non existent document"; Error({message="Document does not exist"; code=None}), [] | Some { st } -> let document = Dm.DocumentManager.Internal.string_of_state st in Ok Request.Client.DocumentStateResult.{ document }, [] @@ -532,7 +540,7 @@ let workspaceDidChangeConfiguration params = | Continuous -> run_documents () | Manual -> reset_observe_ids (); ([] : events) -let dispatch_std_request : type a. Jsonrpc.Id.t -> a Lsp.Client_request.t -> (a,string) result * events = +let dispatch_std_request : type a. Jsonrpc.Id.t -> a Lsp.Client_request.t -> (a, error) result * events = fun id req -> match req with | Initialize params -> @@ -545,9 +553,9 @@ let dispatch_std_request : type a. Jsonrpc.Id.t -> a Lsp.Client_request.t -> (a, textDocumentHover id params, [] | DocumentSymbol params -> documentSymbol id params - | UnknownRequest _ | _ -> Error "Received unknown request", [] + | UnknownRequest _ | _ -> Error ({message="Received unknown request"; code=None}), [] -let dispatch_request : type a. Jsonrpc.Id.t -> a Request.Client.t -> (a,string) result * events = +let dispatch_request : type a. Jsonrpc.Id.t -> a Request.Client.t -> (a,error) result * events = fun id req -> match req with | Std req -> dispatch_std_request id req @@ -599,8 +607,9 @@ let handle_lsp_event = function | Ok(Pack r) -> let resp, events = dispatch_request req.id r in begin match resp with - | Error message -> - output_json @@ Jsonrpc.Response.(yojson_of_t @@ error req.id (Error.make ~code:RequestFailed ~message ())) + | Error {code; message} -> + let code = Option.default Jsonrpc.Response.Error.Code.RequestFailed code in + output_json @@ Jsonrpc.Response.(yojson_of_t @@ error req.id (Error.make ~code ~message ())) | Ok resp -> let resp = Request.Client.yojson_of_result r resp in output_json @@ Jsonrpc.Response.(yojson_of_t @@ ok req.id resp) From 4cf45ed785e9df4d73e80b62b63121164cf2d3b6 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Thu, 5 Dec 2024 13:47:40 +0100 Subject: [PATCH 2/2] feat: log the jsonrpc messages received This will help debug lsp problems. --- language-server/vscoqtop/lspManager.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index c2e0de9f..d7b2c262 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -452,15 +452,14 @@ let textDocumentCompletion id params = Error {message; code=None}, [] let documentSymbol id params = - let Lsp.Types.DocumentSymbolParams.{ textDocument = {uri}; partialResultToken; workDoneToken } = params in - begin match workDoneToken with - | Some token -> log "WE HAVE A TOKEN" - | None -> log "No TOKEN :'(" - end; + let Lsp.Types.DocumentSymbolParams.{ textDocument = {uri}; partialResultToken; workDoneToken } = params in (*TODO: At some point we might get ssupport for partialResult and workDone*) match Hashtbl.find_opt states (DocumentUri.to_path uri) with | None -> log @@ "[documentSymbol] ignoring event on non existent document"; Error({message="Document does not exist"; code=None}), [] | Some tab -> log @@ "[documentSymbol] getting symbols"; if Dm.DocumentManager.is_parsing tab.st then + (* Making use of the error codes: the ServerCancelled error code indicates + that the server is busy and the client should resend the request later. + It doesn't seem to be working for documentSymbol at the moment. *) Error {code=(Some Jsonrpc.Response.Error.Code.ServerCancelled); message="Parsing not finished"} , [] else let symbols = Dm.DocumentManager.get_document_symbols tab.st in @@ -599,6 +598,9 @@ let handle_lsp_event = function | Receive (Some rpc) -> lsp :: (* the event is recurrent *) begin try + let json = Jsonrpc.Packet.yojson_of_t rpc in + let msg = Yojson.Safe.pretty_to_string ~std:true json in + log @@ "recieved: " ^ msg; begin match rpc with | Request req -> log @@ "ui request: " ^ req.method_;