Skip to content

Commit

Permalink
Merge pull request #957 from coq/outline-regression
Browse files Browse the repository at this point in the history 
Adding error codes and better logging
  • Loading branch information
@rtetley
rtetley authored Dec 5, 2024
2 parents 3221018 + 4cf45ed commit 034078f
Show file tree
Hide file tree
Showing 4 changed files with 62 additions and 33 deletions.
29 changes: 20 additions & 9 deletions language-server/dm/documentManager.ml
View file
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
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
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
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

0 comments on commit 034078f

Please sign in to comment.