This file contains types for communication between the watchdog and the workers. These messages are not visible externally to users of the LSP server.

Most reference-related types have custom FromJson/ToJson implementations to reduce the size of the resulting JSON.

structure Lean.Lsp.ImportInfo : Type

Information about a single import statement.

• module : String

  Name of the module that is imported.

• isPrivate : Bool

  Whether the module is being imported via private import.

• isAll : Bool

  Whether the module is being imported via import all.

• isMeta : Bool

  Whether the module is being imported via meta import.

instance Lean.Lsp.instInhabitedImportInfo : Inhabited ImportInfo

Equations

• Lean.Lsp.instInhabitedImportInfo = { default := { module := default, isPrivate := default, isAll := default, isMeta := default } }

instance Lean.Lsp.instToJsonImportInfo : ToJson ImportInfo

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Lsp.instFromJsonImportInfo : FromJson ImportInfo

Equations

• One or more equations did not get rendered due to their size.

inductive Lean.Lsp.RefIdent : Type

Identifier of a reference.

• const (moduleName identName : String) : RefIdent

  Named identifier. These are used in all references that are globally available.

• fvar (moduleName id : String) : RefIdent

  Unnamed identifier. These are used for all local references.

instance Lean.Lsp.instBEqRefIdent : BEq RefIdent

Equations

• Lean.Lsp.instBEqRefIdent = { beq := Lean.Lsp.beqRefIdent✝ }

instance Lean.Lsp.instHashableRefIdent : Hashable RefIdent

Equations

• Lean.Lsp.instHashableRefIdent = { hash := Lean.Lsp.hashRefIdent✝ }

instance Lean.Lsp.instInhabitedRefIdent : Inhabited RefIdent

Equations

• Lean.Lsp.instInhabitedRefIdent = { default := Lean.Lsp.RefIdent.const default default }

instance Lean.Lsp.instOrdRefIdent : Ord RefIdent

Equations

• Lean.Lsp.instOrdRefIdent = { compare := Lean.Lsp.ordRefIdent✝ }

inductive Lean.Lsp.RefIdent.RefIdentJsonRepr : Type

Shortened representation of RefIdent for more compact serialization.

• c (m n : String) : RefIdentJsonRepr

  Shortened representation of RefIdent.const for more compact serialization.

• f (m i : String) : RefIdentJsonRepr

  Shortened representation of RefIdent.fvar for more compact serialization.

instance Lean.Lsp.RefIdent.instFromJsonRefIdentJsonRepr : FromJson RefIdentJsonRepr

Equations

• Lean.Lsp.RefIdent.instFromJsonRefIdentJsonRepr = { fromJson? := Lean.Lsp.RefIdent.fromJsonRefIdentJsonRepr✝ }

instance Lean.Lsp.RefIdent.instToJsonRefIdentJsonRepr : ToJson RefIdentJsonRepr

Equations

• Lean.Lsp.RefIdent.instToJsonRefIdentJsonRepr = { toJson := Lean.Lsp.RefIdent.toJsonRefIdentJsonRepr✝ }

def Lean.Lsp.RefIdent.toJsonRepr (id : RefIdent) : RefIdentJsonRepr

Converts id to its compact serialization representation.

Equations

• (Lean.Lsp.RefIdent.const a a_1).toJsonRepr = Lean.Lsp.RefIdent.RefIdentJsonRepr.c a a_1
• (Lean.Lsp.RefIdent.fvar a a_1).toJsonRepr = Lean.Lsp.RefIdent.RefIdentJsonRepr.f a a_1

def Lean.Lsp.RefIdent.fromJsonRepr (repr : RefIdentJsonRepr) : RefIdent

Converts repr to RefIdent.

Equations

• Lean.Lsp.RefIdent.fromJsonRepr (Lean.Lsp.RefIdent.RefIdentJsonRepr.c a a_1) = Lean.Lsp.RefIdent.const a a_1
• Lean.Lsp.RefIdent.fromJsonRepr (Lean.Lsp.RefIdent.RefIdentJsonRepr.f a a_1) = Lean.Lsp.RefIdent.fvar a a_1

def Lean.Lsp.RefIdent.fromJson? (s : Json) : Except String RefIdent

Converts RefIdent from a JSON for RefIdentJsonRepr.

Equations

• Lean.Lsp.RefIdent.fromJson? s = do let __do_lift ← Lean.fromJson? s pure (Lean.Lsp.RefIdent.fromJsonRepr __do_lift)

