max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: clean up LSP code style and add more definitions from the spec

Browse source
This commit is contained in:
Wojciech Nawrocki 2020-08-08 17:25:34 +02:00 • committed by Leonardo de Moura
parent 098c7af1b6
commit 23feb04d60
19 changed files with 508 additions and 346 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Data/Json.lean
View file

@ -5,6 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner, Marc Huisinga
-/
import Lean.Data.Json.Handle
import Lean.Data.Json.Printer
import Lean.Data.Json.Parser
import Lean.Data.Json.FromToJson
import Lean.Data.Json.Printer
import Lean.Data.Json.Parser
import Lean.Data.Json.FromToJson

2
src/Lean/Data/Json/FromToJson.lean
View file

@ -38,7 +38,7 @@ instance Array.hasFromJson {α : Type u} [HasFromJson α] : HasFromJson (Array
⟨fun j => match j with
| Json.arr a => a.mapM fromJson?
| _ => none⟩
instance List.hasToJson {α : Type u} [HasToJson α] : HasToJson (Array α) :=
instance Array.hasToJson {α : Type u} [HasToJson α] : HasToJson (Array α) :=
⟨fun a => Json.arr (a.map toJson)⟩
namespace Json

79
src/Lean/Data/JsonRpc.lean
View file

@ -3,6 +3,9 @@ import Init.System.IO
import Std.Data.RBTree
import Lean.Data.Json
/-! Implementation of JSON-RPC 2.0 (https://www.jsonrpc.org/specification)
for use in the LSP server. -/
namespace Lean
namespace JsonRpc
@ -29,24 +32,22 @@ inductive ErrorCode
| requestCancelled
| contentModified
instance hasFromJsonErrorCode : HasFromJson ErrorCode :=
instance ErrorCode.hasFromJson : HasFromJson ErrorCode :=
⟨fun j => match j with
| num n =>
if n = (-32700 : Int) then ErrorCode.parseError
else if n = (-32600 : Int) then ErrorCode.invalidRequest
else if n = (-32601 : Int) then ErrorCode.methodNotFound
else if n = (-32602 : Int) then ErrorCode.invalidParams
else if n = (-32603 : Int) then ErrorCode.internalError
else if n = (-32099 : Int) then ErrorCode.serverErrorStart
else if n = (-32000 : Int) then ErrorCode.serverErrorEnd
else if n = (-32002 : Int) then ErrorCode.serverNotInitialized
else if n = (-32001 : Int) then ErrorCode.unknownErrorCode
else if n = (-32800 : Int) then ErrorCode.requestCancelled
else if n = (-32801 : Int) then ErrorCode.contentModified
else none
| _ => none⟩
| num (-32700 : Int) => ErrorCode.parseError
| num (-32600 : Int) => ErrorCode.invalidRequest
| num (-32601 : Int) => ErrorCode.methodNotFound
| num (-32602 : Int) => ErrorCode.invalidParams
| num (-32603 : Int) => ErrorCode.internalError
| num (-32099 : Int) => ErrorCode.serverErrorStart
| num (-32000 : Int) => ErrorCode.serverErrorEnd
| num (-32002 : Int) => ErrorCode.serverNotInitialized
| num (-32001 : Int) => ErrorCode.unknownErrorCode
| num (-32800 : Int) => ErrorCode.requestCancelled
| num (-32801 : Int) => ErrorCode.contentModified
| _ => none⟩
instance hasToJsonErrorCode : HasToJson ErrorCode :=
instance ErrorCode.hasToJson : HasToJson ErrorCode :=
⟨fun e => match e with
| ErrorCode.parseError => (-32700 : Int)
| ErrorCode.invalidRequest => (-32600 : Int)
@ -60,10 +61,10 @@ instance hasToJsonErrorCode : HasToJson ErrorCode :=
| ErrorCode.requestCancelled => (-32800 : Int)
| ErrorCode.contentModified => (-32801 : Int)⟩
-- uses Option Structured because users will likely rarely distinguish between an empty
-- parameter array and an omitted params field.
-- uses seperate constructors for notifications and errors because client and server
-- behavior is expected to be wildly different for both.
/- Uses Option Structured because users will likely rarely distinguish between an empty
parameter array and an omitted params field.
Uses separate constructors for notifications and errors because client and server
behavior is expected to be wildly different for both. -/
inductive Message
| request (id : RequestID) (method : String) (params? : Option Structured)
| notification (method : String) (params? : Option Structured)
@ -80,31 +81,37 @@ structure Error := (id : RequestID) (code : JsonNumber) (message : String) (data
instance stringToRequestID : HasCoe String RequestID := ⟨RequestID.str⟩
instance numToRequestID : HasCoe JsonNumber RequestID := ⟨RequestID.num⟩
instance requestIDToJson : HasToJson RequestID :=
⟨fun rid => match rid with
| RequestID.str s => s
| RequestID.num n => num n
| RequestID.null => null⟩
instance requestIDFromJson : HasFromJson RequestID :=
instance RequestId.hasFromJson : HasFromJson RequestID :=
⟨fun j => match j with
| str s => RequestID.str s
| num n => RequestID.num n
| _ => none⟩
instance messageToJson : HasToJson Message :=
instance RequestID.hasToJson : HasToJson RequestID :=
⟨fun rid => match rid with
| RequestID.str s => s
| RequestID.num n => num n
| RequestID.null => null⟩
instance Message.hasToJson : HasToJson Message :=
⟨fun m =>
mkObj $ ⟨"jsonrpc", "2.0"⟩ :: match m with
| Message.request id method params? =>
[⟨"id", toJson id⟩, ⟨"method", method⟩] ++ opt "params" params?
[ ⟨"id", toJson id⟩
, ⟨"method", method⟩
] ++ opt "params" params?
| Message.notification method params? =>
⟨"method", method⟩ :: opt "params" params?
⟨"method", method⟩ ::
opt "params" params?
| Message.response id result =>
[⟨"id", toJson id⟩, ⟨"result", result⟩]
[ ⟨"id", toJson id⟩
, ⟨"result", result⟩]
| Message.responseError id code message data? =>
[⟨"id", toJson id⟩,
⟨"error", mkObj $
[⟨"code", toJson code⟩, ⟨"message", message⟩] ++ opt "data" data?⟩]⟩
[ ⟨"id", toJson id⟩
, ⟨"error", mkObj $
[ ⟨"code", toJson code⟩
, ⟨"message", message⟩
] ++ opt "data" data?⟩]⟩
def aux1 (j : Json) : Option Message := do
id ← j.getObjValAs? RequestID "id";
@ -132,7 +139,7 @@ pure (Message.responseError id code message data?)
-- HACK: The implementation must be made up of several `auxN`s instead
-- of one large block because of a bug in the compiler.
instance messageFromJson : HasFromJson Message :=
instance Message.hasFromJson : HasFromJson Message :=
⟨fun j => do
"2.0" ← j.getObjVal? "jsonrpc" | none;
aux1 j <|> aux2 j <|> aux3 j <|> aux4 j⟩
@ -150,7 +157,7 @@ def readMessage (h : FS.Handle) (nBytes : Nat) : IO Message := do
j ← h.readJson nBytes;
match fromJson? j with
| some m => pure m
| none => throw (userError ("json '" ++ j.compress ++ "' did not have the format of a jsonrpc message"))
| none => throw (userError ("JSON '" ++ j.compress ++ "' did not have the format of a JSON-RPC message"))
def readRequestAs (h : FS.Handle) (nBytes : Nat) (expectedMethod : String) (α : Type*) [HasFromJson α] : IO (Request α) := do
m ← h.readMessage nBytes;

7
src/Lean/Data/Lsp.lean
View file

@ -5,10 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner, Marc Huisinga
-/
import Lean.Data.Lsp.Basic
import Lean.Data.Lsp.GeneralMessage
import Lean.Data.Lsp.TextSync
import Lean.Data.Lsp.Communication
import Lean.Data.Lsp.Capabilities
import Lean.Data.Lsp.Communication
import Lean.Data.Lsp.Diagnostics
import Lean.Data.Lsp.Hover
import Lean.Data.Lsp.InitShutdown
import Lean.Data.Lsp.TextSync
import Lean.Data.Lsp.Utf16
import Lean.Data.Lsp.Workspace

238
src/Lean/Data/Lsp/Basic.lean
View file

@ -1,38 +1,46 @@
import Lean.Data.Json
/-! Defines most of the 'Basic Structures' in the LSP specification
(https://microsoft.github.io/language-server-protocol/specifications/specification-current/),
as well as some utilities.
Since LSP is Json-based, Ints/Nats are represented by Floats on the wire. -/
namespace Lean
namespace Lsp
open Json
-- all Ints/Nats in this file are Floats in LSP
-- as in http://tools.ietf.org/html/rfc3986
abbrev DocumentUri := String
-- LSP indexes text with rows and colums
/-- An array of the lines in a text document.
Elements mustn't contain newline characters. -/
def DocumentText := Array String
-- character is accepted liberally: actual character := min(line length, character)
/-- Can represent both a UTF-16 position - this is what LSP clients send -
and a codepoint position - what we use internally.
`character` is accepted liberally: actual character := min(line length, character) -/
structure Position := (line : Nat) (character : Nat)
instance positionHasFromJson : HasFromJson Position :=
instance Position.hasFromJson : HasFromJson Position :=
⟨fun j => do
line ← j.getObjValAs? Nat "line";
character ← j.getObjValAs? Nat "character";
pure ⟨line, character⟩⟩
instance positionHasToJson : HasToJson Position :=
instance Position.hasToJson : HasToJson Position :=
⟨fun o => mkObj $
⟨"line", o.line⟩ :: ⟨"character", o.character⟩ :: []⟩
[ ⟨"line", o.line⟩
, ⟨"character", o.character⟩
]⟩
instance positionHasToString : HasToString Position :=
⟨fun p => "(" ++ toString p.line ++ ", " ++ toString p.character ++ ")"⟩
instance Position.hasToString : HasToString Position :=
⟨fun p => "(" ++ toString p.line ++ ", " ++ toString p.character ++ ")"⟩
namespace DocumentText
/-- Computes a linear position in an LF-newlined string corresponding
to `text` from an LSP-style 0-indexed (ln, col) position. -/
/-- Computes a linear position in `("\n".intercalate text.toList)`
from an LSP-style 0-indexed (ln, col) position. -/
def lnColToLinearPos (text : DocumentText) (pos : Position) : String.Pos :=
text.foldrRange 0 pos.line (fun ln acc => acc + ln.length + 1) pos.character
@ -50,87 +58,142 @@ let ⟨_, outPos⟩ : String.Pos × Position :=
end DocumentText
-- [start, end)
structure Range := (start : Position) («end» : Position)
instance rangeHasFromJson : HasFromJson Range :=
instance Range.hasFromJson : HasFromJson Range :=
⟨fun j => do
start ← j.getObjValAs? Position "start";
«end» ← j.getObjValAs? Position "end";
pure ⟨start, «end»⟩⟩
instance rangeHasToJson : HasToJson Range :=
instance Range.hasToJson : HasToJson Range :=
⟨fun o => mkObj $
⟨"start", toJson o.start⟩ :: ⟨"end", toJson o.«end»⟩ :: []⟩
[ ⟨"start", toJson o.start⟩
, ⟨"end", toJson o.«end»⟩
]⟩
structure Location := (uri : DocumentUri) (range : Range)
instance locationHasFromJson : HasFromJson Location :=
instance Location.hasFromJson : HasFromJson Location :=
⟨fun j => do
uri ← j.getObjValAs? DocumentUri "uri";
range ← j.getObjValAs? Range "range";
pure ⟨uri, range⟩⟩
instance locationHasToJson : HasToJson Location :=
instance Location.hasToJson : HasToJson Location :=
⟨fun o => mkObj $
⟨"uri", toJson o.uri⟩ :: ⟨"range", toJson o.range⟩ :: []⟩
[ ⟨"uri", toJson o.uri⟩
, ⟨"range", toJson o.range⟩
]⟩
structure LocationLink :=
-- span in origin that is highlighted (e.g. underlined).
-- default for none: word range at mouse position
(originSelectionRange? : Option Range)
(targetUri : DocumentUri)
-- span in target that is displayed
(targetRange : Range)
-- span in target that is highlighted and focused when link is followed.
-- must be a subrange of targetRange
(targetSelectionRange : Range)
instance LocationLink.hasFromJson : HasFromJson LocationLink :=
⟨fun j => do
let originSelectionRange? := j.getObjValAs? Range "originSelectionRange";
targetUri ← j.getObjValAs? DocumentUri "targetUri";
targetRange ← j.getObjValAs? Range "targetRange";
targetSelectionRange ← j.getObjValAs? Range "targetSelectionRange";
pure ⟨originSelectionRange?, targetUri, targetRange, targetSelectionRange⟩⟩
instance LocationLink.hasToJson : HasToJson LocationLink :=
⟨fun o => mkObj $
opt "originSelectionRange" o.originSelectionRange? ++
[ ⟨"targetUri", toJson o.targetUri⟩
, ⟨"targetRange", toJson o.targetRange⟩
, ⟨"targetSelectionRange", toJson o.targetSelectionRange⟩
]⟩
-- NOTE: Diagnostic defined in Diagnostics.lean
/- NOTE: No specific commands are specified by LSP, hence
possible commands need to be announced as capabilities. -/
structure Command :=
(title : String)
-- no specific commands are specified by LSP, hence
-- possible commands need to be announced as capabilities
(command : String)
(arguments? : Option (Array Json) := none)
instance Command.hasFromJson : HasFromJson Command :=
⟨fun j => do
title ← j.getObjValAs? String "title";
command ← j.getObjValAs? String "command";
let arguments? := j.getObjValAs? (Array Json) "arguments";
pure ⟨title, command, arguments?⟩⟩
instance Command.hasToJson : HasToJson Command :=
⟨fun o => mkObj $
opt "arguments" o.arguments? ++
[ ⟨"title", o.title⟩
, ⟨"command", o.command⟩
]⟩
structure TextEdit :=
-- text insertion: start = end
(range : Range)
-- text deletion: empty string
(newText : String)
-- no intermediate states:
-- - ranges may not overlap
-- - multiple inserts can have the same starting position
-- - the order of the array induces the insert order
-- - a single remove or replace edit after an insert
-- can also have the same starting position as the insert
instance TextEdit.hasFromJson : HasFromJson TextEdit :=
⟨fun j => do
range ← j.getObjValAs? Range "range";
newText ← j.getObjValAs? String "newText";
pure ⟨range, newText⟩⟩
instance TextEdit.hasToJson : HasToJson TextEdit :=
⟨fun o => mkObj $
[ ⟨"range", toJson o.range⟩
, ⟨"newText", o.newText⟩
]⟩
def TextEditBatch := Array TextEdit
instance TextEditBatch.hasFromJson : HasFromJson TextEditBatch :=
⟨@fromJson? (Array TextEdit) _⟩
instance TextEditBatch.hasToJson : HasToJson TextEditBatch :=
⟨@toJson (Array TextEdit) _⟩
structure TextDocumentIdentifier := (uri : DocumentUri)
instance textDocumentIdentifierHasFromJson : HasFromJson TextDocumentIdentifier :=
⟨fun j => do
uri ← j.getObjValAs? DocumentUri "uri";
pure ⟨uri⟩⟩
instance TextDocumentIdentifier.hasFromJson : HasFromJson TextDocumentIdentifier :=
⟨fun j => TextDocumentIdentifier.mk <$> j.getObjValAs? DocumentUri "uri"⟩
instance TextDocumentIdentifier.hasToJson : HasToJson TextDocumentIdentifier :=
⟨fun o => mkObj [⟨"uri", o.uri⟩]⟩
structure VersionedTextDocumentIdentifier :=
(uri : DocumentUri)
-- increases after each change, undo and redo
-- none used when a document is not open and the
-- disk content is the master
(version? : Option Nat := none)
instance versionedTextDocumentIdentifierHasFromJson : HasFromJson VersionedTextDocumentIdentifier :=
instance VersionedTextDocumentIdentifier.hasFromJson : HasFromJson VersionedTextDocumentIdentifier :=
⟨fun j => do
uri ← j.getObjValAs? DocumentUri "uri";
let version? := j.getObjValAs? Nat "version";
pure ⟨uri, version?⟩⟩
instance VersionedTextDocumentIdentifier.hasToJson : HasToJson VersionedTextDocumentIdentifier :=
⟨fun o => mkObj $
opt "version" o.version? ++
[⟨"uri", o.uri⟩]⟩
structure TextDocumentEdit :=
(textDocument : VersionedTextDocumentIdentifier)
(edits : TextEditBatch)
instance TextDocumentEdit.hasFromJson : HasFromJson TextDocumentEdit :=
⟨fun j => do
textDocument ← j.getObjValAs? VersionedTextDocumentIdentifier "textDocument";
edits ← j.getObjValAs? TextEditBatch "edits";
pure ⟨textDocument, edits⟩⟩
instance TextDocumentEdit.hasToJson : HasToJson TextDocumentEdit :=
⟨fun o => mkObj $
[ ⟨"textDocument", toJson o.textDocument⟩
, ⟨"edits", toJson o.edits⟩
]⟩
-- TODO(Marc): missing:
-- File Resource Changes, WorkspaceEdit
-- both of these are pretty global, we can look at their
@ -138,14 +201,11 @@ structure TextDocumentEdit :=
structure TextDocumentItem :=
(uri : DocumentUri)
-- used to identify documents on the server side
-- when handling more than language
(languageId : String)
-- increases after each change, undo and redo
(version : Nat)
(text : String)
instance textDocumentItemHasFromJson : HasFromJson TextDocumentItem :=
instance TextDocumentItem.hasFromJson : HasFromJson TextDocumentItem :=
⟨fun j => do
uri ← j.getObjValAs? DocumentUri "uri";
languageId ← j.getObjValAs? String "languageId";
@ -153,54 +213,104 @@ instance textDocumentItemHasFromJson : HasFromJson TextDocumentItem :=
text ← j.getObjValAs? String "text";
pure ⟨uri, languageId, version, text⟩⟩
-- parameter literal for requests
instance TextDocumentItem.hasToJson : HasToJson TextDocumentItem :=
⟨fun o => mkObj $
[ ⟨"uri", o.uri⟩
, ⟨"languageId", o.languageId⟩
, ⟨"version", o.version⟩
, ⟨"text", o.text⟩
]⟩
structure TextDocumentPositionParams :=
(textDocument : TextDocumentIdentifier)
(position : Position)
instance textDocumentPositionParamsHasFromJson : HasFromJson TextDocumentPositionParams :=
instance TextDocumentPositionParams.hasFromJson : HasFromJson TextDocumentPositionParams :=
⟨fun j => do
textDocument ← j.getObjValAs? TextDocumentIdentifier "textDocument";
position ← j.getObjValAs? Position "position";
pure ⟨textDocument, position⟩⟩
instance TextDocumentPositionParams.hasToJson : HasToJson TextDocumentPositionParams :=
⟨fun o => mkObj $
[ ⟨"textDocument", toJson o.textDocument⟩
, ⟨"position", toJson o.position⟩
]⟩
structure DocumentFilter :=
(language? : Option String := none) -- language id
-- uri scheme like 'file' or 'untitled'
(language? : Option String := none)
(scheme? : Option String := none)
-- glob pattern, like *.{ts,js}
-- syntax:
-- - * for one or more chars
-- - ? for one char in path segment
-- - ** for zero or more chars
-- - {} for group conditions
-- - [] for range of character
-- - [!...] to negate range of characters
(pattern? : Option String := none)
instance documentFilterHasFromJson : HasFromJson DocumentFilter :=
instance DocumentFilter.hasFromJson : HasFromJson DocumentFilter :=
⟨fun j => do
let language? := j.getObjValAs? String "language";
let scheme? := j.getObjValAs? String "scheme";
let pattern? := j.getObjValAs? String "pattern";
pure ⟨language?, scheme?, pattern?⟩⟩
instance DocumentFilter.hasToJson : HasToJson DocumentFilter :=
⟨fun o => mkObj $
opt "language" o.language? ++
opt "scheme" o.scheme? ++
opt "pattern" o.pattern?⟩
def DocumentSelector := Array DocumentFilter
instance documentSelectorHasFromJson : HasFromJson DocumentSelector :=
instance DocumentSelector.hasFromJson : HasFromJson DocumentSelector :=
⟨@fromJson? (Array DocumentFilter) _⟩
instance DocumentSelector.hasToJson : HasToJson DocumentSelector :=
⟨@toJson (Array DocumentFilter) _⟩
structure StaticRegistrationOptions := (id? : Option String := none)
instance StaticRegistrationOptions.hasFromJson : HasFromJson StaticRegistrationOptions :=
⟨fun j => some ⟨j.getObjValAs? String "id"⟩⟩
instance StaticRegistrationOptions.hasToJson : HasToJson StaticRegistrationOptions :=
⟨fun o => mkObj $ opt "id" o.id?⟩
structure TextDocumentRegistrationOptions := (documentSelector? : Option DocumentSelector := none)
instance textDocumentRegistrationOptionsHasFromJson : HasFromJson TextDocumentRegistrationOptions :=
instance TextDocumentRegistrationOptions.hasFromJson : HasFromJson TextDocumentRegistrationOptions :=
⟨fun j => some ⟨j.getObjValAs? DocumentSelector "documentSelector"⟩⟩
instance TextDocumentRegistrationOptions.hasToJson : HasToJson TextDocumentRegistrationOptions :=
⟨fun o => mkObj $ opt "documentSelector" o.documentSelector?⟩
inductive MarkupKind | plaintext | markdown
instance MarkupKind.hasFromJson : HasFromJson MarkupKind :=
⟨fun j => match j with
| str "plaintext" => some MarkupKind.plaintext
| str "markdown" => some MarkupKind.markdown
| _ => none⟩
instance MarkupKind.hasToJson : HasToJson MarkupKind :=
⟨fun k => match k with
| MarkupKind.plaintext => str "plaintext"
| MarkupKind.markdown => str "markdown"⟩
structure MarkupContent := (kind : MarkupKind) (value : String)
instance MarkupContent.hasFromJson : HasFromJson MarkupContent :=
⟨fun j => do
kind ← j.getObjValAs? MarkupKind "kind";
value ← j.getObjValAs? String "value";
pure ⟨kind, value⟩⟩
instance MarkupContent.hasToJson : HasToJson MarkupContent :=
⟨fun o => mkObj $
[ ⟨"kind", toJson o.kind⟩
, ⟨"value", o.value⟩
]⟩
-- TODO(Marc): missing:
-- StaticRegistrationOptions,
-- MarkupContent, WorkDoneProgressBegin, WorkDoneProgressReport,
-- WorkDoneProgressBegin, WorkDoneProgressReport,
-- WorkDoneProgressEnd, WorkDoneProgressParams,
-- WorkDoneProgressOptions, PartialResultParams
-- Markup and Progress can be implemented
-- Progress can be implemented
-- later when the basic functionality stands.
end Lsp

15
src/Lean/Data/Lsp/Capabilities.lean
View file

@ -1,16 +1,19 @@
import Lean.Data.JsonRpc
import Lean.Data.Lsp.TextSync
/-! Minimal LSP servers/clients do not have to implement a lot
of functionality. Most useful additional behaviour is instead
opted into via capabilities. -/
namespace Lean
namespace Lsp
open Json
open JsonRpc
-- TODO: right now we ignore the client's capabilities
inductive ClientCapabilities | mk
instance clientCapabilitiesHasFromJson : HasFromJson ClientCapabilities :=
instance ClientCapabilities.hasFromJson : HasFromJson ClientCapabilities :=
⟨fun j => ClientCapabilities.mk⟩
-- TODO largely unimplemented
@ -18,16 +21,10 @@ structure ServerCapabilities :=
(textDocumentSync? : Option TextDocumentSyncOptions := none)
(hoverProvider : Bool := false)
instance serverCapabilitiesHasToJson : HasToJson ServerCapabilities :=
instance ServerCapabilities.hasToJson : HasToJson ServerCapabilities :=
⟨fun o => mkObj $
opt "textDocumentSync" o.textDocumentSync? ++
[⟨"hoverProvider", o.hoverProvider⟩]⟩
def mkLeanServerCapabilities : ServerCapabilities :=
{ textDocumentSync? := some
{ openClose := true
, change? := TextDocumentSyncKind.incremental }
, hoverProvider := true }
end Lsp
end Lean

10
src/Lean/Data/Lsp/Communication.lean
View file

@ -1,6 +1,8 @@
import Init.System.IO
import Lean.Data.JsonRpc
/-! Reading/writing LSP messages from/to IO handles. -/
namespace Lean
namespace Lsp
@ -29,16 +31,16 @@ private partial def readHeaderFields : FS.Handle → IO (List (String × String)
| some hf => do
tail ← readHeaderFields h;
pure (hf :: tail)
| none => throw (userError $ "invalid header field" ++ l)
| none => throw (userError $ "invalid header field: " ++ l)
-- Returns the Content-Length.
/-- Returns the Content-Length. -/
private def readLspHeader (h : FS.Handle) : IO Nat := do
fields ← readHeaderFields h;
match fields.lookup "Content-Length" with
| some length => match length.toNat? with
| some n => pure n
| none => throw (userError ("Content-Length header value '" ++ length ++ "' is not a Nat"))
| none => throw (userError ("no Content-Length header in header fields " ++ toString fields))
| none => throw (userError ("no Content-Length header in header fields: " ++ toString fields))
def readLspMessage (h : FS.Handle) : IO Message := do
nBytes ← readLspHeader h;
@ -67,7 +69,7 @@ def writeLspNotification {α : Type*} [HasToJson α] (h : FS.Handle) (method : S
match toJson r with
| Json.obj o => writeLspMessage h (Message.notification method o)
| Json.arr a => writeLspMessage h (Message.notification method a)
| _ => throw (userError "internal server error in Lean.Lsp.writeLspNotification: tried to write lsp notification that is neither a json object nor a json array")
| _ => throw (userError "internal server error in Lean.Lsp.writeLspNotification: tried to write LSP notification that is neither a JSON object nor a JSON array")
end Lsp
end Lean

74
src/Lean/Data/Lsp/Diagnostics.lean
View file

@ -1,8 +1,12 @@
import Lean.Message
import Lean.Data.Json
import Lean.Data.Lsp.Basic
import Lean.Data.Lsp.Utf16
import Lean.Message
/-! Definitions and functionality for emitting diagnostic information
such as errors, warnings and #command outputs from the LSP server. -/
namespace Lean
namespace Lsp
@ -11,7 +15,7 @@ open Json
inductive DiagnosticSeverity
| error | warning | information | hint
instance diagnosticSeverityHasFromJson : HasFromJson DiagnosticSeverity :=
instance DiagnosticSeverity.hasFromJson : HasFromJson DiagnosticSeverity :=
⟨fun j => match j.getNat? with
| some 1 => DiagnosticSeverity.error
| some 2 => DiagnosticSeverity.warning
@ -19,7 +23,7 @@ instance diagnosticSeverityHasFromJson : HasFromJson DiagnosticSeverity :=
| some 4 => DiagnosticSeverity.hint
| _ => none⟩
instance diagnosticSeverityHasToJson : HasToJson DiagnosticSeverity :=
instance DiagnosticSeverity.hasToJson : HasToJson DiagnosticSeverity :=
⟨fun o => match o with
| DiagnosticSeverity.error => (1 : Nat)
| DiagnosticSeverity.warning => (2 : Nat)
@ -30,77 +34,58 @@ inductive DiagnosticCode
| int (i : Int)
| string (s : String)
instance diagnosticCodeHasFromJson : HasFromJson DiagnosticCode :=
instance DiagnosticCode.hasFromJson : HasFromJson DiagnosticCode :=
⟨fun j => match j with
| num (i : Int) => DiagnosticCode.int i
| str s => DiagnosticCode.string s
| _ => none⟩
instance diagnosticCodeHasToJson : HasToJson DiagnosticCode :=
instance DiagnosticCode.hasToJson : HasToJson DiagnosticCode :=
⟨fun o => match o with
| DiagnosticCode.int i => i
| DiagnosticCode.string s => s⟩
inductive DiagnosticTag
/- Unused or unnecessary code.
Clients are allowed to render diagnostics with this tag faded out instead of having
an error squiggle. -/
| unnecessary
/- Deprecated or obsolete code.
Clients are allowed to rendered diagnostics with this tag strike through. -/
| deprecated
instance diagnosticTagHasFromJson : HasFromJson DiagnosticTag :=
instance DiagnosticTag.hasFromJson : HasFromJson DiagnosticTag :=
⟨fun j => match j.getNat? with
| some 1 => DiagnosticTag.unnecessary
| some 2 => DiagnosticTag.deprecated
| _ => none⟩
instance diagnosticTagHasToJson : HasToJson DiagnosticTag :=
instance DiagnosticTag.hasToJson : HasToJson DiagnosticTag :=
⟨fun o => match o with
| DiagnosticTag.unnecessary => (1 : Nat)
| DiagnosticTag.deprecated => (2 : Nat)⟩
/- Represents a related message and source code location for a diagnostic. This should be
used to point to code locations that cause or are related to a diagnostics, e.g when duplicating
a symbol in a scope. -/
structure DiagnosticRelatedInformation :=
(location : Location)
(message : String)
instance diagnosticRelatedInformationHasFromJson : HasFromJson DiagnosticRelatedInformation :=
instance DiagnosticRelatedInformation.hasFromJson : HasFromJson DiagnosticRelatedInformation :=
⟨fun j => do
location ← j.getObjValAs? Location "location";
message ← j.getObjValAs? String "message";
pure ⟨location, message⟩⟩
instance diagnosticRelatedInformationHasToJson : HasToJson DiagnosticRelatedInformation :=
instance DiagnosticRelatedInformation.hasToJson : HasToJson DiagnosticRelatedInformation :=
⟨fun o => mkObj $
⟨"location", toJson o.location⟩ :: ⟨"message", o.message⟩ :: []⟩
[ ⟨"location", toJson o.location⟩
, ⟨"message", o.message⟩
]⟩
structure Diagnostic :=
/- The range at which the message applies. -/
(range : Range)
/- The diagnostic's severity. Can be omitted. If omitted it is up to the
client to interpret diagnostics as error, warning, info or hint. -/
(severity? : Option DiagnosticSeverity := none)
/- The diagnostic's code, which might appear in the user interface. -/
(code? : Option DiagnosticCode := none)
/- A human-readable string describing the source of this
diagnostic, e.g. 'typescript' or 'super lint'. -/
(source? : Option String := none)
/- The diagnostic's message. -/
(message : String)
/- Additional metadata about the diagnostic.
@since 3.15.0 -/
(tags? : Option (Array DiagnosticTag) := none)
/- An array of related diagnostic information, e.g. when symbol-names within
a scope collide all definitions can be marked via this property. -/
(relatedInformation? : Option (Array DiagnosticRelatedInformation) := none)
instance diagnosticHasFromJson : HasFromJson Diagnostic :=
instance Diagnostic.hasFromJson : HasFromJson Diagnostic :=
⟨fun j => do
range ← j.getObjValAs? Range "range";
let severity? := j.getObjValAs? DiagnosticSeverity "severity";
@ -111,30 +96,37 @@ instance diagnosticHasFromJson : HasFromJson Diagnostic :=
let relatedInformation? := j.getObjValAs? (Array DiagnosticRelatedInformation) "relatedInformation";
pure ⟨range, severity?, code?, source?, message, tags?, relatedInformation?⟩⟩
instance diagnosticHasToJson : HasToJson Diagnostic :=
instance Diagnostic.hasToJson : HasToJson Diagnostic :=
⟨fun o => mkObj $
⟨"range", toJson o.range⟩ :: opt "severity" o.severity? ++ opt "code" o.code? ++
opt "source" o.source? ++ ⟨"message", o.message⟩ :: opt "tags" o.tags? ++ []⟩
opt "severity" o.severity? ++
opt "code" o.code? ++
opt "source" o.source? ++
opt "tags" o.tags? ++
opt "relatedInformation" o.relatedInformation? ++
[ ⟨"range", toJson o.range⟩
, ⟨"message", o.message⟩
]⟩
structure PublishDiagnosticsParams :=
(uri : DocumentUri)
-- version number of document for which
-- diagnostics are published
(version? : Option Int := none)
(diagnostics: Array Diagnostic)
instance publishDiagnosticsParamsHasFromJson : HasFromJson PublishDiagnosticsParams :=
instance PublishDiagnosticsParams.hasFromJson : HasFromJson PublishDiagnosticsParams :=
⟨fun j => do
uri ← j.getObjValAs? DocumentUri "uri";
let version? := j.getObjValAs? Int "version";
diagnostics ← j.getObjValAs? (Array Diagnostic) "diagnostics";
pure ⟨uri, version?, diagnostics⟩⟩
instance publishDiagnosticsParamsHasToJson : HasToJson PublishDiagnosticsParams :=
instance PublishDiagnosticsParams.hasToJson : HasToJson PublishDiagnosticsParams :=
⟨fun o => mkObj $
⟨"uri", toJson o.uri⟩ :: opt "version" o.version? ++ ⟨"diagnostics", toJson o.diagnostics⟩ :: []⟩
opt "version" o.version? ++
[ ⟨"uri", toJson o.uri⟩
, ⟨"diagnostics", toJson o.diagnostics⟩
]⟩
/-- Transform a Lean Message into an LSP Diagnostic. -/
/-- Transform a Lean Message concerning the given text into an LSP Diagnostic. -/
def msgToDiagnostic (text : DocumentText) (m : Message) : Diagnostic :=
-- Lean Message line numbers are 1-based while LSP Positions are 0-based.
let lowLn := m.pos.line - 1;

82
src/Lean/Data/Lsp/GeneralMessage.lean
View file

@ -1,82 +0,0 @@
import Lean.Data.Lsp.Capabilities
import Lean.Data.Json
namespace Lean
namespace Lsp
open Json
structure ClientInfo :=
(name : String)
(version? : Option String := none)
instance clientInfoHasFromJson : HasFromJson ClientInfo :=
⟨fun j => do
name ← j.getObjValAs? String "name";
let version? := j.getObjValAs? String "version";
pure ⟨name, version?⟩⟩
inductive Trace
| messages
| verbose
instance traceHasFromJson : HasFromJson Trace :=
⟨fun j => match j.getStr? with
| some "messages" => Trace.messages
| some "verbose" => Trace.verbose
| _ => none⟩
structure InitializeParams :=
-- id of parent process, none if no parent process
(processId? : Option Int := none)
(clientInfo? : Option ClientInfo := none)
/- We don't support the deprecated rootPath
(rootPath? : Option String)-/
-- none: no folder is open
(rootUri? : Option String := none)
(initializationOptions? : Option Json := none)
(capabilities : ClientCapabilities)
(trace? : Option Trace := none) -- none: no trace
--(workspaceFolders? : Option Unit) TODO
instance initializeParamsHasFromJson : HasFromJson InitializeParams :=
⟨fun j => do
-- many of these params can be null instead of not present.
-- for ease of implementation, we're liberal:
-- missing params, wrong json types and null all map to none,
-- even if LSP sometimes only allows some subset of these.
-- in cases where LSP makes a meaningful distinction
-- between different kinds of missing values, we'll
-- follow accordingly.
let processId? := j.getObjValAs? Int "processId";
let clientInfo? := j.getObjValAs? ClientInfo "clientInfo";
let rootUri? := j.getObjValAs? String "rootUri";
let initializationOptions? := j.getObjVal? "initializationOptions";
capabilities ← j.getObjValAs? ClientCapabilities "capabilities";
let trace? := j.getObjValAs? Trace "trace";
pure ⟨processId?, clientInfo?, rootUri?, initializationOptions?, capabilities, trace?⟩⟩
inductive Initialized
| mk
instance initializedHasFromJson : HasFromJson Initialized :=
⟨fun j => Initialized.mk⟩
structure ServerInfo :=
(name : String)
(version? : Option String := none)
instance serverInfoHasToJson : HasToJson ServerInfo :=
⟨fun o => mkObj $
⟨"name", o.name⟩ :: opt "version" o.version?⟩
structure InitializeResult :=
(capabilities : ServerCapabilities)
(serverInfo? : Option ServerInfo := none)
instance initializeResultHasToJson : HasToJson InitializeResult :=
⟨fun o => mkObj $
⟨"capabilities", toJson o.capabilities⟩ :: opt "serverInfo" o.serverInfo?⟩
end Lsp
end Lean

28
src/Lean/Data/Lsp/Hover.lean
View file

@ -1,25 +1,39 @@
import Lean.Data.Json
import Lean.Data.Lsp.Basic
/-! Handling of mouse hover requests. -/
namespace Lean
namespace Lsp
open Json
/- The result of a hover request. -/
structure Hover :=
/- The hover's content -/
--(contents: MarkedString | MarkedString[] | MarkupContent)
/- An optional range is a range inside a text document
that is used to visualize a hover, e.g. by changing the background color. -/
/- NOTE we should also accept MarkedString/MarkedString[] here
but they are deprecated, so maybe can get away without. -/
(contents : MarkupContent)
(range? : Option Range := none)
instance Hover.hasFromJson : HasFromJson Hover :=
⟨fun j => do
contents ← j.getObjValAs? MarkupContent "contents";
let range? := j.getObjValAs? Range "range";
pure ⟨contents, range?⟩⟩
instance Hover.hasToJson : HasToJson Hover :=
⟨fun o => mkObj $
⟨"contents", toJson o.contents⟩ ::
opt "range" o.range?⟩
structure HoverParams extends TextDocumentPositionParams
instance hoverParamsHasFromJson : HasFromJson HoverParams :=
instance HoverParams.hasFromJson : HasFromJson HoverParams :=
⟨fun j => do
tdpp : TextDocumentPositionParams ← fromJson? j;
tdpp ← @fromJson? TextDocumentPositionParams _ j;
pure ⟨tdpp⟩⟩
instance HoverParams.hasToJson : HasToJson HoverParams :=
⟨fun o => toJson o.toTextDocumentPositionParams⟩
end Lsp
end Lean

89
src/Lean/Data/Lsp/InitShutdown.lean Normal file
View file

@ -0,0 +1,89 @@
import Lean.Data.Lsp.Capabilities
import Lean.Data.Lsp.Workspace
import Lean.Data.Json
/-! Functionality to do with initializing and shutting down
the server ("General Messages" section of LSP spec). -/
namespace Lean
namespace Lsp
open Json
structure ClientInfo :=
(name : String)
(version? : Option String := none)
instance ClientInfo.hasFromJson : HasFromJson ClientInfo :=
⟨fun j => do
name ← j.getObjValAs? String "name";
let version? := j.getObjValAs? String "version";
pure ⟨name, version?⟩⟩
inductive Trace
| off
| messages
| verbose
instance Trace.hasFromJson : HasFromJson Trace :=
⟨fun j => match j.getStr? with
| some "off" => Trace.off
| some "messages" => Trace.messages
| some "verbose" => Trace.verbose
| _ => none⟩
structure InitializeParams :=
(processId? : Option Int := none)
(clientInfo? : Option ClientInfo := none)
/- We don't support the deprecated rootPath
(rootPath? : Option String) -/
(rootUri? : Option String := none)
(initializationOptions? : Option Json := none)
(capabilities : ClientCapabilities)
/- If omitted, we default to off. -/
(trace : Trace := Trace.off)
(workspaceFolders? : Option (Array WorkspaceFolder) := none)
instance InitializeParams.hasFromJson : HasFromJson InitializeParams :=
⟨fun j => do
/- Many of these params can be null instead of not present.
For ease of implementation, we're liberal:
missing params, wrong json types and null all map to none,
even if LSP sometimes only allows some subset of these.
In cases where LSP makes a meaningful distinction
between different kinds of missing values, we'll
follow accordingly. -/
let processId? := j.getObjValAs? Int "processId";
let clientInfo? := j.getObjValAs? ClientInfo "clientInfo";
let rootUri? := j.getObjValAs? String "rootUri";
let initializationOptions? := j.getObjVal? "initializationOptions";
capabilities ← j.getObjValAs? ClientCapabilities "capabilities";
let trace := (j.getObjValAs? Trace "trace").getD Trace.off;
let workspaceFolders? := j.getObjValAs? (Array WorkspaceFolder) "workspaceFolders";
pure ⟨processId?, clientInfo?, rootUri?, initializationOptions?, capabilities, trace, workspaceFolders?⟩⟩
inductive InitializedParams | mk
instance InitializedParams.hasFromJson : HasFromJson InitializedParams :=
⟨fun j => InitializedParams.mk⟩
structure ServerInfo :=
(name : String)
(version? : Option String := none)
instance ServerInfo.hasToJson : HasToJson ServerInfo :=
⟨fun o => mkObj $
⟨"name", o.name⟩ ::
opt "version" o.version?⟩
structure InitializeResult :=
(capabilities : ServerCapabilities)
(serverInfo? : Option ServerInfo := none)
instance InitializeResult.hasToJson : HasToJson InitializeResult :=
⟨fun o => mkObj $
⟨"capabilities", toJson o.capabilities⟩ ::
opt "serverInfo" o.serverInfo?⟩
end Lsp
end Lean

143
src/Lean/Data/Lsp/TextSync.lean
View file

@ -1,116 +1,105 @@
import Lean.Data.Json
import Lean.Data.Lsp.Basic
/-! Section "Text Document Synchronization" of the LSP spec. -/
namespace Lean
namespace Lsp
open Json
inductive TextDocumentSyncKind
/- Documents should not be synced at all. -/
--| none
/- Documents are synced by always sending the full content of the document. -/
| none
| full
/- Documents are synced by sending the full content on open. After that only incremental updates to the document are send. -/
| incremental
structure TextDocumentSyncOptions :=
/- Open and close notifications are sent to the server.
If omitted open close notification should not be sent. -/
(openClose : Bool)
/- Change notifications are sent to the server.
If omitted it defaults to TextDocumentSyncKind.None.
none: not synced -/
(change? : Option TextDocumentSyncKind := none)
instance TextDocumentSyncKind.hasFromJson : HasFromJson TextDocumentSyncKind :=
⟨fun j => match j.getNat? with
| some 0 => TextDocumentSyncKind.none
| some 1 => TextDocumentSyncKind.full
| some 2 => TextDocumentSyncKind.incremental
| _ => none⟩
instance TextDocumentSyncKind.hasToJson : HasToJson TextDocumentSyncKind :=
⟨fun o => match o with
| TextDocumentSyncKind.none => (0 : Nat)
| TextDocumentSyncKind.full => (1 : Nat)
| TextDocumentSyncKind.incremental => (2 : Nat)⟩
structure DidOpenTextDocumentParams :=
(textDocument : TextDocumentItem)
instance didOpenTextDocumentParamsHasFromJson : HasFromJson DidOpenTextDocumentParams :=
⟨fun j => do
textDocument ← j.getObjValAs? TextDocumentItem "textDocument";
pure ⟨textDocument⟩⟩
instance DidOpenTextDocumentParams.hasFromJson : HasFromJson DidOpenTextDocumentParams :=
⟨fun j => DidOpenTextDocumentParams.mk <$> j.getObjValAs? TextDocumentItem "textDocument"⟩
instance DidOpenTextDocumentParams.hasToJson : HasToJson DidOpenTextDocumentParams :=
⟨fun o => mkObj $ [⟨"textDocument", toJson o.textDocument⟩]⟩
structure TextDocumentChangeRegistrationOptions :=
(documentSelector? : Option DocumentSelector := none)
(syncKind : TextDocumentSyncKind)
instance TextDocumentChangeRegistrationOptions.hasFromJson : HasFromJson TextDocumentChangeRegistrationOptions :=
⟨fun j => do
let documentSelector? := j.getObjValAs? DocumentSelector "documentSelector";
syncKind ← j.getObjValAs? TextDocumentSyncKind "syncKind";
pure ⟨documentSelector?, syncKind⟩⟩
inductive TextDocumentContentChangeEvent
-- omitted: deprecated rangeLength
| rangeChange (range : Range) (text : String)
| fullChange (text : String)
structure DidChangeTextDocumentParams :=
/- The document that did change. The version number points
to the version after all provided content changes have
been applied. -/
(textDocument : VersionedTextDocumentIdentifier)
/- The actual content changes. The content changes describe single state changes
to the document. So if there are two content changes c1 (at array index 0) and
c2 (at array index 1) for a document in state S then c1 moves the document from
S to S' and c2 from S' to S''. So c1 is computed on the state S and c2 is computed
on the state S'.
To mirror the content of a document using change events use the following approach:
- start with the same initial content
- apply the 'textDocument/didChange' notifications in the order you recevie them.
- apply the `TextDocumentContentChangeEvent`s in a single notification in the order
you receive them. -/
(contentChanges : Array TextDocumentContentChangeEvent)
-- TODO: missing:
-- WillSaveTextDocumentParams, TextDocumentSaveReason, SaveOptions
-- TextDocumentSaveRegistrationOptions, DidSaveTextDocumentParams
structure DidCloseTextDocumentParams := (textDocument : TextDocumentIdentifier)
instance textDocumentSyncKindHasFromJson : HasFromJson TextDocumentSyncKind :=
⟨fun j => match j.getNat? with
| some 1 => TextDocumentSyncKind.full
| some 2 => TextDocumentSyncKind.incremental
| _ => none⟩
instance textDocumentSyncKindHasToJson : HasToJson TextDocumentSyncKind :=
⟨fun o => match o with
| TextDocumentSyncKind.full => (1 : Nat)
| TextDocumentSyncKind.incremental => (2 : Nat)⟩
instance textDocumentSyncOptionsHasFromJson : HasFromJson TextDocumentSyncOptions :=
⟨fun j => do
openClose ← j.getObjValAs? Bool "openClose";
let change? := j.getObjValAs? TextDocumentSyncKind "change";
pure ⟨openClose, change?⟩⟩
instance textDocumentSyncOptionsHasToJson : HasToJson TextDocumentSyncOptions :=
⟨fun o => mkObj $
⟨"openClose", o.openClose⟩ :: opt "change" o.change? ++ []⟩
instance textDocumentChangeRegistrationOptionsHasFromJson : HasFromJson TextDocumentChangeRegistrationOptions :=
⟨fun j => do
let documentSelector? := j.getObjValAs? DocumentSelector "documentSelector";
syncKind ← j.getObjValAs? TextDocumentSyncKind "syncKind";
pure ⟨documentSelector?, syncKind⟩⟩
instance textDocumentContentChangeEventHasFromJson : HasFromJson TextDocumentContentChangeEvent :=
instance TextDocumentContentChangeEvent.hasFromJson : HasFromJson TextDocumentContentChangeEvent :=
⟨fun j =>
(do
range ← j.getObjValAs? Range "range";
text ← j.getObjValAs? String "text";
pure (TextDocumentContentChangeEvent.rangeChange range text)) <|>
(do
text ← j.getObjValAs? String "text";
pure (TextDocumentContentChangeEvent.fullChange text))⟩
pure $ TextDocumentContentChangeEvent.rangeChange range text) <|>
(TextDocumentContentChangeEvent.fullChange <$> j.getObjValAs? String "text")⟩
instance didChangeTextDocumentParamsHasFromJson : HasFromJson DidChangeTextDocumentParams :=
structure DidChangeTextDocumentParams :=
(textDocument : VersionedTextDocumentIdentifier)
(contentChanges : Array TextDocumentContentChangeEvent)
instance DidChangeTextDocumentParams.hasFromJson : HasFromJson DidChangeTextDocumentParams :=
⟨fun j => do
textDocument ← j.getObjValAs? VersionedTextDocumentIdentifier "textDocument";
contentChanges ← j.getObjValAs? (Array TextDocumentContentChangeEvent) "contentChanges";
pure ⟨textDocument, contentChanges⟩⟩
instance didCloseTextDocumentParamsHasFromJson : HasFromJson DidCloseTextDocumentParams :=
⟨fun j => do
textDocument ← j.getObjValAs? TextDocumentIdentifier "textDocument";
pure ⟨textDocument⟩⟩
-- TODO: missing:
-- WillSaveTextDocumentParams, TextDocumentSaveReason,
-- TextDocumentSaveRegistrationOptions, DidSaveTextDocumentParams
structure SaveOptions := (includeText : Bool)
instance SaveOptions.hasToJson : HasToJson SaveOptions :=
⟨fun o => mkObj $ [⟨"includeText", o.includeText⟩]⟩
structure DidCloseTextDocumentParams := (textDocument : TextDocumentIdentifier)
instance DidCloseTextDocumentParams.hasFromJson : HasFromJson DidCloseTextDocumentParams :=
⟨fun j => DidCloseTextDocumentParams.mk <$> j.getObjValAs? TextDocumentIdentifier "textDocument"⟩
-- TODO: TextDocumentSyncClientCapabilities
/- NOTE: This is defined twice in the spec. The latter version has more fields. -/
structure TextDocumentSyncOptions :=
(openClose : Bool)
(change : TextDocumentSyncKind)
(willSave : Bool)
(willSaveWaitUntil : Bool)
(save? : Option SaveOptions := none)
instance TextDocumentSyncOptions.hasToJson : HasToJson TextDocumentSyncOptions :=
⟨fun o => mkObj $
opt "save" o.save? ++
[ ⟨"openClose", toJson o.openClose⟩
, ⟨"change", toJson o.change⟩
, ⟨"willSave", toJson o.willSave⟩
, ⟨"willSaveWaitUntil", toJson o.willSaveWaitUntil⟩
]⟩
end Lsp
end Lean

8
src/Lean/Data/Lsp/Utf16.lean
View file

@ -2,8 +2,8 @@ import Init.Data.String
import Init.Data.Array
import Lean.Data.Lsp.Basic
-- LSP uses UTF-16 for indexing, so we need to provide some primitives
-- to interact with Lean strings using UTF-16 indices
/-! LSP uses UTF-16 for indexing, so we need to provide some primitives
to interact with Lean strings using UTF-16 indices. -/
namespace Char
@ -14,7 +14,7 @@ end Char
namespace String
-- LSP is EOL agnostic, so we first split on "\r\n" to avoid possibly redundant line breaks
/-- LSP is EOL agnostic, so we first split on "\r\n" to avoid possibly redundant line breaks. -/
def splitOnEOLs (s : String) : List String := do
line ← s.splitOn "\r\n";
line ← line.splitOn "\n";
@ -43,7 +43,7 @@ utf16PosToCodepointPosAux s.toList pos 0
def utf16Length (s : String) : Nat :=
s.foldr (fun c acc => csize c + acc) 0
-- delete text until endIdx
/-- Delete text until endIdx. -/
private def utf16ReplaceAux₀ : List Char → Nat → Nat → List Char
| [], i, endIdx => [] -- no more text to delete
| (c :: s), i, endIdx =>

31
src/Lean/Data/Lsp/Workspace.lean Normal file
View file

@ -0,0 +1,31 @@
import Lean.Data.Lsp.Basic
import Lean.Data.Json
namespace Lean
namespace Lsp
open Json
structure WorkspaceFolder :=
(uri : DocumentUri)
(name : String)
instance WorkspaceFolder.hasFromJson : HasFromJson WorkspaceFolder :=
⟨fun j => do
uri ← j.getObjValAs? DocumentUri "uri";
name ← j.getObjValAs? String "name";
pure ⟨uri, name⟩⟩
instance WorkspaceFolder.hasToJson : HasToJson WorkspaceFolder :=
⟨fun o => mkObj $
[ ⟨"uri", toJson o.uri⟩
, ⟨"name", toJson o.name⟩
]⟩
-- TODO(WN):
-- WorkspaceFoldersServerCapabilities,
-- DidChangeWorkspaceFoldersParams,
-- WorkspaceFoldersChangeEvent
end Lsp
end Lean

20
src/Lean/Server.lean
View file

@ -186,11 +186,8 @@ match method with
def handleRequest (id : RequestID) (method : String) (params : Json)
: ServerM Unit := do
let h := (fun paramType responseType [HasFromJson paramType] [HasToJson responseType]
(handler : paramType → ServerM responseType) => do
-- NOTE: for some reason Lean is unhappy with a >>= chain here
p ← parseParams paramType params;
reply ← handler p;
writeLspResponse id reply);
(handler : paramType → ServerM responseType) =>
parseParams paramType params >>= handler >>= writeLspResponse id);
match method with
| "textDocument/hover" => h HoverParams Json handleHover
| _ => throw (userError "got unsupported request")
@ -207,7 +204,16 @@ partial def mainLoop : Unit → ServerM Unit
| Message.notification method (some params) => do
handleNotification method (toJson params);
mainLoop ()
| _ => throw (userError "got invalid jsonrpc message")
| _ => throw (userError "got invalid JSON-RPC message")
def mkLeanServerCapabilities : ServerCapabilities :=
{ textDocumentSync? := some
{ openClose := true
, change := TextDocumentSyncKind.incremental
, willSave := false
, willSaveWaitUntil := false
, save? := none }
, hoverProvider := true }
def initAndRunServer (i o : FS.Handle) : IO Unit := do
openDocumentsRef ← IO.mkRef (RBMap.empty : DocumentMap);
@ -219,7 +225,7 @@ def initAndRunServer (i o : FS.Handle) : IO Unit := do
{ capabilities := mkLeanServerCapabilities
, serverInfo? := some { name := "Lean 4 server"
, version? := "0.0.1" } : InitializeResult };
_ ← readLspNotificationAs "initialized" Initialized;
_ ← readLspNotificationAs "initialized" InitializedParams;
mainLoop ();
Message.notification "exit" none ← readLspMessage
| throw (userError "Expected an Exit Notification.");

6
src/Lean/Server/README.md
View file

@ -5,6 +5,12 @@
leanmake +lean4 bin PKG=ServerBin LINK_OPTS=-rdynamic
```
## Server code style
Comments should exist to denote specifics of our implementation but, for
the most part, we shouldn't copy comments over from the LSP specification
to avoid unnecessary duplication.
## Logging LSP requests
### In `bash`:

6
tests/lean/server/diags.lean.expected.out
View file

@ -1,7 +1,7 @@
Content-Length: 178
Content-Length: 221
{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 1020
{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"willSaveWaitUntil":false,"willSave":false,"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 1020
{"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":28},"end":{"line":14,"character":28}},"message":"type mismatch\n \"NotANat\"\nhas type\n String\nbut it is expected to have type\n Nat\nfailed to synthesize instance\n CoeT String \"NotANat\" Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 38
{"result":null,"jsonrpc":"2.0","id":1}
{"result":null,"jsonrpc":"2.0","id":1}

6
tests/lean/server/edits.lean.expected.out
View file

@ -1,6 +1,6 @@
Content-Length: 178
Content-Length: 221
{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 1020
{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"willSaveWaitUntil":false,"willSave":false,"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 1020
{"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":28},"end":{"line":14,"character":28}},"message":"type mismatch\n \"NotANat\"\nhas type\n String\nbut it is expected to have type\n Nat\nfailed to synthesize instance\n CoeT String \"NotANat\" Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 184
@ -44,4 +44,4 @@ Content-Length: 178
{"params":{"version":11,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 38
{"result":null,"jsonrpc":"2.0","id":1}
{"result":null,"jsonrpc":"2.0","id":1}

4
tests/lean/server/init_exit.lean.expected.out
View file

@ -1,5 +1,5 @@
Content-Length: 178
Content-Length: 221
{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 38
{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"willSaveWaitUntil":false,"willSave":false,"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 38
{"result":null,"jsonrpc":"2.0","id":1}