From 28d3323d3221e9c725eac3e471e3db473d1d7cdc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 27 Dec 2022 01:18:51 +0100 Subject: [PATCH 1/2] [lsp] Cancel requests that require non-processed document positions. We use the new `code=-32802` RequestFailed, but maybe we should do differently. c.f. #100 --- CHANGES.md | 2 ++ controller/coq_lsp.ml | 80 ++++++++++++++++++++++++------------------- fleche/info.ml | 3 ++ fleche/info.mli | 1 + lsp/base.ml | 7 ++++ lsp/base.mli | 3 ++ 6 files changed, 60 insertions(+), 36 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 5da3d540b..95edeb684 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -23,6 +23,8 @@ goal list (@ejgallego, #115, fixes #109) - Resume checking from common prefix on document update (@ejgallego, #111, fixes #110) + - Cancel / reject requests that can be served due to document not + being processed sufficiently (@ejgallego, fixes #100) # coq-lsp 0.1.0: Memory ----------------------- diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index bb0605522..19c3aaaf2 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -275,10 +275,28 @@ let get_docTextPosition params = (* XXX refactor *) let loc_info loc = Coq.Ast.pr_loc loc -let do_hover ofmt ~id params = - let show_loc_info = true in +let do_position_request ofmt ~id params ~handler = let uri, point = get_docTextPosition params in + let line, col = point in let doc = Hashtbl.find doc_table uri in + let in_range = + match doc.completed with + | Yes _ -> true + | Stopped loc -> + line < loc.line_nb_last + || (line = loc.line_nb_last && col <= loc.ep - loc.bol_pos_last) + in + if in_range then + let result = handler ~doc ~point in + LSP.mk_reply ~id ~result |> LIO.send_json ofmt + else + (* -32802 = RequestFailed | -32803 = ServerCancelled ; *) + let code = -32802 in + let message = "Document is not ready" in + LSP.mk_request_error ~id ~code ~message |> LIO.send_json ofmt + +let hover_handler ~doc ~point = + let show_loc_info = true in let loc_string = Fleche.Info.LC.loc ~doc ~point Exact |> Option.map loc_info |> Option.default "no ast" @@ -289,26 +307,13 @@ let do_hover ofmt ~id params = let hover_string = if show_loc_info then loc_string ^ "\n___\n" ^ info_string else info_string in - let result = - `Assoc - [ ( "contents" - , `Assoc - [ ("kind", `String "markdown"); ("value", `String hover_string) ] ) - ] - in - let msg = LSP.mk_reply ~id ~result in - LIO.send_json ofmt msg + `Assoc + [ ( "contents" + , `Assoc [ ("kind", `String "markdown"); ("value", `String hover_string) ] + ) + ] -let do_completion ofmt ~id params = - let uri, _ = get_docTextPosition params in - let doc = Hashtbl.find doc_table uri in - let f _loc id = `Assoc [ ("label", `String Names.Id.(to_string id)) ] in - let ast = asts_of_doc doc in - let clist = Coq.Ast.grab_definitions f ast in - let result = `List clist in - let msg = LSP.mk_reply ~id ~result in - LIO.send_json ofmt msg -(* LIO.log_error "do_completion" (string_of_int line ^"-"^ string_of_int pos) *) +let do_hover ofmt = do_position_request ofmt ~handler:hover_handler (* Replace by ppx when we can print goals properly in the client *) let mk_hyp { Coq.Goals.names; def = _; ty } : Yojson.Safe.t = @@ -327,23 +332,26 @@ let goals_mode = if !Fleche.Config.v.goal_after_tactic then Fleche.Info.PrevIfEmpty else Fleche.Info.Prev -let do_goals ofmt ~id params = - let uri, point = get_docTextPosition params in - let doc = Hashtbl.find doc_table uri in +let goals_handler ~doc ~point = let goals = Fleche.Info.LC.goals ~doc ~point goals_mode in - let result = - `Assoc - [ ( "textDocument" - , `Assoc [ ("uri", `String uri); ("version", `Int doc.version) ] ) - ; ( "position" - , `Assoc [ ("line", `Int (fst point)); ("character", `Int (snd point)) ] - ) - ; ("goals", `List (mk_goals goals)) - ] - in - let msg = LSP.mk_reply ~id ~result in - LIO.send_json ofmt msg + `Assoc + [ ( "textDocument" + , `Assoc [ ("uri", `String doc.uri); ("version", `Int doc.version) ] ) + ; ( "position" + , `Assoc [ ("line", `Int (fst point)); ("character", `Int (snd point)) ] + ) + ; ("goals", `List (mk_goals goals)) + ] + +let do_goals ofmt = do_position_request ofmt ~handler:goals_handler + +let completion_handler ~doc ~point:_ = + let f _loc id = `Assoc [ ("label", `String Names.Id.(to_string id)) ] in + let ast = asts_of_doc doc in + let clist = Coq.Ast.grab_definitions f ast in + `List clist +let do_completion ofmt = do_position_request ofmt ~handler:completion_handler let memo_cache_file = ".coq-lsp.cache" let memo_save_to_disk () = diff --git a/fleche/info.ml b/fleche/info.ml index 02e174197..a55273b05 100644 --- a/fleche/info.ml +++ b/fleche/info.ml @@ -113,6 +113,7 @@ module type S = sig type ('a, 'r) query = doc:Doc.t -> point:P.t -> 'a -> 'r option + val node : (approx, Doc.node) query val loc : (approx, Loc.t) query val ast : (approx, Coq.Ast.t) query val goals : (approx, Coq.Goals.reified_pp) query @@ -142,6 +143,8 @@ module Make (P : Point) : S with module P := P = struct in find None doc.Doc.nodes + let node = find + let if_not_empty (pp : Pp.t) = if Pp.(repr pp = Ppcmd_empty) then None else Some pp diff --git a/fleche/info.mli b/fleche/info.mli index d51319b47..456c34267 100644 --- a/fleche/info.mli +++ b/fleche/info.mli @@ -44,6 +44,7 @@ module type S = sig type ('a, 'r) query = doc:Doc.t -> point:P.t -> 'a -> 'r option + val node : (approx, Doc.node) query val loc : (approx, Loc.t) query val ast : (approx, Coq.Ast.t) query val goals : (approx, Coq.Goals.reified_pp) query diff --git a/lsp/base.ml b/lsp/base.ml index 7dbab7a25..7188ad7db 100644 --- a/lsp/base.ml +++ b/lsp/base.ml @@ -34,6 +34,13 @@ let _parse_uri str = let mk_reply ~id ~result = `Assoc [ ("jsonrpc", `String "2.0"); ("id", `Int id); ("result", result) ] +let mk_request_error ~id ~code ~message = + `Assoc + [ ("jsonrpc", `String "2.0") + ; ("id", `Int id) + ; ("error", `Assoc [ ("code", `Int code); ("message", `String message) ]) + ] + let mk_notification ~method_ ~params = `Assoc [ ("jsonrpc", `String "2.0") diff --git a/lsp/base.mli b/lsp/base.mli index 9de39941f..3f84fb891 100644 --- a/lsp/base.mli +++ b/lsp/base.mli @@ -24,6 +24,9 @@ val mk_notification : (** Answer to a request *) val mk_reply : id:int -> result:Yojson.Safe.t -> Yojson.Safe.t +(** Fail a request *) +val mk_request_error : id:int -> code:int -> message:string -> Yojson.Safe.t + (* val mk_diagnostic : Range.t * int * string * unit option -> Yojson.Basic.t *) val mk_diagnostics : uri:string From 77945c32645daa4c5a618a5cc7f067c3c1d6f983 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 27 Dec 2022 01:28:22 +0100 Subject: [PATCH 2/2] [lsp] Only serve document symbols when the checking is complete. We could alternatively delay the request / provide a partial result, but that's more complex; let's aim for correctness now and let's do that as future work. --- controller/coq_lsp.ml | 47 ++++++++++++++++++++++--------------------- 1 file changed, 24 insertions(+), 23 deletions(-) diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 19c3aaaf2..a35e32322 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -233,11 +233,16 @@ let do_close _ofmt params = let doc_file = string_field "uri" document in Hashtbl.remove doc_table doc_file -let grab_doc params = +let get_textDocument params = let document = dict_field "textDocument" params in - let doc_file = string_field "uri" document in - let doc = Hashtbl.(find doc_table doc_file) in - (doc_file, doc) + let uri = string_field "uri" document in + let doc = Hashtbl.find doc_table uri in + (uri, doc) + +let get_position params = + let pos = dict_field "position" params in + let line, character = (int_field "line" pos, int_field "character" pos) in + (line, character) let mk_syminfo file (name, _path, kind, pos) : J.t = `Assoc @@ -258,27 +263,23 @@ let _kind_of_type _tm = 13 *) | _ -> 12 (* Function *) *) let do_symbols ofmt ~id params = - let file, doc = grab_doc params in - let f loc id = mk_syminfo file (Names.Id.to_string id, "", 12, loc) in - let ast = asts_of_doc doc in - let slist = Coq.Ast.grab_definitions f ast in - let msg = LSP.mk_reply ~id ~result:(`List slist) in - LIO.send_json ofmt msg - -let get_docTextPosition params = - let document = dict_field "textDocument" params in - let file = string_field "uri" document in - let pos = dict_field "position" params in - let line, character = (int_field "line" pos, int_field "character" pos) in - (file, (line, character)) - -(* XXX refactor *) -let loc_info loc = Coq.Ast.pr_loc loc + let uri, doc = get_textDocument params in + match doc.completed with + | Yes _ -> + let f loc id = mk_syminfo uri (Names.Id.to_string id, "", 12, loc) in + let ast = asts_of_doc doc in + let slist = Coq.Ast.grab_definitions f ast in + let msg = LSP.mk_reply ~id ~result:(`List slist) in + LIO.send_json ofmt msg + | Stopped _ -> + let code = -32802 in + let message = "Document is not ready" in + LSP.mk_request_error ~id ~code ~message |> LIO.send_json ofmt let do_position_request ofmt ~id params ~handler = - let uri, point = get_docTextPosition params in + let _uri, doc = get_textDocument params in + let point = get_position params in let line, col = point in - let doc = Hashtbl.find doc_table uri in let in_range = match doc.completed with | Yes _ -> true @@ -299,7 +300,7 @@ let hover_handler ~doc ~point = let show_loc_info = true in let loc_string = Fleche.Info.LC.loc ~doc ~point Exact - |> Option.map loc_info |> Option.default "no ast" + |> Option.map Coq.Ast.pr_loc |> Option.default "no ast" in let info_string = Fleche.Info.LC.info ~doc ~point Exact |> Option.default "no info"