def Lean.Lsp.RefIdent.toJson (id : RefIdent) : Json

Converts RefIdent to a JSON for RefIdentJsonRepr.

Equations

• id.toJson = Lean.toJson id.toJsonRepr

instance Lean.Lsp.RefIdent.instFromJson : FromJson RefIdent

Equations

• Lean.Lsp.RefIdent.instFromJson = { fromJson? := Lean.Lsp.RefIdent.fromJson? }

instance Lean.Lsp.RefIdent.instToJson : ToJson RefIdent

Equations

• Lean.Lsp.RefIdent.instToJson = { toJson := Lean.Lsp.RefIdent.toJson }

structure Lean.Lsp.RefInfo.ParentDecl : Type

Information about the declaration surrounding a reference.

• name : String

  Name of the declaration surrounding a reference.

• range : Range

  Range of the declaration surrounding a reference.

• selectionRange : Range

  Selection range of the declaration surrounding a reference.

instance Lean.Lsp.RefInfo.instToJsonParentDecl : ToJson ParentDecl

Equations

• Lean.Lsp.RefInfo.instToJsonParentDecl = { toJson := Lean.Lsp.RefInfo.toJsonParentDecl✝ }

structure Lean.Lsp.RefInfo.Location : Type

Denotes the range of a reference, as well as the parent declaration of the reference. If the reference is itself a declaration, then it contains no parent declaration.

• range : Range

  Range of the reference.

• parentDecl? : Option ParentDecl

  Parent declaration of the reference. none if the reference is itself a declaration.

instance Lean.Lsp.RefInfo.instInhabitedLocation : Inhabited Location

Equations

• Lean.Lsp.RefInfo.instInhabitedLocation = { default := { range := default, parentDecl? := default } }

structure Lean.Lsp.RefInfo : Type

Definition site and usage sites of a reference. Obtained from Lean.Server.RefInfo.

• definition? : Option Location

  Definition site of the reference. May be none when we cannot find a definition site.

• usages : Array Location

  Usage sites of the reference.

instance Lean.Lsp.instToJsonRefInfo : ToJson RefInfo

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Lsp.instFromJsonRefInfo : FromJson RefInfo

Equations

• One or more equations did not get rendered due to their size.

def Lean.Lsp.ModuleRefs : Type

References from a single module/file

Equations

• Lean.Lsp.ModuleRefs = Std.TreeMap Lean.Lsp.RefIdent Lean.Lsp.RefInfo compare

instance Lean.Lsp.instEmptyCollectionModuleRefs : EmptyCollection ModuleRefs

Equations

• Lean.Lsp.instEmptyCollectionModuleRefs = Std.TreeMap.instEmptyCollection

instance Lean.Lsp.instForInModuleRefsProdRefIdentRefInfo {m : Type u_1 → Type u_2} : ForIn m ModuleRefs (RefIdent × RefInfo)

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Lsp.instToJsonModuleRefs : ToJson ModuleRefs

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Lsp.instFromJsonModuleRefs : FromJson ModuleRefs

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Lsp.LeanILeanHeaderInfoParams : Type

Used in the $/lean/ileanHeaderInfo watchdog <- worker notifications. Contains the direct imports of the file managed by a worker.

• version : Nat

  Version of the file these imports are from.

• directImports : Array ImportInfo

  Direct imports of this file.

instance Lean.Lsp.instFromJsonLeanILeanHeaderInfoParams : FromJson LeanILeanHeaderInfoParams

Equations

• Lean.Lsp.instFromJsonLeanILeanHeaderInfoParams = { fromJson? := Lean.Lsp.fromJsonLeanILeanHeaderInfoParams✝ }

instance Lean.Lsp.instToJsonLeanILeanHeaderInfoParams : ToJson LeanILeanHeaderInfoParams

Equations

• Lean.Lsp.instToJsonLeanILeanHeaderInfoParams = { toJson := Lean.Lsp.toJsonLeanILeanHeaderInfoParams✝ }

structure Lean.Lsp.LeanIleanInfoParams : Type

Used in the $/lean/ileanInfoUpdate and $/lean/ileanInfoFinal watchdog <- worker notifications. Contains the definitions and references of the file managed by a worker.

• version : Nat

  Version of the file these references are from.

• references : ModuleRefs

  All references for the file.

instance Lean.Lsp.instFromJsonLeanIleanInfoParams : FromJson LeanIleanInfoParams

