Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adding error codes and better logging #957

Merged
merged 2 commits into from
Dec 5, 2024
Merged

Adding error codes and better logging #957

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
19ff5cc
feat: adding the possiblity of error codes to reponses
rtetley Dec 4, 2024
4cf45ed
feat: log the jsonrpc messages received
rtetley Dec 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 20 additions & 9 deletions language-server/dm/documentManager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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 =
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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]
Expand All @@ -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]
Expand Down Expand Up @@ -672,15 +681,16 @@ 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
let udecl = None (* TODO? *) in
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
Expand Down Expand Up @@ -742,15 +752,16 @@ 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
let redexpr = None in
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
Expand All @@ -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)
Expand All @@ -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*)
Expand Down
10 changes: 6 additions & 4 deletions language-server/dm/documentManager.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)
Expand Down Expand Up @@ -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
Expand Down
5 changes: 5 additions & 0 deletions language-server/dm/types.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
51 changes: 31 additions & 20 deletions language-server/vscoqtop/lspManager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ open Lsp.Types
open Protocol
open Protocol.LspWrapper
open Protocol.ExtProtocol
open Dm.Types

module CompactedDecl = Context.Compacted.Declaration

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -440,28 +441,34 @@ 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 ->
let items = List.mapi make_CompletionItem completionItems in
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 (*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("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
(* 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
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;
Expand All @@ -481,46 +488,46 @@ 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
Ok(()), inject_notifications notifications
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 }, []

Expand All @@ -532,7 +539,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 ->
Expand All @@ -545,9 +552,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
Expand Down Expand Up @@ -591,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_;
Expand All @@ -599,8 +609,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)
Expand Down
Loading