diff --git a/dune-project b/dune-project index 251fbd92aabb..aaa2ec052adc 100644 --- a/dune-project +++ b/dune-project @@ -81,6 +81,21 @@ implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/de which allows clients, such as CoqIDE, to interact with Coq in a structured way.")) +(package + (name coqlsp-server) + (depends + (coq-core (= :version))) + (synopsis "The Coq Proof Assistant, Language Server Protocol server") + (description "Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. + +This package provides the `coqlsptop` language server, an +implementation of [Language Server Protocol](https://microsoft.github.io/language-server-protocol/) +which allows clients, such as VSCoq, to interact with Coq in a +structured way.")) + (package (name coqide) (depends diff --git a/ide/lsp/dune b/ide/lsp/dune new file mode 100644 index 000000000000..cb3b831bb813 --- /dev/null +++ b/ide/lsp/dune @@ -0,0 +1,14 @@ +; LSP Server + +(executable + (name lsptop) + (public_name coqlsptop.opt) + (package coqlsp-server) + (modes native byte) + (libraries coq-core.boot coq-core.lib coq-core.toplevel yojson)) + +(install + (section bin) + (package coqlsp-server) + (files + (lsptop.bc as coqlsptop.byte))) diff --git a/ide/lsp/json_helper.ml b/ide/lsp/json_helper.ml new file mode 100644 index 000000000000..b74704ee5e9f --- /dev/null +++ b/ide/lsp/json_helper.ml @@ -0,0 +1,105 @@ +open Yojson.Basic +open Yojson.Basic.Util + +let pmember (k: string) (r: t): t = + member "params" r |> member k + +let sub_from (str: string) (pos: int) : string = + String.sub str pos (String.length str - pos) + +(** UNIX paths: "file:///foo/bar" corresponds to /foo/bar + Windows paths: "file:///z%3A/foo" corresponds to z:/foo **) +let uri_to_path u = if String.sub u 9 3 = "%3A" then + Printf.sprintf "%s:%s" (String.sub u 8 1) (sub_from u 12) + else sub_from u 7 +let path_to_uri u = if u.[1] = ':' then + let s = sub_from u 2 in + let rest = String.map (fun character -> if character == '\\' then '/' else character) s in + "file:///" ^ (String.sub u 0 1) ^ "%3A" ^ rest + else + "file://" ^ u + +type completion_context = { trigger_kind: int; trigger_char: string option } +let to_compl_context (j: t) : completion_context = + { trigger_kind = member "triggerKind" j |> to_int; + trigger_char = + match member "triggerChar" j |> to_string with + | character -> Some character + | exception _ -> None; } + +type txdoc_item = { fname: string; langId: string; version: int; text: string } +let to_txdoc_item (j: t) : txdoc_item = + { fname = member "uri" j |> to_string |> uri_to_path; + langId = member "languageId" j |> to_string; + version = member "version" j |> to_int; + text = member "text" j |> to_string } + +type txdoc_pos = { path: string; line: int; col: int } + +(* Argument is of the form { "textDocument" : {"uri" : ... } } *) +let to_txdoc_id (r: t) : string = + member "textDocument" r |> member "uri" |> to_string |> uri_to_path + +(* Argument is of the form { "textDocument" : ..., + "position" : { "line" : ..., "character" : ... } } *) +let to_txdoc_pos (r: t) : txdoc_pos = + let pos = pmember "position" r in + { path = to_txdoc_id r; + line = pos |> member "line" |> to_int; + col = pos |> member "character" |> to_int } + +type workspace_folder = { wk_uri: string; wk_name: string } +type wsch_event = { added: workspace_folder; removed: workspace_folder } +let to_wsch_event (j: t) : wsch_event = + { added = { wk_uri = member "added" j |> member "uri" |> to_string; + wk_name = member "added" j |> member "name" |> to_string }; + removed = { wk_uri = member "removed" j |> member "uri" |> to_string; + wk_name = member "removed" j |> member "name" |> to_string } } + +let to_contentch (j: t) : string = + member "text" j |> to_string + +type position = { line: int; character: int } +type range = { rng_start: position; rng_end: position } + +let server_capabilities : t = + `Assoc [("capabilities", + `Assoc [("textDocumentSync", `Assoc [ + ("openClose", `Bool true); + ("change", `Int 1); + ("willSave", `Bool false); + ("willSaveWaitUntil", `Bool false); + ("save", `Assoc [("includeText", `Bool true)])]); + ("hoverProvider", `Bool true); + ("completionProvider", `Assoc []); + ("signatureHelpProvider", `Assoc []); + ("definitionProvider", `Bool true); + ("typeDefinitionProvider", `Bool false); + ("implementationProvider", `Bool false); + ("referencesProvider", `Bool false); + ("documentSymbolProvider", `Bool false); + ("workspaceSymbolProvider", `Bool false); + ("codeActionProvider", `Bool false)])] + +let from_position (p: position) : t = `Assoc [("line", `Int p.line); + ("character", `Int p.character)] + +let from_range (r: range) : t = + `Assoc [("start", from_position r.rng_start); ("end", from_position r.rng_end)] + +let dummyrange : t = + from_range { rng_start = { line = 0; character = 0; }; + rng_end = { line = 0; character = 0; }; } + +let diag (fname: string) (msg: string) (r: range option) : t = + let r' = match r with + | Some r -> from_range r + | None -> dummyrange in + `Assoc [("method", `String "textDocument/publishDiagnostics"); + ("params", `Assoc [("uri", `String (path_to_uri fname)); + ("diagnostics", + `List [`Assoc [("range", r'); ("message", `String msg)]])])] + +let diag_clear (fname: string) : t = + `Assoc [("method", `String "textDocument/publishDiagnostics"); + ("params", `Assoc [("uri", `String (path_to_uri fname)); ("diagnostics", `List [])])] diff --git a/ide/lsp/json_helper.mli b/ide/lsp/json_helper.mli new file mode 100644 index 000000000000..fb578ef839a5 --- /dev/null +++ b/ide/lsp/json_helper.mli @@ -0,0 +1,32 @@ +open Yojson.Basic + +val sub_from : string -> int -> string +val pmember : string -> t -> t +val uri_to_path : string -> string + +type completion_context = { trigger_kind: int; trigger_char: string option } +val to_compl_context : t -> completion_context + +type txdoc_item = { fname: string; langId: string; version: int; text: string } +val to_txdoc_item : t -> txdoc_item + +type txdoc_pos = { path: string; line: int; col: int } +val to_txdoc_id : t -> string +val to_txdoc_pos : t -> txdoc_pos + +type workspace_folder = { wk_uri: string; wk_name: string } +type wsch_event = { added: workspace_folder; removed: workspace_folder } +val to_wsch_event : t -> wsch_event +val to_contentch : t -> string + +(* Report on server capabilities *) +val server_capabilities : t + +type position = { line: int; character: int } +type range = { rng_start: position; rng_end: position } + +(* Build a JSON diagnostic *) +val diag : string -> string -> range option -> t + +(* Build an empty JSON diagnostic; used for clearing diagnostic *) +val diag_clear : string -> t diff --git a/ide/lsp/lsp.ml b/ide/lsp/lsp.ml new file mode 100644 index 000000000000..f6ce861f1236 --- /dev/null +++ b/ide/lsp/lsp.ml @@ -0,0 +1,210 @@ +open Yojson.Basic +open Yojson.Basic.Util + +open Json_helper + +type assoct = (string * t) list + +let lsp_of_response (qid: int option) (response: t) : t = + match qid with + | Some i -> `Assoc ([("jsonrpc", `String "2.0"); ("id", `Int i)] @ (response |> to_assoc)) + (* In the case of a notification response, there is no query_id associated *) + | None -> `Assoc ([("jsonrpc", `String "2.0")] @ (response |> to_assoc)) + +type lquery = +| Initialize of int * string +| Initialized +| Shutdown +| Exit +| Cancel of int +| FolderChange of wsch_event +| ChangeConfig +| ChangeWatch +| Symbol of string +| ExecCommand of string +| DidOpen of txdoc_item +| DidChange of string * string +| WillSave of string +| WillSaveWait of string +| DidSave of string * string +| DidClose of string +| Completion of txdoc_pos * completion_context +| Resolve +| Hover of txdoc_pos +| SignatureHelp of txdoc_pos +| Declaration of txdoc_pos +| Definition of txdoc_pos +| TypeDefinition of txdoc_pos +| Implementation of txdoc_pos +| References +| DocumentHighlight of txdoc_pos +| DocumentSymbol +| CodeAction +| CodeLens +| CodeLensResolve +| DocumentLink +| DocumentLinkResolve +| DocumentColor +| ColorPresentation +| Formatting +| RangeFormatting +| TypeFormatting +| Rename +| PrepareRename of txdoc_pos +| FoldingRange +| BadProtocolMsg of string + +type lsp_query = { query_id: int option; q: lquery } + +type error_code = +| MethodNotFound +| InternalError + +let errorcode_to_int : error_code -> int = function +| MethodNotFound -> -32601 +| InternalError -> -32603 + +(** For converting back into json **) +let response_err (err: error_code) (msg: string option) : t = + match msg with + | Some msg -> `Assoc [("code", `Int (errorcode_to_int err)); ("message", `String msg)] + | None -> `Assoc [("code", `Int (errorcode_to_int err))] + +let wrap_jsfail (qid: int option) (str: string) (js: t): lsp_query = + { query_id = qid; q = BadProtocolMsg (str ^ "\n" ^ (pretty_to_string js)) } + +let wrap_parse_err (str: string): lsp_query = + { query_id = None; q = BadProtocolMsg str } + +let unpack_lsp_query (r : t) : lsp_query = + try + let qid = member "id" r |> to_int in + try + { query_id = Some qid; + q = match member "method" r |> to_string with + | "initialize" -> Initialize (pmember "processId" r |> to_int, + pmember "rootUri" r |> to_string) + | "initialized" -> Initialized + | "shutdown" -> Shutdown + | "exit" -> Exit + | "$/cancelRequest" -> Cancel (pmember "id" r |> to_int) + | "workspace/didChangeWorkspaceFolders" -> FolderChange + (pmember "event" r |> to_wsch_event) + | "workspace/didChangeConfiguration" -> ChangeConfig + | "workspace/didChangeWatchedFiles" -> ChangeWatch + | "workspace/symbol" -> Symbol (pmember "r" r |> to_string) + | "workspace/executeCommand" -> ExecCommand + (pmember "command" r |> to_string) + | "textDocument/didOpen" -> DidOpen (pmember "textDocument" r |> to_txdoc_item) + | "textDocument/didChange" -> DidChange (to_txdoc_id r, + pmember "contentChanges" r |> to_contentch) + | "textDocument/willSave" -> WillSave (to_txdoc_id r) + | "textDocument/willSaveWaitUntil" -> WillSaveWait (to_txdoc_id r) + | "textDocument/didSave" -> DidSave (to_txdoc_id r, pmember "text" r |> to_string) + | "textDocument/didClose" -> DidClose (to_txdoc_id r) + | "textDocument/completion" -> Completion (to_txdoc_pos r, + pmember "context" r |> to_compl_context) + | "completionItem/resolve" -> Resolve + | "textDocument/hover" -> Hover (to_txdoc_pos r) + | "textDocument/signatureHelp" -> SignatureHelp (to_txdoc_pos r) + | "textDocument/declaration" -> Declaration (to_txdoc_pos r) + | "textDocument/definition" -> Definition (to_txdoc_pos r) + | "textDocument/typeDefinition" -> TypeDefinition (to_txdoc_pos r) + | "textDocument/implementation" -> Implementation (to_txdoc_pos r) + | "textDocument/references" -> References + | "textDocument/documentHighlight" -> DocumentHighlight (to_txdoc_pos r) + | "textDocument/documentSymbol" -> DocumentSymbol + | "textDocument/codeAction" -> CodeAction + | "textDocument/codeLens" -> CodeLens + | "codeLens/resolve" -> CodeLensResolve + | "textDocument/documentLink" -> DocumentLink + | "documentLink/resolve" -> DocumentLinkResolve + | "textDocument/documentColor" -> DocumentColor + | "textDocument/colorPresentation" -> ColorPresentation + | "textDocument/formatting" -> Formatting + | "textDocument/rangeFormatting" -> RangeFormatting + | "textDocument/onTypeFormatting" -> TypeFormatting + | "textDocument/rename" -> Rename + | "textDocument/prepareRename" -> PrepareRename (to_txdoc_pos r) + | "textDocument/foldingRange" -> FoldingRange + | m -> BadProtocolMsg (Printf.sprintf "Unknown method '%s'" m) } + with + | Type_error (str, js) -> wrap_jsfail (Some qid) str js + | Undefined (str, js) -> wrap_jsfail (Some qid) str js + with + | Type_error (str, js) -> wrap_jsfail None str js + | Undefined (str, js) -> wrap_jsfail None str js + +(* The three kinds of responses *) +let resultResponse (r: t) : t option = Some (`Assoc [("result", r)]) +let errorResponse (r: t) : t option = Some (`Assoc [("error", r)]) +let nullResponse : t option = resultResponse `Null + +type state_or_exit_t = State of Vernac.State.t | ExitCode of int +type response_state_t = t option * state_or_exit_t + +let run_query (state: Vernac.State.t) (q: lquery) : response_state_t = + try + match q with + | Initialize (_, _) -> resultResponse server_capabilities, State state + | Initialized -> None, State state + | Shutdown -> nullResponse, State state + | Exit -> None, ExitCode 0 + | Cancel id -> None, State state + | FolderChange evt -> nullResponse, State state + | ChangeConfig -> nullResponse, State state + | ChangeWatch -> None, State state + | Symbol sym -> nullResponse, State state + | ExecCommand cmd -> nullResponse, State state + | DidOpen { fname = f; langId = _; version = _; text = t } -> nullResponse, State state + | DidChange (txid, content) -> None, State state + | WillSave txid -> None, State state + | WillSaveWait txid -> nullResponse, State state + | DidSave (f, t) -> nullResponse, State state + | DidClose txid -> None, State state + | Completion (txpos, ctx) -> nullResponse, State state + | Resolve -> nullResponse, State state + | Hover txpos -> nullResponse, State state + | SignatureHelp txpos -> nullResponse, State state + | Declaration txpos -> nullResponse, State state + | Definition txpos -> nullResponse, State state + | TypeDefinition txpos -> nullResponse, State state + | Implementation txpos -> nullResponse, State state + | References -> nullResponse, State state + | DocumentHighlight txpos -> nullResponse, State state + | DocumentSymbol -> nullResponse, State state + | CodeAction -> nullResponse, State state + | CodeLens -> nullResponse, State state + | CodeLensResolve -> nullResponse, State state + | DocumentLink -> nullResponse, State state + | DocumentLinkResolve -> nullResponse, State state + | DocumentColor -> nullResponse, State state + | ColorPresentation -> nullResponse, State state + | Formatting -> nullResponse, State state + | RangeFormatting -> nullResponse, State state + | TypeFormatting -> nullResponse, State state + | Rename -> nullResponse, State state + | PrepareRename txpos -> nullResponse, State state + | FoldingRange -> nullResponse, State state + | BadProtocolMsg msg -> errorResponse (response_err MethodNotFound (Some msg)), State state + with + | _ -> errorResponse (response_err InternalError None), State state + +let rec parse_header_len (stream: string Stream.t) (len: int): int = + let line = Stream.next stream in + if String.starts_with ~prefix:"Content-Length: " line then + parse_header_len stream (int_of_string (sub_from line 16)) + else if String.starts_with ~prefix:"Content-Type: " line then + parse_header_len stream len + else + len + +let read_lsp_query (stream: string Stream.t): lsp_query = + match parse_header_len stream 0 with + | n -> let str = Stream.npeek n stream in + if List.length str != n then + wrap_parse_err (Printf.sprintf "Could not read %d bytes" n) + else + unpack_lsp_query (from_string (List.fold_right (fun s1 s2 -> s1 ^ s2) str "")) + | exception Stream.Failure -> wrap_parse_err "Malformed LSP header" + diff --git a/ide/lsp/lsp.mli b/ide/lsp/lsp.mli new file mode 100644 index 000000000000..c03577ef4572 --- /dev/null +++ b/ide/lsp/lsp.mli @@ -0,0 +1,14 @@ +open Yojson.Basic + +type assoct +type lquery +type lsp_query = { query_id: int option; q: lquery } +val lsp_of_response : int option -> t -> t +val unpack_lsp_query : t -> lsp_query + +type state_or_exit_t = State of Vernac.State.t | ExitCode of int +type response_state_t = t option * state_or_exit_t +val run_query : Vernac.State.t -> lquery -> response_state_t + +val parse_header_len : string Stream.t -> int -> int +val read_lsp_query : string Stream.t -> lsp_query diff --git a/ide/lsp/lsptop.ml b/ide/lsp/lsptop.ml new file mode 100644 index 000000000000..0fdfe1021666 --- /dev/null +++ b/ide/lsp/lsptop.ml @@ -0,0 +1,104 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* exit 0 + | Coqtop.(Query PrintTags) -> Coqtop.print_style_tags color_mode; exit 0 + | Coqtop.(Query _) -> Printf.eprintf "Unknown query"; exit 1 + | Coqtop.Interactive -> + let open Vernac.State in + set_doc state.doc; + init_signal_handler (); + let in_ch, out_ch = Spawned.get_channels () in + let json_oc = out_ch in + (* TODO! *) + let json_ic = Stream.from (fun s len -> + CThread.thread_friendly_read in_ch s ~off:0 ~len) in + let process_json json_ic json_oc out_ch = + let open Yojson.Basic in + let open Lsp in + let open Json_helper in + let lsp_query = read_lsp_query json_ic in + match run_query state lsp_query.q with + | (Some r, State _) -> to_channel json_oc (lsp_of_response lsp_query.query_id r) + | (None, _) -> quit := 1 + | (_, ExitCode c) -> quit := c; + flush out_ch + in + + while !quit < 0 do + process_json json_ic json_oc out_ch + done; + exit !quit + +let islave_parse extra_args = + let open Coqtop in + let ({ run_mode; color_mode }, stm_opts), extra_args = coqtop_toplevel.parse_extra extra_args in + let extra_args = parse extra_args in + (* One of the role of coqidetop is to find the name of buffers to open *) + (* in the command line; Coqide is waiting these names on stdout *) + (* (see filter_coq_opts in coq.ml), so we send them now *) + print_string (String.concat "\n" extra_args); + ( { Coqtop.run_mode; color_mode }, stm_opts), [] + +let islave_init ( { Coqtop.run_mode; color_mode }, stm_opts) injections ~opts = + if run_mode = Coqtop.Batch then Flags.quiet := true; + Coqtop.init_toploop opts stm_opts injections + +let islave_default_opts = Coqargs.default + +let islave_usage = Boot.Usage.{ + executable_name = "coqlsptop"; + extra_args = ""; + extra_options = ""; +} + +let islave_parse extra_args = + let open Coqtop in + let ({ run_mode; color_mode }, stm_opts), extra_args = coqtop_toplevel.parse_extra extra_args in + let extra_args = parse extra_args in + (* One of the role of coqidetop is to find the name of buffers to open *) + (* in the command line; Coqide is waiting these names on stdout *) + (* (see filter_coq_opts in coq.ml), so we send them now *) + print_string (String.concat "\n" extra_args); + ( { Coqtop.run_mode; color_mode }, stm_opts), [] + + +let () = + let open Coqtop in + let custom = { + usage = islave_usage; + parse_extra = islave_parse; + init_extra = islave_init; + run = loop; + initial_args = islave_default_opts } in + start_coq custom