Equations

• Lean.Lsp.instFromJsonLeanIleanInfoParams = { fromJson? := Lean.Lsp.fromJsonLeanIleanInfoParams✝ }

instance Lean.Lsp.instToJsonLeanIleanInfoParams : ToJson LeanIleanInfoParams

Equations

• Lean.Lsp.instToJsonLeanIleanInfoParams = { toJson := Lean.Lsp.toJsonLeanIleanInfoParams✝ }

structure Lean.Lsp.LeanImportClosureParams : Type

Used in the $/lean/importClosure watchdog <- worker notification. Contains the full import closure of the file managed by a worker.

• importClosure : Array DocumentUri

  Full import closure of the file.

instance Lean.Lsp.instFromJsonLeanImportClosureParams : FromJson LeanImportClosureParams

Equations

• Lean.Lsp.instFromJsonLeanImportClosureParams = { fromJson? := Lean.Lsp.fromJsonLeanImportClosureParams✝ }

instance Lean.Lsp.instToJsonLeanImportClosureParams : ToJson LeanImportClosureParams

Equations

• Lean.Lsp.instToJsonLeanImportClosureParams = { toJson := Lean.Lsp.toJsonLeanImportClosureParams✝ }

structure Lean.Lsp.LeanStaleDependencyParams : Type

Used in the $/lean/importClosure watchdog -> worker notification. Informs the worker that one of its dependencies has gone stale and likely needs to be rebuilt.

• staleDependency : DocumentUri

  The dependency that is stale.

instance Lean.Lsp.instFromJsonLeanStaleDependencyParams : FromJson LeanStaleDependencyParams

Equations

• Lean.Lsp.instFromJsonLeanStaleDependencyParams = { fromJson? := Lean.Lsp.fromJsonLeanStaleDependencyParams✝ }

instance Lean.Lsp.instToJsonLeanStaleDependencyParams : ToJson LeanStaleDependencyParams

Equations

• Lean.Lsp.instToJsonLeanStaleDependencyParams = { toJson := Lean.Lsp.toJsonLeanStaleDependencyParams✝ }

inductive Lean.Lsp.OpenNamespace : Type

LSP type for Lean.OpenDecl.

• allExcept («namespace» : Name) (exceptions : Array Name) : OpenNamespace

  All declarations in «namespace» are opened, except for exceptions.

• renamed («from» to : Name) : OpenNamespace

  The declaration «from» is renamed to to.

instance Lean.Lsp.instFromJsonOpenNamespace : FromJson OpenNamespace

Equations

• Lean.Lsp.instFromJsonOpenNamespace = { fromJson? := Lean.Lsp.fromJsonOpenNamespace✝ }

instance Lean.Lsp.instToJsonOpenNamespace : ToJson OpenNamespace

Equations

• Lean.Lsp.instToJsonOpenNamespace = { toJson := Lean.Lsp.toJsonOpenNamespace✝ }

structure Lean.Lsp.LeanModuleQuery : Type

Query in the $/lean/queryModule watchdog <- worker request.

• identifier : String

  Identifier (potentially partial) to query.

• openNamespaces : Array OpenNamespace

  Namespaces that are open at the position of identifier. Used for accurately matching declarations against identifier in context.

instance Lean.Lsp.instFromJsonLeanModuleQuery : FromJson LeanModuleQuery

Equations

• Lean.Lsp.instFromJsonLeanModuleQuery = { fromJson? := Lean.Lsp.fromJsonLeanModuleQuery✝ }

instance Lean.Lsp.instToJsonLeanModuleQuery : ToJson LeanModuleQuery

Equations

• Lean.Lsp.instToJsonLeanModuleQuery = { toJson := Lean.Lsp.toJsonLeanModuleQuery✝ }

structure Lean.Lsp.LeanQueryModuleParams : Type

Used in the $/lean/queryModule watchdog <- worker request, which is used by the worker to extract information from the .ilean information in the watchdog.

• sourceRequestID : JsonRpc.RequestID

  The request ID in the context of which this worker -> watchdog request was emitted. Used for cancelling this request in the watchdog.

• queries : Array LeanModuleQuery

  Module queries for extracting .ilean information in the watchdog.

instance Lean.Lsp.instFromJsonLeanQueryModuleParams : FromJson LeanQueryModuleParams

Equations

• Lean.Lsp.instFromJsonLeanQueryModuleParams = { fromJson? := Lean.Lsp.fromJsonLeanQueryModuleParams✝ }

