Implementation of JSON-RPC 2.0 (https://www.jsonrpc.org/specification) for use in the LSP server.

inductive Lean.JsonRpc.RequestID : Type

In JSON-RPC, each request from the client editor to the language server comes with a request id so that the corresponding response can be identified or cancelled.

• str (s : String) : RequestID
• num (n : JsonNumber) : RequestID
• null : RequestID

@[implicit_reducible]

instance Lean.JsonRpc.instInhabitedRequestID : Inhabited RequestID

def Lean.JsonRpc.instInhabitedRequestID.default : RequestID

@[implicit_reducible]

instance Lean.JsonRpc.instBEqRequestID : BEq RequestID

def Lean.JsonRpc.instBEqRequestID.beq : RequestID → RequestID → Bool

@[implicit_reducible]

instance Lean.JsonRpc.instHashableRequestID : Hashable RequestID

def Lean.JsonRpc.instHashableRequestID.hash : RequestID → UInt64

def Lean.JsonRpc.instOrdRequestID.ord : RequestID → RequestID → Ordering

@[implicit_reducible]

instance Lean.JsonRpc.instOrdRequestID : Ord RequestID

@[implicit_reducible]

instance Lean.JsonRpc.instOfNatRequestID {n : Nat} : OfNat RequestID n

@[implicit_reducible]

instance Lean.JsonRpc.instToStringRequestID : ToString RequestID

inductive Lean.JsonRpc.ErrorCode : Type

Error codes defined by JSON-RPC and LSP.

• parseError : ErrorCode

  Invalid JSON was received by the server. An error occurred on the server while parsing the JSON text.

• invalidRequest : ErrorCode

  The JSON sent is not a valid Request object.

• methodNotFound : ErrorCode

  The method does not exist / is not available.

• invalidParams : ErrorCode

  Invalid method parameter(s).

• internalError : ErrorCode

  Internal JSON-RPC error.

• serverNotInitialized : ErrorCode

  Error code indicating that a server received a notification or request before the server has received the initialize request.

• unknownErrorCode : ErrorCode
• contentModified : ErrorCode

  The server detected that the content of a document got modified outside normal conditions. A server should NOT send this error code if it detects a content change in it unprocessed messages. The result even computed on an older state might still be useful for the client.

  If a client decides that a result is not of any use anymore the client should cancel the request.

• requestCancelled : ErrorCode

  The client has canceled a request and a server as detected the cancel.

• rpcNeedsReconnect : ErrorCode
• workerExited : ErrorCode
• workerCrashed : ErrorCode

def Lean.JsonRpc.instInhabitedErrorCode.default : ErrorCode

@[implicit_reducible]

instance Lean.JsonRpc.instInhabitedErrorCode : Inhabited ErrorCode

def Lean.JsonRpc.instBEqErrorCode.beq : ErrorCode → ErrorCode → Bool

@[implicit_reducible]

instance Lean.JsonRpc.instBEqErrorCode : BEq ErrorCode

@[implicit_reducible]

instance Lean.JsonRpc.instFromJsonErrorCode : FromJson ErrorCode

@[implicit_reducible]

instance Lean.JsonRpc.instToJsonErrorCode : ToJson ErrorCode

inductive Lean.JsonRpc.Message : Type

A JSON-RPC message.

Uses separate constructors for notifications and errors because client and server behavior is expected to be wildly different for both.

• request (id : RequestID) (method : String) (params? : Option Json.Structured) : Message

  A request message to describe a request between the client and the server. Every processed request must send a response back to the sender of the request.

• notification (method : String) (params? : Option Json.Structured) : Message

  A notification message. A processed notification message must not send a response back. They work like events.

• response (id : RequestID) (result : Json) : Message

  A Response Message sent as a result of a request.

• responseError (id : RequestID) (code : ErrorCode) (message : String) (data? : Option Json) : Message

  A non-successful response.

@[implicit_reducible]

instance Lean.JsonRpc.instInhabitedMessage : Inhabited Message

def Lean.JsonRpc.instInhabitedMessage.default : Message

def Lean.JsonRpc.Batch : Type

structure Lean.JsonRpc.Request (α : Type u) : Type u

Generic version of Message.request.

A request message to describe a request between the client and the server. Every processed request must send a response back to the sender of the request.

• LSP
• JSON-RPC

• id : RequestID
• method : String
• param : α

def Lean.JsonRpc.instInhabitedRequest.default {a✝ : Type u_1} [Inhabited a✝] : Request a✝

@[implicit_reducible]

instance Lean.JsonRpc.instInhabitedRequest {a✝ : Type u_1} [Inhabited a✝] : Inhabited (Request a✝)

@[implicit_reducible]

instance Lean.JsonRpc.instBEqRequest {α✝ : Type u_1} [BEq α✝] : BEq (Request α✝)

def Lean.JsonRpc.instBEqRequest.beq {α✝ : Type u_1} [BEq α✝] : Request α✝ → Request α✝ → Bool

@[implicit_reducible]

instance Lean.JsonRpc.instCoeOutRequestMessageOfToJson {α : Type u_1} [ToJson α] : CoeOut (Request α) Message

def Lean.JsonRpc.Request.ofMessage? : Message → Option (Request Json)

structure Lean.JsonRpc.Notification (α : Type u) : Type u

Generic version of Message.notification.

A notification message. A processed notification message must not send a response back. They work like events.

• JSON-RPC
• LSP.

• method : String
• param : α

@[implicit_reducible]

instance Lean.JsonRpc.instInhabitedNotification {a✝ : Type u_1} [Inhabited a✝] : Inhabited (Notification a✝)

def Lean.JsonRpc.instInhabitedNotification.default {a✝ : Type u_1} [Inhabited a✝] : Notification a✝

def Lean.JsonRpc.instBEqNotification.beq {α✝ : Type u_1} [BEq α✝] : Notification α✝ → Notification α✝ → Bool

@[implicit_reducible]

instance Lean.JsonRpc.instBEqNotification {α✝ : Type u_1} [BEq α✝] : BEq (Notification α✝)

@[implicit_reducible]

instance Lean.JsonRpc.instCoeOutNotificationMessageOfToJson {α : Type u_1} [ToJson α] : CoeOut (Notification α) Message

def Lean.JsonRpc.Notification.ofMessage? : Message → Option (Notification Json)

structure Lean.JsonRpc.Response (α : Type u) : Type u

Generic version of Message.response.

A Response Message sent as a result of a request. If a request doesn’t provide a result value the receiver of a request still needs to return a response message to conform to the JSON-RPC specification. The result property of the ResponseMessage should be set to null in this case to signal a successful request.

References:

• JSON-RPC
• LSP

• id : RequestID
• result : α

@[implicit_reducible]

instance Lean.JsonRpc.instInhabitedResponse {a✝ : Type u_1} [Inhabited a✝] : Inhabited (Response a✝)

def Lean.JsonRpc.instInhabitedResponse.default {a✝ : Type u_1} [Inhabited a✝] : Response a✝

@[implicit_reducible]

instance Lean.JsonRpc.instBEqResponse {α✝ : Type u_1} [BEq α✝] : BEq (Response α✝)

def Lean.JsonRpc.instBEqResponse.beq {α✝ : Type u_1} [BEq α✝] : Response α✝ → Response α✝ → Bool

@[implicit_reducible]

instance Lean.JsonRpc.instCoeOutResponseMessageOfToJson {α : Type u_1} [ToJson α] : CoeOut (Response α) Message

def Lean.JsonRpc.Response.ofMessage? : Message → Option (Response Json)

structure Lean.JsonRpc.ResponseError (α : Type u) : Type u

Generic version of Message.responseError.

References:

• JSON-RPC
• LSP.

• id : RequestID
• code : ErrorCode
• message : String

  A string providing a short description of the error.

• data? : Option α

  A primitive or structured value that contains additional information about the error. Can be omitted.

def Lean.JsonRpc.instInhabitedResponseError.default {a✝ : Type u_1} : ResponseError a✝

@[implicit_reducible]

instance Lean.JsonRpc.instInhabitedResponseError {a✝ : Type u_1} : Inhabited (ResponseError a✝)

@[implicit_reducible]

instance Lean.JsonRpc.instBEqResponseError {α✝ : Type u_1} [BEq α✝] : BEq (ResponseError α✝)

def Lean.JsonRpc.instBEqResponseError.beq {α✝ : Type u_1} [BEq α✝] : ResponseError α✝ → ResponseError α✝ → Bool

@[implicit_reducible]

instance Lean.JsonRpc.instCoeOutResponseErrorMessageOfToJson {α : Type u_1} [ToJson α] : CoeOut (ResponseError α) Message

@[implicit_reducible]

instance Lean.JsonRpc.instCoeOutResponseErrorUnitMessage : CoeOut (ResponseError Unit) Message

def Lean.JsonRpc.ResponseError.ofMessage? : Message → Option (ResponseError Json)

@[implicit_reducible]

instance Lean.JsonRpc.instCoeStringRequestID : Coe String RequestID

@[implicit_reducible]

instance Lean.JsonRpc.instCoeJsonNumberRequestID : Coe JsonNumber RequestID

def Lean.JsonRpc.RequestID.lt : RequestID → RequestID → Bool

@[implicit_reducible]

def Lean.JsonRpc.RequestID.ltProp : LT RequestID

@[implicit_reducible]

instance Lean.JsonRpc.instLTRequestID : LT RequestID

@[implicit_reducible]

instance Lean.JsonRpc.instDecidableLtRequestID (a b : RequestID) : Decidable (a < b)

@[implicit_reducible]

instance Lean.JsonRpc.instFromJsonRequestID : FromJson RequestID

@[implicit_reducible]

instance Lean.JsonRpc.instToJsonRequestID : ToJson RequestID

@[implicit_reducible]

instance Lean.JsonRpc.instToJsonMessage : ToJson Message

@[implicit_reducible]

instance Lean.JsonRpc.instFromJsonMessage : FromJson Message

@[implicit_reducible]

instance Lean.JsonRpc.instFromJsonNotification {α : Type} [FromJson α] : FromJson (Notification α)

inductive Lean.JsonRpc.MessageMetaData : Type

A variant of Message that has been parsed partially, without the payload. This is useful when we want to process the metadata of a Message without parsing and converting the whole thing.

• request (id : RequestID) (method : String) : MessageMetaData
• notification (method : String) : MessageMetaData
• response (id : RequestID) : MessageMetaData
• responseError (id : RequestID) (code : ErrorCode) (message : String) (data? : Option Json) : MessageMetaData

@[implicit_reducible]

instance Lean.JsonRpc.instInhabitedMessageMetaData : Inhabited MessageMetaData

def Lean.JsonRpc.instInhabitedMessageMetaData.default : MessageMetaData

def Lean.JsonRpc.Message.metaData : Message → MessageMetaData

def Lean.JsonRpc.MessageMetaData.toMessage : MessageMetaData → Message

def Lean.JsonRpc.parseMessageMetaData (input : String) : Except String MessageMetaData

Danger: For performance reasons, this function makes a number of fragile assumptions about input. Namely:

• input is the output of (toJson (v : Message)).compress
• compress yields a lexicographic ordering of JSON object keys

inductive Lean.JsonRpc.MessageDirection : Type

• clientToServer : MessageDirection
• serverToClient : MessageDirection

@[implicit_reducible]

instance Lean.JsonRpc.instInhabitedMessageDirection : Inhabited MessageDirection

def Lean.JsonRpc.instInhabitedMessageDirection.default : MessageDirection

@[implicit_reducible]

instance Lean.JsonRpc.instFromJsonMessageDirection : FromJson MessageDirection

def Lean.JsonRpc.instFromJsonMessageDirection.fromJson : Json → Except String MessageDirection

@[implicit_reducible]

instance Lean.JsonRpc.instToJsonMessageDirection : ToJson MessageDirection

def Lean.JsonRpc.instToJsonMessageDirection.toJson : MessageDirection → Json

inductive Lean.JsonRpc.MessageKind : Type

• request : MessageKind
• notification : MessageKind
• response : MessageKind
• responseError : MessageKind

@[implicit_reducible]

instance Lean.JsonRpc.instFromJsonMessageKind : FromJson MessageKind

def Lean.JsonRpc.instFromJsonMessageKind.fromJson : Json → Except String MessageKind

@[implicit_reducible]

instance Lean.JsonRpc.instToJsonMessageKind : ToJson MessageKind

def Lean.JsonRpc.instToJsonMessageKind.toJson : MessageKind → Json

def Lean.JsonRpc.MessageKind.ofMessage : Message → MessageKind

def IO.FS.Stream.readMessage (h : Stream) (nBytes : Nat) : IO Lean.JsonRpc.Message

def IO.FS.Stream.readRequestAs (h : Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [Lean.FromJson α] : IO (Lean.JsonRpc.Request α)

def IO.FS.Stream.readNotificationAs (h : Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [Lean.FromJson α] : IO (Lean.JsonRpc.Notification α)

def IO.FS.Stream.readResponseAs (h : Stream) (nBytes : Nat) (expectedID : Lean.JsonRpc.RequestID) (α : Type) [Lean.FromJson α] : IO (Lean.JsonRpc.Response α)

def IO.FS.Stream.writeMessage (h : Stream) (m : Lean.JsonRpc.Message) : IO Unit

def IO.FS.Stream.writeRequest {α : Type u_1} [Lean.ToJson α] (h : Stream) (r : Lean.JsonRpc.Request α) : IO Unit

def IO.FS.Stream.writeNotification {α : Type u_1} [Lean.ToJson α] (h : Stream) (n : Lean.JsonRpc.Notification α) : IO Unit

def IO.FS.Stream.writeResponse {α : Type u_1} [Lean.ToJson α] (h : Stream) (r : Lean.JsonRpc.Response α) : IO Unit

def IO.FS.Stream.writeResponseError (h : Stream) (e : Lean.JsonRpc.ResponseError Unit) : IO Unit

def IO.FS.Stream.writeResponseErrorWithData {α : Type u_1} [Lean.ToJson α] (h : Stream) (e : Lean.JsonRpc.ResponseError α) : IO Unit