instance Lean.Lsp.instToJsonLeanQueryModuleParams : ToJson LeanQueryModuleParams

Equations

• Lean.Lsp.instToJsonLeanQueryModuleParams = { toJson := Lean.Lsp.toJsonLeanQueryModuleParams✝ }

structure Lean.Lsp.LeanIdentifier : Type

Result entry of a module query.

• module : Name

  Module that decl is defined in.

• decl : Name

  Full name of the declaration that matches the query.

• isExactMatch : Bool

  Whether this decl matched the query exactly.

instance Lean.Lsp.instFromJsonLeanIdentifier : FromJson LeanIdentifier

Equations

• Lean.Lsp.instFromJsonLeanIdentifier = { fromJson? := Lean.Lsp.fromJsonLeanIdentifier✝ }

instance Lean.Lsp.instToJsonLeanIdentifier : ToJson LeanIdentifier

Equations

• Lean.Lsp.instToJsonLeanIdentifier = { toJson := Lean.Lsp.toJsonLeanIdentifier✝ }

@[reducible, inline]

abbrev Lean.Lsp.LeanQueriedModule : Type

Result for a single module query. Identifiers in the response are sorted descendingly by how well they match the query.

Equations

• Lean.Lsp.LeanQueriedModule = Array Lean.Lsp.LeanIdentifier

structure Lean.Lsp.LeanQueryModuleResponse : Type

Response for the $/lean/queryModule watchdog <- worker request.

• queryResults : Array LeanQueriedModule

  Results for each query in LeanQueryModuleParams. Positions correspond to queries in the parameter of the request.

instance Lean.Lsp.instFromJsonLeanQueryModuleResponse : FromJson LeanQueryModuleResponse

Equations

• Lean.Lsp.instFromJsonLeanQueryModuleResponse = { fromJson? := Lean.Lsp.fromJsonLeanQueryModuleResponse✝ }

instance Lean.Lsp.instToJsonLeanQueryModuleResponse : ToJson LeanQueryModuleResponse

Equations

• Lean.Lsp.instToJsonLeanQueryModuleResponse = { toJson := Lean.Lsp.toJsonLeanQueryModuleResponse✝ }

instance Lean.Lsp.instInhabitedLeanQueryModuleResponse : Inhabited LeanQueryModuleResponse

Equations

• Lean.Lsp.instInhabitedLeanQueryModuleResponse = { default := { queryResults := default } }

structure Lean.Lsp.LeanDeclIdent : Type

Name of a declaration in a given module.

• module : Name

  Name of the module that this identifier is in.

• decl : Name

  Name of the declaration.

instance Lean.Lsp.instFromJsonLeanDeclIdent : FromJson LeanDeclIdent

Equations

• Lean.Lsp.instFromJsonLeanDeclIdent = { fromJson? := Lean.Lsp.fromJsonLeanDeclIdent✝ }

instance Lean.Lsp.instToJsonLeanDeclIdent : ToJson LeanDeclIdent

Equations

• Lean.Lsp.instToJsonLeanDeclIdent = { toJson := Lean.Lsp.toJsonLeanDeclIdent✝ }

structure Lean.Lsp.LeanLocationLinkextends Lean.Lsp.LocationLink : Type

LocationLink with additional meta-data that allows the watchdog to resolve the range of this LocationLink. This is necessary because the position information from the .olean may be stale (e.g. if the user has edited the file that the definition is from, but neither saved or built it), while file workers sync their current reference information into the watchdog using ilean info notifications, which is up-to-date.

• originSelectionRange? : Option Range
• targetUri : DocumentUri
• targetRange : Range
• targetSelectionRange : Range
• ident? : Option LeanDeclIdent

  Identifier that caused this location link.

• isDefault : Bool

  Whether this location link was generated by a fallback handler. If the file worker can't produce any non-fallback location links, the watchdog tries again using its reference information from the ileans and ilean updates.

instance Lean.Lsp.instFromJsonLeanLocationLink : FromJson LeanLocationLink

Equations

• Lean.Lsp.instFromJsonLeanLocationLink = { fromJson? := Lean.Lsp.fromJsonLeanLocationLink✝ }

instance Lean.Lsp.instToJsonLeanLocationLink : ToJson LeanLocationLink

Equations

• Lean.Lsp.instToJsonLeanLocationLink = { toJson := Lean.Lsp.toJsonLeanLocationLink✝ }