feat: add call hierarchy support (#3082)
This PR adds support for the "call hierarchy" feature of LSP that allows quickly navigating both inbound and outbound call sites of functions. In this PR, "call" is taken to mean "usage", so inbound and outbound references of all kinds of identifiers (e.g. functions or types) can be navigated. To implement the call hierarchy feature, this PR implements the LSP requests `textDocument/prepareCallHierarchy`, `callHierarchy/incomingCalls` and `callHierarchy/outgoingCalls`. <details> <summary>Showing the call hierarchy (click to show image)</summary>  </details> <details> <summary>Incoming calls (click to show image)</summary>  </details> <details> <summary>Outgoing calls (click to show image)</summary>  </details> It is based on #3159, which should be merged before this PR. To route the parent declaration name through to the language server, the `.ilean` format is adjusted, breaking backwards compatibility with version 1 of the ILean format and yielding version 2. This PR also makes the following more minor adjustments: - `Lean.Server.findModuleRefs` now also combines the identifiers of constants and FVars and prefers constant over FVars for the combined identifier. This is necessary because e.g. declarations declared using `where` yield both a constant (for usage outside of the function) and an FVar (for usage inside of the function) with the same range, whereas we would typically like all references to refer to the former. This also fixes a bug introduced in #2462 where renaming a declaration declared using `where` would not rename usages outside of the function, as well as a bug in the unused variable linter where `where` declarations would be reported as unused even if they were being used outside of the function. - The function converting `Lean.Server.RefInfo` to `Lean.Lsp.RefInfo` now also computes the `Lean.DeclarationRanges` for parent declaration names via `MetaM` and must hence be in `IO` now. - Add a utility function `Array.groupByKey` to `HashMap.lean`. - Stylistic refactoring of `Watchdog.lean` and `LanguageFeatures.lean`.
This commit is contained in:
Marc Huisinga
GitHub
parent
6b0e7e1f46
commit
f9e5f1f1fd
14 changed files with 631 additions and 225 deletions
|
|
@ -192,7 +192,9 @@ example : x + foo 2 = 12 + x := by
|
|||
ought to be applied to multiple functions, the `decreasing_by` clause has to
|
||||
be repeated at each of these functions.
|
||||
|
||||
* Modify `InfoTree.context` to facilitate augmenting it with partial contexts while elaborating a command. This breaks backwards compatibility with all downstream projects that traverse the `InfoTree` manually instead of going through the functions in `InfoUtils.lean`, as well as those manually creating and saving `InfoTree`s. See https://github.com/leanprover/lean4/pull/3159 for how to migrate your code.
|
||||
* Modify `InfoTree.context` to facilitate augmenting it with partial contexts while elaborating a command. This breaks backwards compatibility with all downstream projects that traverse the `InfoTree` manually instead of going through the functions in `InfoUtils.lean`, as well as those manually creating and saving `InfoTree`s. See [PR #3159](https://github.com/leanprover/lean4/pull/3159) for how to migrate your code.
|
||||
|
||||
* Add language server support for [call hierarchy requests](https://devblogs.microsoft.com/cppblog/c-extension-in-vs-code-1-16-release-call-hierarchy-more/) ([PR #3082](https://github.com/leanprover/lean4/pull/3082)). The change to the .ilean format in this PR means that projects must be fully rebuilt once in order to generate .ilean files with the new format before features like "find references" work correctly again.
|
||||
|
||||
|
||||
v4.5.0
|
||||
|
|
|
|||
|
|
@ -227,3 +227,17 @@ def ofListWith (l : List (α × β)) (f : β → β → β) : HashMap α β :=
|
|||
match m.find? p.fst with
|
||||
| none => m.insert p.fst p.snd
|
||||
| some v => m.insert p.fst $ f v p.snd)
|
||||
end Lean.HashMap
|
||||
|
||||
/--
|
||||
Groups all elements `x`, `y` in `xs` with `key x == key y` into the same array
|
||||
`(xs.groupByKey key).find! (key x)`. Groups preserve the relative order of elements in `xs`.
|
||||
-/
|
||||
def Array.groupByKey [BEq α] [Hashable α] (key : β → α) (xs : Array β)
|
||||
: Lean.HashMap α (Array β) := Id.run do
|
||||
let mut groups := ∅
|
||||
for x in xs do
|
||||
let group := groups.findD (key x) #[]
|
||||
groups := groups.erase (key x) -- make `group` referentially unique
|
||||
groups := groups.insert (key x) (group.push x)
|
||||
return groups
|
||||
|
|
|
|||
|
|
@ -74,6 +74,7 @@ structure ServerCapabilities where
|
|||
declarationProvider : Bool := false
|
||||
typeDefinitionProvider : Bool := false
|
||||
referencesProvider : Bool := false
|
||||
callHierarchyProvider : Bool := false
|
||||
renameProvider? : Option RenameOptions := none
|
||||
workspaceSymbolProvider : Bool := false
|
||||
foldingRangeProvider : Bool := false
|
||||
|
|
|
|||
|
|
@ -8,6 +8,8 @@ Authors: Joscha Mennicken
|
|||
import Lean.Expr
|
||||
import Lean.Data.Lsp.Basic
|
||||
|
||||
set_option linter.missingDocs true -- keep it documented
|
||||
|
||||
/-! This file contains types for communication between the watchdog and the
|
||||
workers. These messages are not visible externally to users of the LSP server.
|
||||
-/
|
||||
|
|
@ -17,17 +19,27 @@ namespace Lean.Lsp
|
|||
/-! Most reference-related types have custom FromJson/ToJson implementations to
|
||||
reduce the size of the resulting JSON. -/
|
||||
|
||||
/--
|
||||
Identifier of a reference.
|
||||
-/
|
||||
inductive RefIdent where
|
||||
/-- Named identifier. These are used in all references that are globally available. -/
|
||||
| const : Name → RefIdent
|
||||
| fvar : FVarId → RefIdent
|
||||
/-- Unnamed identifier. These are used for all local references. -/
|
||||
| fvar : FVarId → RefIdent
|
||||
deriving BEq, Hashable, Inhabited
|
||||
|
||||
namespace RefIdent
|
||||
|
||||
/-- Converts the reference identifier to a string by prefixing it with a symbol. -/
|
||||
def toString : RefIdent → String
|
||||
| RefIdent.const n => s!"c:{n}"
|
||||
| RefIdent.fvar id => s!"f:{id.name}"
|
||||
|
||||
/--
|
||||
Converts the string representation of a reference identifier back to a reference identifier.
|
||||
The string representation must have been created by `RefIdent.toString`.
|
||||
-/
|
||||
def fromString (s : String) : Except String RefIdent := do
|
||||
let sPrefix := s.take 2
|
||||
let sName := s.drop 2
|
||||
|
|
@ -43,33 +55,92 @@ def fromString (s : String) : Except String RefIdent := do
|
|||
| "f:" => return RefIdent.fvar <| FVarId.mk name
|
||||
| _ => throw "string must start with 'c:' or 'f:'"
|
||||
|
||||
instance : FromJson RefIdent where
|
||||
fromJson?
|
||||
| (s : String) => fromString s
|
||||
| j => Except.error s!"expected a String, got {j}"
|
||||
|
||||
instance : ToJson RefIdent where
|
||||
toJson ident := toString ident
|
||||
|
||||
end RefIdent
|
||||
|
||||
/-- Information about the declaration surrounding a reference. -/
|
||||
structure RefInfo.ParentDecl where
|
||||
/-- Name of the declaration surrounding a reference. -/
|
||||
name : Name
|
||||
/-- Range of the declaration surrounding a reference. -/
|
||||
range : Lsp.Range
|
||||
/-- Selection range of the declaration surrounding a reference. -/
|
||||
selectionRange : Lsp.Range
|
||||
deriving ToJson
|
||||
|
||||
/--
|
||||
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.
|
||||
-/
|
||||
structure RefInfo.Location where
|
||||
/-- Range of the reference. -/
|
||||
range : Lsp.Range
|
||||
/-- Parent declaration of the reference. `none` if the reference is itself a declaration. -/
|
||||
parentDecl? : Option RefInfo.ParentDecl
|
||||
|
||||
/-- Definition site and usage sites of a reference. Obtained from `Lean.Server.RefInfo`. -/
|
||||
structure RefInfo where
|
||||
definition : Option Lsp.Range
|
||||
usages : Array Lsp.Range
|
||||
/-- Definition site of the reference. May be `none` when we cannot find a definition site. -/
|
||||
definition? : Option RefInfo.Location
|
||||
/-- Usage sites of the reference. -/
|
||||
usages : Array RefInfo.Location
|
||||
|
||||
instance : ToJson RefInfo where
|
||||
toJson i :=
|
||||
let rangeToList (r : Lsp.Range) : List Nat :=
|
||||
[r.start.line, r.start.character, r.end.line, r.end.character]
|
||||
let parentDeclToList (d : RefInfo.ParentDecl) : List Json :=
|
||||
let name := d.name.toString |> toJson
|
||||
let range := rangeToList d.range |>.map toJson
|
||||
let selectionRange := rangeToList d.selectionRange |>.map toJson
|
||||
[name] ++ range ++ selectionRange
|
||||
let locationToList (l : RefInfo.Location) : List Json :=
|
||||
let range := rangeToList l.range |>.map toJson
|
||||
let parentDecl := l.parentDecl?.map parentDeclToList |>.getD []
|
||||
range ++ parentDecl
|
||||
Json.mkObj [
|
||||
("definition", toJson $ i.definition.map rangeToList),
|
||||
("usages", toJson $ i.usages.map rangeToList)
|
||||
("definition", toJson $ i.definition?.map locationToList),
|
||||
("usages", toJson $ i.usages.map locationToList)
|
||||
]
|
||||
|
||||
instance : FromJson RefInfo where
|
||||
fromJson? j := do
|
||||
let listToRange (l : List Nat) : Except String Lsp.Range := match l with
|
||||
let toRange : List Nat → Except String Lsp.Range
|
||||
| [sLine, sChar, eLine, eChar] => pure ⟨⟨sLine, sChar⟩, ⟨eLine, eChar⟩⟩
|
||||
| _ => throw s!"Expected list of length 4, not {l.length}"
|
||||
let definition ← j.getObjValAs? (Option $ List Nat) "definition"
|
||||
let definition ← match definition with
|
||||
| l => throw s!"Expected list of length 4, not {l.length}"
|
||||
let toParentDecl (a : Array Json) : Except String RefInfo.ParentDecl := do
|
||||
let name := String.toName <| ← fromJson? a[0]!
|
||||
let range ← a[1:5].toArray.toList |>.mapM fromJson?
|
||||
let range ← toRange range
|
||||
let selectionRange ← a[5:].toArray.toList |>.mapM fromJson?
|
||||
let selectionRange ← toRange selectionRange
|
||||
return ⟨name, range, selectionRange⟩
|
||||
let toLocation (l : List Json) : Except String RefInfo.Location := do
|
||||
let l := l.toArray
|
||||
if l.size != 4 && l.size != 13 then
|
||||
.error "Expected list of length 4 or 13, not {l.size}"
|
||||
let range ← l[:4].toArray.toList |>.mapM fromJson?
|
||||
let range ← toRange range
|
||||
if l.size == 13 then
|
||||
let parentDecl ← toParentDecl l[4:].toArray
|
||||
return ⟨range, parentDecl⟩
|
||||
else
|
||||
return ⟨range, none⟩
|
||||
|
||||
let definition? ← j.getObjValAs? (Option $ List Json) "definition"
|
||||
let definition? ← match definition? with
|
||||
| none => pure none
|
||||
| some list => some <$> listToRange list
|
||||
let usages ← j.getObjValAs? (Array $ List Nat) "usages"
|
||||
let usages ← usages.mapM listToRange
|
||||
pure { definition, usages }
|
||||
| some list => some <$> toLocation list
|
||||
let usages ← j.getObjValAs? (Array $ List Json) "usages"
|
||||
let usages ← usages.mapM toLocation
|
||||
pure { definition?, usages }
|
||||
|
||||
/-- References from a single module/file -/
|
||||
def ModuleRefs := HashMap RefIdent RefInfo
|
||||
|
|
@ -88,7 +159,8 @@ instance : FromJson ModuleRefs where
|
|||
Contains the file's definitions and references. -/
|
||||
structure LeanIleanInfoParams where
|
||||
/-- Version of the file these references are from. -/
|
||||
version : Nat
|
||||
version : Nat
|
||||
/-- All references for the file. -/
|
||||
references : ModuleRefs
|
||||
deriving FromJson, ToJson
|
||||
|
||||
|
|
|
|||
|
|
@ -36,16 +36,16 @@ instance : FromJson CompletionItemKind where
|
|||
|
||||
structure InsertReplaceEdit where
|
||||
newText : String
|
||||
insert : Range
|
||||
insert : Range
|
||||
replace : Range
|
||||
deriving FromJson, ToJson
|
||||
|
||||
structure CompletionItem where
|
||||
label : String
|
||||
detail? : Option String := none
|
||||
label : String
|
||||
detail? : Option String := none
|
||||
documentation? : Option MarkupContent := none
|
||||
kind? : Option CompletionItemKind := none
|
||||
textEdit? : Option InsertReplaceEdit := none
|
||||
kind? : Option CompletionItemKind := none
|
||||
textEdit? : Option InsertReplaceEdit := none
|
||||
/-
|
||||
tags? : CompletionItemTag[]
|
||||
deprecated? : boolean
|
||||
|
|
@ -63,7 +63,7 @@ structure CompletionItem where
|
|||
|
||||
structure CompletionList where
|
||||
isIncomplete : Bool
|
||||
items : Array CompletionItem
|
||||
items : Array CompletionItem
|
||||
deriving FromJson, ToJson
|
||||
|
||||
structure CompletionParams extends TextDocumentPositionParams where
|
||||
|
|
@ -74,7 +74,7 @@ structure Hover where
|
|||
/- NOTE we should also accept MarkedString/MarkedString[] here
|
||||
but they are deprecated, so maybe can get away without. -/
|
||||
contents : MarkupContent
|
||||
range? : Option Range := none
|
||||
range? : Option Range := none
|
||||
deriving ToJson, FromJson
|
||||
|
||||
structure HoverParams extends TextDocumentPositionParams
|
||||
|
|
@ -153,45 +153,76 @@ inductive SymbolKind where
|
|||
| event
|
||||
| operator
|
||||
| typeParameter
|
||||
deriving BEq, Hashable, Inhabited
|
||||
|
||||
instance : FromJson SymbolKind where
|
||||
fromJson?
|
||||
| 1 => .ok .file
|
||||
| 2 => .ok .module
|
||||
| 3 => .ok .namespace
|
||||
| 4 => .ok .package
|
||||
| 5 => .ok .class
|
||||
| 6 => .ok .method
|
||||
| 7 => .ok .property
|
||||
| 8 => .ok .field
|
||||
| 9 => .ok .constructor
|
||||
| 10 => .ok .enum
|
||||
| 11 => .ok .interface
|
||||
| 12 => .ok .function
|
||||
| 13 => .ok .variable
|
||||
| 14 => .ok .constant
|
||||
| 15 => .ok .string
|
||||
| 16 => .ok .number
|
||||
| 17 => .ok .boolean
|
||||
| 18 => .ok .array
|
||||
| 19 => .ok .object
|
||||
| 20 => .ok .key
|
||||
| 21 => .ok .null
|
||||
| 22 => .ok .enumMember
|
||||
| 23 => .ok .struct
|
||||
| 24 => .ok .event
|
||||
| 25 => .ok .operator
|
||||
| 26 => .ok .typeParameter
|
||||
| j => .error s!"invalid symbol kind {j}"
|
||||
|
||||
instance : ToJson SymbolKind where
|
||||
toJson
|
||||
| SymbolKind.file => 1
|
||||
| SymbolKind.module => 2
|
||||
| SymbolKind.namespace => 3
|
||||
| SymbolKind.package => 4
|
||||
| SymbolKind.class => 5
|
||||
| SymbolKind.method => 6
|
||||
| SymbolKind.property => 7
|
||||
| SymbolKind.field => 8
|
||||
| SymbolKind.constructor => 9
|
||||
| SymbolKind.enum => 10
|
||||
| SymbolKind.interface => 11
|
||||
| SymbolKind.function => 12
|
||||
| SymbolKind.variable => 13
|
||||
| SymbolKind.constant => 14
|
||||
| SymbolKind.string => 15
|
||||
| SymbolKind.number => 16
|
||||
| SymbolKind.boolean => 17
|
||||
| SymbolKind.array => 18
|
||||
| SymbolKind.object => 19
|
||||
| SymbolKind.key => 20
|
||||
| SymbolKind.null => 21
|
||||
| SymbolKind.enumMember => 22
|
||||
| SymbolKind.struct => 23
|
||||
| SymbolKind.event => 24
|
||||
| SymbolKind.operator => 25
|
||||
| SymbolKind.typeParameter => 26
|
||||
toJson
|
||||
| .file => 1
|
||||
| .module => 2
|
||||
| .namespace => 3
|
||||
| .package => 4
|
||||
| .class => 5
|
||||
| .method => 6
|
||||
| .property => 7
|
||||
| .field => 8
|
||||
| .constructor => 9
|
||||
| .enum => 10
|
||||
| .interface => 11
|
||||
| .function => 12
|
||||
| .variable => 13
|
||||
| .constant => 14
|
||||
| .string => 15
|
||||
| .number => 16
|
||||
| .boolean => 17
|
||||
| .array => 18
|
||||
| .object => 19
|
||||
| .key => 20
|
||||
| .null => 21
|
||||
| .enumMember => 22
|
||||
| .struct => 23
|
||||
| .event => 24
|
||||
| .operator => 25
|
||||
| .typeParameter => 26
|
||||
|
||||
structure DocumentSymbolAux (Self : Type) where
|
||||
name : String
|
||||
detail? : Option String := none
|
||||
kind : SymbolKind
|
||||
name : String
|
||||
detail? : Option String := none
|
||||
kind : SymbolKind
|
||||
-- tags? : Array SymbolTag
|
||||
range : Range
|
||||
range : Range
|
||||
selectionRange : Range
|
||||
children? : Option (Array Self) := none
|
||||
deriving ToJson
|
||||
children? : Option (Array Self) := none
|
||||
deriving FromJson, ToJson
|
||||
|
||||
inductive DocumentSymbol where
|
||||
| mk (sym : DocumentSymbolAux DocumentSymbol)
|
||||
|
|
@ -212,18 +243,56 @@ instance : ToJson DocumentSymbolResult where
|
|||
|
||||
inductive SymbolTag where
|
||||
| deprecated
|
||||
deriving BEq, Hashable, Inhabited
|
||||
|
||||
instance : FromJson SymbolTag where
|
||||
fromJson?
|
||||
| 1 => .ok .deprecated
|
||||
| j => .error s!"unknown symbol tag {j}"
|
||||
|
||||
instance : ToJson SymbolTag where
|
||||
toJson
|
||||
| SymbolTag.deprecated => 1
|
||||
toJson
|
||||
| .deprecated => 1
|
||||
|
||||
structure SymbolInformation where
|
||||
name : String
|
||||
kind : SymbolKind
|
||||
tags : Array SymbolTag := #[]
|
||||
location : Location
|
||||
name : String
|
||||
kind : SymbolKind
|
||||
tags : Array SymbolTag := #[]
|
||||
location : Location
|
||||
containerName? : Option String := none
|
||||
deriving ToJson
|
||||
deriving FromJson, ToJson
|
||||
|
||||
structure CallHierarchyPrepareParams extends TextDocumentPositionParams
|
||||
deriving FromJson, ToJson
|
||||
|
||||
structure CallHierarchyItem where
|
||||
name : String
|
||||
kind : SymbolKind
|
||||
tags? : Option (Array SymbolTag) := none
|
||||
detail? : Option String := none
|
||||
uri : DocumentUri
|
||||
range : Range
|
||||
selectionRange : Range
|
||||
-- data? : Option unknown
|
||||
deriving FromJson, ToJson, BEq, Hashable, Inhabited
|
||||
|
||||
structure CallHierarchyIncomingCallsParams where
|
||||
item : CallHierarchyItem
|
||||
deriving FromJson, ToJson
|
||||
|
||||
structure CallHierarchyIncomingCall where
|
||||
«from» : CallHierarchyItem
|
||||
fromRanges : Array Range
|
||||
deriving FromJson, ToJson, Inhabited
|
||||
|
||||
structure CallHierarchyOutgoingCallsParams where
|
||||
item : CallHierarchyItem
|
||||
deriving FromJson, ToJson
|
||||
|
||||
structure CallHierarchyOutgoingCall where
|
||||
to : CallHierarchyItem
|
||||
fromRanges : Array Range
|
||||
deriving FromJson, ToJson, Inhabited
|
||||
|
||||
inductive SemanticTokenType where
|
||||
-- Used by Lean
|
||||
|
|
@ -304,14 +373,14 @@ example {v : SemanticTokenModifier} : open SemanticTokenModifier in
|
|||
cases v <;> native_decide
|
||||
|
||||
structure SemanticTokensLegend where
|
||||
tokenTypes : Array String
|
||||
tokenTypes : Array String
|
||||
tokenModifiers : Array String
|
||||
deriving FromJson, ToJson
|
||||
|
||||
structure SemanticTokensOptions where
|
||||
legend : SemanticTokensLegend
|
||||
range : Bool
|
||||
full : Bool /- | {
|
||||
range : Bool
|
||||
full : Bool /- | {
|
||||
delta?: boolean;
|
||||
} -/
|
||||
deriving FromJson, ToJson
|
||||
|
|
@ -322,12 +391,12 @@ structure SemanticTokensParams where
|
|||
|
||||
structure SemanticTokensRangeParams where
|
||||
textDocument : TextDocumentIdentifier
|
||||
range : Range
|
||||
range : Range
|
||||
deriving FromJson, ToJson
|
||||
|
||||
structure SemanticTokens where
|
||||
resultId? : Option String := none
|
||||
data : Array Nat
|
||||
data : Array Nat
|
||||
deriving FromJson, ToJson
|
||||
|
||||
structure FoldingRangeParams where
|
||||
|
|
@ -343,12 +412,12 @@ instance : ToJson FoldingRangeKind where
|
|||
toJson
|
||||
| FoldingRangeKind.comment => "comment"
|
||||
| FoldingRangeKind.imports => "imports"
|
||||
| FoldingRangeKind.region => "region"
|
||||
| FoldingRangeKind.region => "region"
|
||||
|
||||
structure FoldingRange where
|
||||
startLine : Nat
|
||||
endLine : Nat
|
||||
kind? : Option FoldingRangeKind := none
|
||||
endLine : Nat
|
||||
kind? : Option FoldingRangeKind := none
|
||||
deriving ToJson
|
||||
|
||||
structure RenameOptions where
|
||||
|
|
|
|||
|
|
@ -8,6 +8,7 @@ import Init.Data.String
|
|||
import Init.Data.Array
|
||||
import Lean.Data.Lsp.Basic
|
||||
import Lean.Data.Position
|
||||
import Lean.DeclarationRange
|
||||
|
||||
/-! LSP uses UTF-16 for indexing, so we need to provide some primitives
|
||||
to interact with Lean strings using UTF-16 indices. -/
|
||||
|
|
@ -86,3 +87,13 @@ def utf8PosToLspPos (text : FileMap) (pos : String.Pos) : Lsp.Position :=
|
|||
|
||||
end FileMap
|
||||
end Lean
|
||||
|
||||
/--
|
||||
Convert the Lean `DeclarationRange` to an LSP `Range` by turning the 1-indexed line numbering into a
|
||||
0-indexed line numbering and converting the character offset within the line to a UTF-16 indexed
|
||||
offset.
|
||||
-/
|
||||
def Lean.DeclarationRange.toLspRange (r : Lean.DeclarationRange) : Lsp.Range := {
|
||||
start := ⟨r.pos.line - 1, r.charUtf16⟩
|
||||
«end» := ⟨r.endPos.line - 1, r.endCharUtf16⟩
|
||||
}
|
||||
|
|
|
|||
|
|
@ -118,7 +118,7 @@ def runFrontend
|
|||
if let some ileanFileName := ileanFileName? then
|
||||
let trees := s.commandState.infoState.trees.toArray
|
||||
let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false)
|
||||
let ilean := { module := mainModuleName, references : Lean.Server.Ilean }
|
||||
let ilean := { module := mainModuleName, references := ← references.toLspModuleRefs : Lean.Server.Ilean }
|
||||
IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean
|
||||
|
||||
pure (s.commandState.env, !s.commandState.messages.hasErrors)
|
||||
|
|
|
|||
|
|
@ -76,7 +76,7 @@ section Elab
|
|||
private def publishIleanInfo (method : String) (m : DocumentMeta) (hOut : FS.Stream)
|
||||
(snaps : Array Snapshot) : IO Unit := do
|
||||
let trees := snaps.map fun snap => snap.infoTree
|
||||
let references := findModuleRefs m.text trees (localVars := true)
|
||||
let references ← findModuleRefs m.text trees (localVars := true) |>.toLspModuleRefs
|
||||
let param := { version := m.version, references : LeanIleanInfoParams }
|
||||
hOut.writeLspNotification { method, param }
|
||||
|
||||
|
|
|
|||
|
|
@ -290,23 +290,23 @@ partial def handleDocumentHighlight (p : DocumentHighlightParams)
|
|||
| `(do%$i $elems) => highlightReturn? (i.getRange?.get!.toLspRange text) elems
|
||||
| stx => stx.getArgs.findSome? (highlightReturn? doRange?)
|
||||
|
||||
let highlightRefs? (snaps : Array Snapshot) : Option (Array DocumentHighlight) := Id.run do
|
||||
let highlightRefs? (snaps : Array Snapshot) : IO (Option (Array DocumentHighlight)) := do
|
||||
let trees := snaps.map (·.infoTree)
|
||||
let refs : Lsp.ModuleRefs := findModuleRefs text trees
|
||||
let refs : Lsp.ModuleRefs ← findModuleRefs text trees |>.toLspModuleRefs
|
||||
let mut ranges := #[]
|
||||
for ident in ← refs.findAt p.position do
|
||||
if let some info ← refs.find? ident then
|
||||
if let some definition := info.definition then
|
||||
ranges := ranges.push definition
|
||||
ranges := ranges.append info.usages
|
||||
for ident in refs.findAt p.position do
|
||||
if let some info := refs.find? ident then
|
||||
if let some ⟨definitionRange, _⟩ := info.definition? then
|
||||
ranges := ranges.push definitionRange
|
||||
ranges := ranges.append <| info.usages.map (·.range)
|
||||
if ranges.isEmpty then
|
||||
return none
|
||||
some <| ranges.map ({ range := ·, kind? := DocumentHighlightKind.text })
|
||||
return some <| ranges.map ({ range := ·, kind? := DocumentHighlightKind.text })
|
||||
|
||||
withWaitFindSnap doc (fun s => s.endPos > pos)
|
||||
(notFoundX := pure #[]) fun snap => do
|
||||
let (snaps, _) ← doc.cmdSnaps.getFinishedPrefix
|
||||
if let some his := highlightRefs? snaps.toArray then
|
||||
if let some his ← highlightRefs? snaps.toArray then
|
||||
return his
|
||||
if let some hi := highlightReturn? none snap.stx then
|
||||
return #[hi]
|
||||
|
|
|
|||
|
|
@ -34,14 +34,11 @@ def locationLinksFromDecl (srcSearchPath : SearchPath) (uri : DocumentUri) (n :
|
|||
|
||||
let ranges? ← findDeclarationRanges? n
|
||||
if let (some ranges, some modUri) := (ranges?, modUri?) then
|
||||
let declRangeToLspRange (r : DeclarationRange) : Lsp.Range :=
|
||||
{ start := ⟨r.pos.line - 1, r.charUtf16⟩
|
||||
«end» := ⟨r.endPos.line - 1, r.endCharUtf16⟩ }
|
||||
let ll : LocationLink := {
|
||||
originSelectionRange? := originRange?
|
||||
targetUri := modUri
|
||||
targetRange := declRangeToLspRange ranges.range
|
||||
targetSelectionRange := declRangeToLspRange ranges.selectionRange
|
||||
targetRange := ranges.range.toLspRange
|
||||
targetSelectionRange := ranges.selectionRange.toLspRange
|
||||
}
|
||||
return #[ll]
|
||||
return #[]
|
||||
|
|
|
|||
|
|
@ -13,18 +13,18 @@ namespace Lean.Server
|
|||
open Lsp Lean.Elab Std
|
||||
|
||||
structure Reference where
|
||||
ident : RefIdent
|
||||
ident : RefIdent
|
||||
/-- FVarIds that are logically identical to this reference -/
|
||||
aliases : Array RefIdent := #[]
|
||||
range : Lsp.Range
|
||||
stx : Syntax
|
||||
ci : ContextInfo
|
||||
info : Info
|
||||
aliases : Array RefIdent := #[]
|
||||
range : Lsp.Range
|
||||
stx : Syntax
|
||||
ci : ContextInfo
|
||||
info : Info
|
||||
isBinder : Bool
|
||||
|
||||
structure RefInfo where
|
||||
definition : Option Reference
|
||||
usages : Array Reference
|
||||
usages : Array Reference
|
||||
|
||||
namespace RefInfo
|
||||
|
||||
|
|
@ -37,11 +37,26 @@ def addRef : RefInfo → Reference → RefInfo
|
|||
{ i with usages := usages.push ref }
|
||||
| i, _ => i
|
||||
|
||||
instance : Coe RefInfo Lsp.RefInfo where
|
||||
coe self :=
|
||||
{
|
||||
definition := self.definition.map (·.range)
|
||||
usages := self.usages.map (·.range)
|
||||
def toLspRefInfo (i : RefInfo) : IO Lsp.RefInfo := do
|
||||
let refToRefInfoLocation (ref : Reference) : IO RefInfo.Location := do
|
||||
let parentDeclName? := ref.ci.parentDecl?
|
||||
let parentDeclRanges? ← ref.ci.runMetaM ref.info.lctx do
|
||||
let some parentDeclName := parentDeclName?
|
||||
| return none
|
||||
findDeclarationRanges? parentDeclName
|
||||
return {
|
||||
range := ref.range
|
||||
parentDecl? := do
|
||||
let parentDeclName ← parentDeclName?
|
||||
let parentDeclRange := (← parentDeclRanges?).range.toLspRange
|
||||
let parentDeclSelectionRange := (← parentDeclRanges?).selectionRange.toLspRange
|
||||
return ⟨parentDeclName, parentDeclRange, parentDeclSelectionRange⟩
|
||||
}
|
||||
let definition? ← i.definition.mapM refToRefInfoLocation
|
||||
let usages ← i.usages.mapM refToRefInfoLocation
|
||||
return {
|
||||
definition? := definition?
|
||||
usages := usages
|
||||
}
|
||||
|
||||
end RefInfo
|
||||
|
|
@ -54,8 +69,10 @@ def addRef (self : ModuleRefs) (ref : Reference) : ModuleRefs :=
|
|||
let refInfo := self.findD ref.ident RefInfo.empty
|
||||
self.insert ref.ident (refInfo.addRef ref)
|
||||
|
||||
instance : Coe ModuleRefs Lsp.ModuleRefs where
|
||||
coe self := HashMap.ofList <| List.map (fun (k, v) => (k, v)) <| self.toList
|
||||
def toLspModuleRefs (refs : ModuleRefs) : IO Lsp.ModuleRefs := do
|
||||
let refs ← refs.toList.mapM fun (k, v) => do
|
||||
return (k, ← v.toLspRefInfo)
|
||||
return HashMap.ofList refs
|
||||
|
||||
end ModuleRefs
|
||||
|
||||
|
|
@ -68,15 +85,15 @@ def empty : RefInfo := ⟨ none, #[] ⟩
|
|||
|
||||
def merge (a : RefInfo) (b : RefInfo) : RefInfo :=
|
||||
{
|
||||
definition := b.definition.orElse fun _ => a.definition
|
||||
definition? := b.definition?.orElse fun _ => a.definition?
|
||||
usages := a.usages.append b.usages
|
||||
}
|
||||
|
||||
def findRange? (self : RefInfo) (pos : Lsp.Position) (includeStop := false) : Option Range := do
|
||||
if let some range := self.definition then
|
||||
if let some ⟨range, _⟩ := self.definition? then
|
||||
if contains range pos then
|
||||
return range
|
||||
for range in self.usages do
|
||||
for ⟨range, _⟩ in self.usages do
|
||||
if contains range pos then
|
||||
return range
|
||||
none
|
||||
|
|
@ -117,8 +134,8 @@ open Elab
|
|||
|
||||
/-- Content of individual `.ilean` files -/
|
||||
structure Ilean where
|
||||
version : Nat := 1
|
||||
module : Name
|
||||
version : Nat := 2
|
||||
module : Name
|
||||
references : Lsp.ModuleRefs
|
||||
deriving FromJson, ToJson
|
||||
|
||||
|
|
@ -152,64 +169,98 @@ def findReferences (text : FileMap) (trees : Array InfoTree) : Array Reference :
|
|||
get
|
||||
|
||||
/--
|
||||
The `FVarId`s of a function parameter in the function's signature and body
|
||||
differ. However, they have `TermInfo` nodes with `binder := true` in the exact
|
||||
same position. Moreover, macros such as do-reassignment `x := e` may create
|
||||
chains of variable definitions where a helper definition overlaps with a use
|
||||
of a variable.
|
||||
There are several different identifiers that should be considered equal for the purpose of finding
|
||||
all references of an identifier:
|
||||
- `FVarId`s of a function parameter in the function's signature and body
|
||||
- Chains of helper definitions like those created for do-reassignment `x := e`
|
||||
- Overlapping definitions like those defined by `where` declarations that define both an FVar
|
||||
(for local usage) and a constant (for non-local usage)
|
||||
- Identifiers connected by `FVarAliasInfo` such as variables before and after `match` generalization
|
||||
|
||||
This function changes every such group to use a single `FVarId` (the head of the
|
||||
chain/DAG) and gets rid of duplicate definitions.
|
||||
In the first three cases that are not explicitly denoted as aliases with an `FVarAliasInfo`, the
|
||||
corresponding `Reference`s have the exact same range.
|
||||
This function finds all definitions that have the exact same range as another definition or usage
|
||||
and collapses them into a single identifier. It also collapses identifiers connected by
|
||||
an `FVarAliasInfo`.
|
||||
When collapsing identifiers, it prefers using a `RefIdent.const name` over a `RefIdent.fvar id` for
|
||||
all identifiers that are being collapsed into one.
|
||||
-/
|
||||
partial def combineFvars (trees : Array InfoTree) (refs : Array Reference) : Array Reference := Id.run do
|
||||
partial def combineIdents (trees : Array InfoTree) (refs : Array Reference) : Array Reference := Id.run do
|
||||
-- Deduplicate definitions based on their exact range
|
||||
let mut posMap : HashMap Lsp.Range FVarId := HashMap.empty
|
||||
let mut posMap : HashMap Lsp.Range RefIdent := HashMap.empty
|
||||
for ref in refs do
|
||||
if let { ident := RefIdent.fvar id, range, isBinder := true, .. } := ref then
|
||||
posMap := posMap.insert range id
|
||||
if let { ident, range, isBinder := true, .. } := ref then
|
||||
posMap := posMap.insert range ident
|
||||
|
||||
let idMap := buildIdMap posMap
|
||||
let idMap := useConstRepresentatives <| buildIdMap posMap
|
||||
|
||||
let mut refs' := #[]
|
||||
for ref in refs do
|
||||
match ref with
|
||||
| { ident := ident@(RefIdent.fvar id), .. } =>
|
||||
if idMap.contains id then
|
||||
refs' := refs'.push { ref with ident := applyIdMap idMap ident, aliases := #[ident] }
|
||||
else if !idMap.contains id then
|
||||
refs' := refs'.push ref
|
||||
| _ =>
|
||||
let id := ref.ident
|
||||
if idMap.contains id then
|
||||
refs' := refs'.push { ref with ident := findCanonicalRepresentative idMap id, aliases := #[id] }
|
||||
else if !idMap.contains id then
|
||||
refs' := refs'.push ref
|
||||
refs'
|
||||
where
|
||||
findCanonicalBinder (idMap : HashMap FVarId FVarId) (id : FVarId) : FVarId :=
|
||||
match idMap.find? id with
|
||||
| some id' => findCanonicalBinder idMap id' -- recursion depth is expected to be very low
|
||||
| none => id
|
||||
useConstRepresentatives (idMap : HashMap RefIdent RefIdent)
|
||||
: HashMap RefIdent RefIdent := Id.run do
|
||||
let insertIntoClass classesById id :=
|
||||
let representative := findCanonicalRepresentative idMap id
|
||||
let «class» := classesById.findD representative ∅
|
||||
let classesById := classesById.erase representative -- make `«class»` referentially unique
|
||||
let «class» := «class».insert id
|
||||
classesById.insert representative «class»
|
||||
|
||||
applyIdMap : HashMap FVarId FVarId → RefIdent → RefIdent
|
||||
| m, RefIdent.fvar id => RefIdent.fvar <| findCanonicalBinder m id
|
||||
| _, ident => ident
|
||||
-- collect equivalence classes
|
||||
let mut classesById : HashMap RefIdent (HashSet RefIdent) := ∅
|
||||
for ⟨id, baseId⟩ in idMap.toArray do
|
||||
classesById := insertIntoClass classesById id
|
||||
classesById := insertIntoClass classesById baseId
|
||||
|
||||
let mut r := ∅
|
||||
for ⟨currentRepresentative, «class»⟩ in classesById.toArray do
|
||||
-- find best representative (ideally a const if available)
|
||||
let mut bestRepresentative := currentRepresentative
|
||||
for id in «class» do
|
||||
bestRepresentative :=
|
||||
match bestRepresentative, id with
|
||||
| .fvar a, .fvar _ => .fvar a
|
||||
| .fvar _, .const b => .const b
|
||||
| .const a, .fvar _ => .const a
|
||||
| .const a, .const _ => .const a
|
||||
|
||||
-- compress `idMap` so that all identifiers in a class point to the best representative
|
||||
for id in «class» do
|
||||
if id != bestRepresentative then
|
||||
r := r.insert id bestRepresentative
|
||||
return r
|
||||
|
||||
findCanonicalRepresentative (idMap : HashMap RefIdent RefIdent) (id : RefIdent) : RefIdent := Id.run do
|
||||
let mut canonicalRepresentative := id
|
||||
while idMap.contains canonicalRepresentative do
|
||||
canonicalRepresentative := idMap.find! canonicalRepresentative
|
||||
return canonicalRepresentative
|
||||
|
||||
buildIdMap posMap := Id.run <| StateT.run' (s := HashMap.empty) do
|
||||
-- map fvar defs to overlapping fvar defs/uses
|
||||
for ref in refs do
|
||||
if let { ident := RefIdent.fvar baseId, range, .. } := ref then
|
||||
if let some id := posMap.find? range then
|
||||
insertIdMap id baseId
|
||||
let baseId := ref.ident
|
||||
if let some id := posMap.find? ref.range then
|
||||
insertIdMap id baseId
|
||||
|
||||
-- apply `FVarAliasInfo`
|
||||
trees.forM (·.visitM' (postNode := fun _ info _ => do
|
||||
if let .ofFVarAliasInfo ai := info then
|
||||
insertIdMap ai.id ai.baseId))
|
||||
insertIdMap (.fvar ai.id) (.fvar ai.baseId)))
|
||||
|
||||
get
|
||||
|
||||
-- NOTE: poor man's union-find; see also `findCanonicalBinder`
|
||||
-- poor man's union-find; see also `findCanonicalBinder`
|
||||
insertIdMap id baseId := do
|
||||
let idMap ← get
|
||||
let id := findCanonicalBinder idMap id
|
||||
let baseId := findCanonicalBinder idMap baseId
|
||||
let id := findCanonicalRepresentative idMap id
|
||||
let baseId := findCanonicalRepresentative idMap baseId
|
||||
if baseId != id then
|
||||
modify (·.insert id baseId)
|
||||
|
||||
|
|
@ -229,7 +280,7 @@ def findModuleRefs (text : FileMap) (trees : Array InfoTree) (localVars : Bool :
|
|||
(allowSimultaneousBinderUse := false) : ModuleRefs := Id.run do
|
||||
let mut refs :=
|
||||
dedupReferences (allowSimultaneousBinderUse := allowSimultaneousBinderUse) <|
|
||||
combineFvars trees <|
|
||||
combineIdents trees <|
|
||||
findReferences text trees
|
||||
if !localVars then
|
||||
refs := refs.filter fun
|
||||
|
|
@ -291,8 +342,12 @@ def findRange? (self : References) (module : Name) (pos : Lsp.Position) (include
|
|||
let refs ← self.allRefs.find? module
|
||||
refs.findRange? pos includeStop
|
||||
|
||||
structure DocumentRefInfo where
|
||||
location : Location
|
||||
parentInfo? : Option RefInfo.ParentDecl
|
||||
|
||||
def referringTo (self : References) (identModule : Name) (ident : RefIdent) (srcSearchPath : SearchPath)
|
||||
(includeDefinition : Bool := true) : IO (Array Location) := do
|
||||
(includeDefinition : Bool := true) : IO (Array DocumentRefInfo) := do
|
||||
let refsToCheck := match ident with
|
||||
| RefIdent.const _ => self.allRefs.toList
|
||||
| RefIdent.fvar _ => match self.allRefs.find? identModule with
|
||||
|
|
@ -306,22 +361,22 @@ def referringTo (self : References) (identModule : Name) (ident : RefIdent) (src
|
|||
-- opened in the right folder
|
||||
let uri := System.Uri.pathToUri <| ← IO.FS.realPath path
|
||||
if includeDefinition then
|
||||
if let some range := info.definition then
|
||||
result := result.push ⟨uri, range⟩
|
||||
for range in info.usages do
|
||||
result := result.push ⟨uri, range⟩
|
||||
if let some ⟨range, parentDeclInfo?⟩ := info.definition? then
|
||||
result := result.push ⟨⟨uri, range⟩, parentDeclInfo?⟩
|
||||
for ⟨range, parentDeclInfo?⟩ in info.usages do
|
||||
result := result.push ⟨⟨uri, range⟩, parentDeclInfo?⟩
|
||||
return result
|
||||
|
||||
def definitionOf? (self : References) (ident : RefIdent) (srcSearchPath : SearchPath)
|
||||
: IO (Option Location) := do
|
||||
: IO (Option DocumentRefInfo) := do
|
||||
for (module, refs) in self.allRefs.toList do
|
||||
if let some info := refs.find? ident then
|
||||
if let some definition := info.definition then
|
||||
if let some ⟨definitionRange, definitionParentDeclInfo?⟩ := info.definition? then
|
||||
if let some path ← srcSearchPath.findModuleWithExt "lean" module then
|
||||
-- Resolve symlinks (such as `src` in the build dir) so that files are
|
||||
-- opened in the right folder
|
||||
let uri := System.Uri.pathToUri <| ← IO.FS.realPath path
|
||||
return some ⟨uri, definition⟩
|
||||
return some ⟨⟨uri, definitionRange⟩, definitionParentDeclInfo?⟩
|
||||
return none
|
||||
|
||||
def definitionsMatching (self : References) (srcSearchPath : SearchPath) (filter : Name → Option α)
|
||||
|
|
@ -331,9 +386,9 @@ def definitionsMatching (self : References) (srcSearchPath : SearchPath) (filter
|
|||
if let some path ← srcSearchPath.findModuleWithExt "lean" module then
|
||||
let uri := System.Uri.pathToUri <| ← IO.FS.realPath path
|
||||
for (ident, info) in refs.toList do
|
||||
if let (RefIdent.const name, some definition) := (ident, info.definition) then
|
||||
if let (RefIdent.const name, some ⟨definitionRange, _⟩) := (ident, info.definition?) then
|
||||
if let some a := filter name then
|
||||
result := result.push (a, ⟨uri, definition⟩)
|
||||
result := result.push (a, ⟨uri, definitionRange⟩)
|
||||
if let some maxAmount := maxAmount? then
|
||||
if result.size >= maxAmount then
|
||||
return result
|
||||
|
|
|
|||
|
|
@ -22,42 +22,49 @@ For general server architecture, see `README.md`. This module implements the wat
|
|||
|
||||
## Watchdog state
|
||||
|
||||
Most LSP clients only send us file diffs, so to facilitate sending entire file contents to freshly restarted
|
||||
workers, the watchdog needs to maintain the current state of each file. It can also use this state to detect changes
|
||||
to the header and thus restart the corresponding worker, freeing its imports.
|
||||
Most LSP clients only send us file diffs, so to facilitate sending entire file contents to freshly
|
||||
restarted workers, the watchdog needs to maintain the current state of each file. It can also use
|
||||
this state to detect changes to the header and thus restart the corresponding worker, freeing its
|
||||
imports.
|
||||
|
||||
TODO(WN):
|
||||
We may eventually want to keep track of approximately (since this isn't knowable exactly) where in the file a worker
|
||||
crashed. Then on restart, we tell said worker to only parse up to that point and query the user about how to proceed
|
||||
(continue OR allow the user to fix the bug and then continue OR ..). Without this, if the crash is deterministic,
|
||||
users may be confused about why the server seemingly stopped working for a single file.
|
||||
We may eventually want to keep track of approximately (since this isn't knowable exactly) where in
|
||||
the file a worker crashed. Then on restart, we tell said worker to only parse up to that point and
|
||||
query the user about how to proceed (continue OR allow the user to fix the bug and then continue OR
|
||||
..). Without this, if the crash is deterministic, users may be confused about why the server
|
||||
seemingly stopped working for a single file.
|
||||
|
||||
## Watchdog <-> worker communication
|
||||
|
||||
The watchdog process and its file worker processes communicate via LSP. If the necessity arises,
|
||||
we might add non-standard commands similarly based on JSON-RPC. Most requests and notifications
|
||||
are forwarded to the corresponding file worker process, with the exception of these notifications:
|
||||
The watchdog process and its file worker processes communicate via LSP. If the necessity arises, we
|
||||
might add non-standard commands similarly based on JSON-RPC. Most requests and notifications are
|
||||
forwarded to the corresponding file worker process, with the exception of these notifications:
|
||||
|
||||
- textDocument/didOpen: Launch the file worker, create the associated watchdog state and launch a task to
|
||||
asynchronously receive LSP packets from the worker (e.g. request responses).
|
||||
- textDocument/didOpen: Launch the file worker, create the associated watchdog state and launch a
|
||||
task to asynchronously receive LSP packets from the worker (e.g. request
|
||||
responses).
|
||||
- textDocument/didChange: Update the local file state so that it can be resent to restarted workers.
|
||||
Then forward the `didChange` notification.
|
||||
- textDocument/didClose: Signal a shutdown to the file worker and remove the associated watchdog state.
|
||||
- textDocument/didClose: Signal a shutdown to the file worker and remove the associated watchdog
|
||||
state.
|
||||
|
||||
Moreover, we don't implement the full protocol at this level:
|
||||
|
||||
- Upon starting, the `initialize` request is forwarded to the worker, but it must not respond with its server
|
||||
capabilities. Consequently, the watchdog will not send an `initialized` notification to the worker.
|
||||
- After `initialize`, the watchdog sends the corresponding `didOpen` notification with the full current state of
|
||||
the file. No additional `didOpen` notifications will be forwarded to the worker process.
|
||||
- Upon starting, the `initialize` request is forwarded to the worker, but it must not respond with
|
||||
its server capabilities. Consequently, the watchdog will not send an `initialized` notification to
|
||||
the worker.
|
||||
- After `initialize`, the watchdog sends the corresponding `didOpen` notification with the full
|
||||
current state of the file. No additional `didOpen` notifications will be forwarded to the worker
|
||||
process.
|
||||
- `$/cancelRequest` notifications are forwarded to all file workers.
|
||||
- File workers are always terminated with an `exit` notification, without previously receiving a `shutdown` request.
|
||||
Similarly, they never receive a `didClose` notification.
|
||||
- File workers are always terminated with an `exit` notification, without previously receiving a
|
||||
`shutdown` request. Similarly, they never receive a `didClose` notification.
|
||||
|
||||
## Watchdog <-> client communication
|
||||
|
||||
The watchdog itself should implement the LSP standard as closely as possible. However we reserve the right to add
|
||||
non-standard extensions in case they're needed, for example to communicate tactic state.
|
||||
The watchdog itself should implement the LSP standard as closely as possible. However we reserve the
|
||||
right to add non-standard extensions in case they're needed, for example to communicate tactic
|
||||
state.
|
||||
-/
|
||||
|
||||
namespace Lean.Server.Watchdog
|
||||
|
|
@ -83,13 +90,13 @@ section Utils
|
|||
| ioError (e : IO.Error)
|
||||
|
||||
inductive WorkerState where
|
||||
/-- The watchdog can detect a crashed file worker in two places: When trying to send a message to the file worker
|
||||
and when reading a request reply.
|
||||
In the latter case, the forwarding task terminates and delegates a `crashed` event to the main task.
|
||||
Then, in both cases, the file worker has its state set to `crashed` and requests that are in-flight are errored.
|
||||
Upon receiving the next packet for that file worker, the file worker is restarted and the packet is forwarded
|
||||
to it. If the crash was detected while writing a packet, we queue that packet until the next packet for the file
|
||||
worker arrives. -/
|
||||
/-- The watchdog can detect a crashed file worker in two places: When trying to send a message
|
||||
to the file worker and when reading a request reply.
|
||||
In the latter case, the forwarding task terminates and delegates a `crashed` event to the
|
||||
main task. Then, in both cases, the file worker has its state set to `crashed` and requests
|
||||
that are in-flight are errored. Upon receiving the next packet for that file worker, the file
|
||||
worker is restarted and the packet is forwarded to it. If the crash was detected while writing
|
||||
a packet, we queue that packet until the next packet for the file worker arrives. -/
|
||||
| crashed (queuedMsgs : Array JsonRpc.Message)
|
||||
| running
|
||||
|
||||
|
|
@ -102,11 +109,12 @@ section FileWorker
|
|||
proc : Process.Child workerCfg
|
||||
commTask : Task WorkerEvent
|
||||
state : WorkerState
|
||||
-- This should not be mutated outside of namespace FileWorker, as it is used as shared mutable state
|
||||
/-- The pending requests map contains all requests
|
||||
that have been received from the LSP client, but were not answered yet.
|
||||
We need them for forwarding cancellation requests to the correct worker as well as cleanly aborting
|
||||
requests on worker crashes. -/
|
||||
-- This should not be mutated outside of namespace FileWorker,
|
||||
-- as it is used as shared mutable state
|
||||
/-- The pending requests map contains all requests that have been received from the LSP client,
|
||||
but were not answered yet.
|
||||
We need them for forwarding cancellation requests to the correct worker as well as cleanly
|
||||
aborting requests on worker crashes. -/
|
||||
pendingRequestsRef : IO.Ref PendingRequestMap
|
||||
|
||||
namespace FileWorker
|
||||
|
|
@ -120,8 +128,10 @@ section FileWorker
|
|||
def erasePendingRequest (fw : FileWorker) (id : RequestID) : IO Unit :=
|
||||
fw.pendingRequestsRef.modify fun pendingRequests => pendingRequests.erase id
|
||||
|
||||
def errorPendingRequests (fw : FileWorker) (hError : FS.Stream) (code : ErrorCode) (msg : String) : IO Unit := do
|
||||
let pendingRequests ← fw.pendingRequestsRef.modifyGet (fun pendingRequests => (pendingRequests, RBMap.empty))
|
||||
def errorPendingRequests (fw : FileWorker) (hError : FS.Stream) (code : ErrorCode) (msg : String)
|
||||
: IO Unit := do
|
||||
let pendingRequests ← fw.pendingRequestsRef.modifyGet
|
||||
fun pendingRequests => (pendingRequests, RBMap.empty)
|
||||
for ⟨id, _⟩ in pendingRequests do
|
||||
hError.writeLspResponseError { id := id, code := code, message := msg }
|
||||
|
||||
|
|
@ -173,13 +183,15 @@ section ServerM
|
|||
let s ← read
|
||||
if let some path := fileUriToPath? fw.doc.uri then
|
||||
if let some module ← searchModuleNameOfFileName path s.srcSearchPath then
|
||||
s.references.modify fun refs => refs.updateWorkerRefs module params.version params.references
|
||||
s.references.modify fun refs =>
|
||||
refs.updateWorkerRefs module params.version params.references
|
||||
|
||||
def handleIleanInfoFinal (fw : FileWorker) (params : LeanIleanInfoParams) : ServerM Unit := do
|
||||
let s ← read
|
||||
if let some path := fileUriToPath? fw.doc.uri then
|
||||
if let some module ← searchModuleNameOfFileName path s.srcSearchPath then
|
||||
s.references.modify fun refs => refs.finalizeWorkerRefs module params.version params.references
|
||||
s.references.modify fun refs =>
|
||||
refs.finalizeWorkerRefs module params.version params.references
|
||||
|
||||
/-- Creates a Task which forwards a worker's messages into the output stream until an event
|
||||
which must be handled in the main watchdog thread (e.g. an I/O error) happens. -/
|
||||
|
|
@ -217,8 +229,9 @@ section ServerM
|
|||
| 0 =>
|
||||
-- Worker was terminated
|
||||
fw.errorPendingRequests o ErrorCode.contentModified
|
||||
(s!"The file worker for {fw.doc.uri} has been terminated. Either the header has changed,"
|
||||
++ " or the file was closed, or the server is shutting down.")
|
||||
(s!"The file worker for {fw.doc.uri} has been terminated. "
|
||||
++ "Either the header has changed, or the file was closed, "
|
||||
++ " or the server is shutting down.")
|
||||
-- one last message to clear the diagnostics for this file so that stale errors
|
||||
-- do not remain in the editor forever.
|
||||
publishDiagnostics fw.doc #[] o
|
||||
|
|
@ -227,8 +240,13 @@ section ServerM
|
|||
return .importsChanged
|
||||
| _ =>
|
||||
-- Worker crashed
|
||||
fw.errorPendingRequests o (if exitCode = 1 then ErrorCode.workerExited else ErrorCode.workerCrashed)
|
||||
s!"Server process for {fw.doc.uri} crashed, {if exitCode = 1 then "see stderr for exception" else "likely due to a stack overflow or a bug"}."
|
||||
let (errorCode, errorCausePointer) :=
|
||||
if exitCode = 1 then
|
||||
(ErrorCode.workerExited, "see stderr for exception")
|
||||
else
|
||||
(ErrorCode.workerCrashed, "likely due to a stack overflow or a bug")
|
||||
fw.errorPendingRequests o errorCode
|
||||
s!"Server process for {fw.doc.uri} crashed, {errorCausePointer}."
|
||||
publishProgressAtPos fw.doc 0 o (kind := LeanFileProgressKind.fatalError)
|
||||
return WorkerEvent.crashed err
|
||||
loop
|
||||
|
|
@ -300,15 +318,22 @@ section ServerM
|
|||
updateFileWorkers { ←findFileWorker! uri with state := WorkerState.crashed queuedMsgs }
|
||||
|
||||
/-- Tries to write a message, sets the state of the FileWorker to `crashed` if it does not succeed
|
||||
and restarts the file worker if the `crashed` flag was already set. Just logs an error if there
|
||||
is no FileWorker at this `uri`.
|
||||
and restarts the file worker if the `crashed` flag was already set. Just logs an error if
|
||||
there is no FileWorker at this `uri`.
|
||||
Messages that couldn't be sent can be queued up via the queueFailedMessage flag and
|
||||
will be discharged after the FileWorker is restarted. -/
|
||||
def tryWriteMessage (uri : DocumentUri) (msg : JsonRpc.Message) (queueFailedMessage := true) (restartCrashedWorker := false) :
|
||||
ServerM Unit := do
|
||||
def tryWriteMessage
|
||||
(uri : DocumentUri)
|
||||
(msg : JsonRpc.Message)
|
||||
(queueFailedMessage := true)
|
||||
(restartCrashedWorker := false)
|
||||
: ServerM Unit := do
|
||||
let some fw ← findFileWorker? uri
|
||||
| do
|
||||
(←read).hLog.putStrLn s!"Cannot send message to unknown document '{uri}':\n{(toJson msg).compress}"
|
||||
let errorMsg :=
|
||||
s!"Cannot send message to unknown document '{uri}':\n"
|
||||
++ s!"{(toJson msg).compress}"
|
||||
(←read).hLog.putStrLn errorMsg
|
||||
return
|
||||
match fw.state with
|
||||
| WorkerState.crashed queuedMsgs =>
|
||||
|
|
@ -353,8 +378,8 @@ def findDefinitions (p : TextDocumentPositionParams) : ServerM <| Array Location
|
|||
if let some module ← searchModuleNameOfFileName path srcSearchPath then
|
||||
let references ← (← read).references.get
|
||||
for ident in references.findAt module p.position (includeStop := true) do
|
||||
if let some definition ← references.definitionOf? ident srcSearchPath then
|
||||
definitions := definitions.push definition
|
||||
if let some ⟨definitionLocation, _⟩ ← references.definitionOf? ident srcSearchPath then
|
||||
definitions := definitions.push definitionLocation
|
||||
return definitions
|
||||
|
||||
def handleReference (p : ReferenceParams) : ServerM (Array Location) := do
|
||||
|
|
@ -364,10 +389,142 @@ def handleReference (p : ReferenceParams) : ServerM (Array Location) := do
|
|||
if let some module ← searchModuleNameOfFileName path srcSearchPath then
|
||||
let references ← (← read).references.get
|
||||
for ident in references.findAt module p.position (includeStop := true) do
|
||||
let identRefs ← references.referringTo module ident srcSearchPath p.context.includeDeclaration
|
||||
result := result.append identRefs
|
||||
let identRefs ← references.referringTo module ident srcSearchPath
|
||||
p.context.includeDeclaration
|
||||
result := result.append <| identRefs.map (·.location)
|
||||
return result
|
||||
|
||||
private def callHierarchyItemOf? (refs : References) (ident : RefIdent) (srcSearchPath : SearchPath)
|
||||
: IO (Option CallHierarchyItem) := do
|
||||
let some ⟨definitionLocation, parentDecl?⟩ ← refs.definitionOf? ident srcSearchPath
|
||||
| return none
|
||||
|
||||
match ident with
|
||||
| .const definitionName =>
|
||||
-- If we have a constant with a proper name, use it.
|
||||
-- If `callHierarchyItemOf?` is used either on the name of a definition itself or e.g. an
|
||||
-- `inductive` constructor, this is the right thing to do and using the parent decl is
|
||||
-- the wrong thing to do.
|
||||
return some {
|
||||
name := definitionName.toString
|
||||
kind := SymbolKind.constant
|
||||
uri := definitionLocation.uri
|
||||
range := definitionLocation.range,
|
||||
selectionRange := definitionLocation.range
|
||||
}
|
||||
| _ =>
|
||||
let some ⟨parentDeclName, parentDeclRange, parentDeclSelectionRange⟩ := parentDecl?
|
||||
| return none
|
||||
|
||||
return some {
|
||||
name := parentDeclName.toString
|
||||
kind := SymbolKind.constant
|
||||
uri := definitionLocation.uri
|
||||
range := parentDeclRange,
|
||||
selectionRange := parentDeclSelectionRange
|
||||
}
|
||||
|
||||
def handlePrepareCallHierarchy (p : CallHierarchyPrepareParams)
|
||||
: ServerM (Array CallHierarchyItem) := do
|
||||
let some path := fileUriToPath? p.textDocument.uri
|
||||
| return #[]
|
||||
|
||||
let srcSearchPath := (← read).srcSearchPath
|
||||
let some module ← searchModuleNameOfFileName path srcSearchPath
|
||||
| return #[]
|
||||
|
||||
let references ← (← read).references.get
|
||||
let idents := references.findAt module p.position (includeStop := true)
|
||||
|
||||
let items ← idents.filterMapM fun ident => callHierarchyItemOf? references ident srcSearchPath
|
||||
return items
|
||||
|
||||
def handleCallHierarchyIncomingCalls (p : CallHierarchyIncomingCallsParams)
|
||||
: ServerM (Array CallHierarchyIncomingCall) := do
|
||||
let some path := fileUriToPath? p.item.uri
|
||||
| return #[]
|
||||
|
||||
let srcSearchPath := (← read).srcSearchPath
|
||||
let some module ← searchModuleNameOfFileName path srcSearchPath
|
||||
| return #[]
|
||||
|
||||
let references ← (← read).references.get
|
||||
let identRefs ← references.referringTo module (.const p.item.name.toName) srcSearchPath false
|
||||
|
||||
let incomingCalls := identRefs.filterMap fun ⟨location, parentDecl?⟩ => Id.run do
|
||||
|
||||
let some ⟨parentDeclName, parentDeclRange, parentDeclSelectionRange⟩ := parentDecl?
|
||||
| return none
|
||||
return some {
|
||||
«from» := {
|
||||
name := parentDeclName.toString
|
||||
kind := SymbolKind.constant
|
||||
uri := location.uri
|
||||
range := parentDeclRange
|
||||
selectionRange := parentDeclSelectionRange
|
||||
}
|
||||
fromRanges := #[location.range]
|
||||
}
|
||||
|
||||
return collapseSameIncomingCalls incomingCalls
|
||||
|
||||
where
|
||||
|
||||
collapseSameIncomingCalls (incomingCalls : Array CallHierarchyIncomingCall)
|
||||
: Array CallHierarchyIncomingCall :=
|
||||
let grouped := incomingCalls.groupByKey (·.«from»)
|
||||
let collapsed := grouped.toArray.map fun ⟨_, group⟩ => {
|
||||
«from» := group[0]!.«from»
|
||||
fromRanges := group.concatMap (·.fromRanges)
|
||||
}
|
||||
collapsed
|
||||
|
||||
def handleCallHierarchyOutgoingCalls (p : CallHierarchyOutgoingCallsParams)
|
||||
: ServerM (Array CallHierarchyOutgoingCall) := do
|
||||
let some path := fileUriToPath? p.item.uri
|
||||
| return #[]
|
||||
|
||||
let srcSearchPath := (← read).srcSearchPath
|
||||
let some module ← searchModuleNameOfFileName path srcSearchPath
|
||||
| return #[]
|
||||
|
||||
let references ← (← read).references.get
|
||||
|
||||
let some refs := references.allRefs.find? module
|
||||
| return #[]
|
||||
|
||||
let items ← refs.toArray.filterMapM fun ⟨ident, info⟩ => do
|
||||
let outgoingUsages := info.usages.filter fun usage => Id.run do
|
||||
let some parentDecl := usage.parentDecl?
|
||||
| return false
|
||||
return p.item.name.toName == parentDecl.name
|
||||
|
||||
let outgoingUsages := outgoingUsages.map (·.range)
|
||||
if outgoingUsages.isEmpty then
|
||||
return none
|
||||
|
||||
let some item ← callHierarchyItemOf? references ident srcSearchPath
|
||||
| return none
|
||||
|
||||
-- filter local defs from outgoing calls
|
||||
if item.name == p.item.name then
|
||||
return none
|
||||
|
||||
return some ⟨item, outgoingUsages⟩
|
||||
|
||||
return collapseSameOutgoingCalls items
|
||||
|
||||
where
|
||||
|
||||
collapseSameOutgoingCalls (outgoingCalls : Array CallHierarchyOutgoingCall)
|
||||
: Array CallHierarchyOutgoingCall :=
|
||||
let grouped := outgoingCalls.groupByKey (·.to)
|
||||
let collapsed := grouped.toArray.map fun ⟨_, group⟩ => {
|
||||
to := group[0]!.to
|
||||
fromRanges := group.concatMap (·.fromRanges)
|
||||
}
|
||||
collapsed
|
||||
|
||||
def handleWorkspaceSymbol (p : WorkspaceSymbolParams) : ServerM (Array SymbolInformation) := do
|
||||
if p.query.isEmpty then
|
||||
return #[]
|
||||
|
|
@ -436,7 +593,8 @@ section NotificationHandling
|
|||
let newDocText := foldDocumentChanges changes oldDoc.text
|
||||
let newDoc : DocumentMeta := ⟨doc.uri, newVersion, newDocText, oldDoc.dependencyBuildMode⟩
|
||||
updateFileWorkers { fw with doc := newDoc }
|
||||
tryWriteMessage doc.uri (Notification.mk "textDocument/didChange" p) (restartCrashedWorker := true)
|
||||
let notification := Notification.mk "textDocument/didChange" p
|
||||
tryWriteMessage doc.uri notification (restartCrashedWorker := true)
|
||||
|
||||
def handleDidClose (p : DidCloseTextDocumentParams) : ServerM Unit :=
|
||||
terminateFileWorker p.textDocument.uri
|
||||
|
|
@ -469,15 +627,18 @@ section NotificationHandling
|
|||
if (← fw.pendingRequestsRef.get).contains p.id then
|
||||
tryWriteMessage uri (Notification.mk "$/cancelRequest" p) (queueFailedMessage := false)
|
||||
|
||||
def forwardNotification {α : Type} [ToJson α] [FileSource α] (method : String) (params : α) : ServerM Unit :=
|
||||
def forwardNotification {α : Type} [ToJson α] [FileSource α] (method : String) (params : α)
|
||||
: ServerM Unit :=
|
||||
tryWriteMessage (fileSource params) (Notification.mk method params) (queueFailedMessage := true)
|
||||
end NotificationHandling
|
||||
|
||||
section MessageHandling
|
||||
def parseParams (paramType : Type) [FromJson paramType] (params : Json) : ServerM paramType :=
|
||||
match fromJson? params with
|
||||
| Except.ok parsed => pure parsed
|
||||
| Except.error inner => throwServerError s!"Got param with wrong structure: {params.compress}\n{inner}"
|
||||
| Except.ok parsed =>
|
||||
pure parsed
|
||||
| Except.error inner =>
|
||||
throwServerError s!"Got param with wrong structure: {params.compress}\n{inner}"
|
||||
|
||||
def forwardRequestToWorker (id : RequestID) (method : String) (params : Json) : ServerM Unit := do
|
||||
let uri: DocumentUri ←
|
||||
|
|
@ -532,25 +693,48 @@ section MessageHandling
|
|||
(← read).hOut.writeLspResponse ⟨id, definitions⟩
|
||||
return
|
||||
match method with
|
||||
| "textDocument/references" => handle ReferenceParams (Array Location) handleReference
|
||||
| "workspace/symbol" => handle WorkspaceSymbolParams (Array SymbolInformation) handleWorkspaceSymbol
|
||||
| "textDocument/prepareRename" => handle PrepareRenameParams (Option Range) handlePrepareRename
|
||||
| "textDocument/rename" => handle RenameParams WorkspaceEdit handleRename
|
||||
| _ => forwardRequestToWorker id method params
|
||||
| "textDocument/references" =>
|
||||
handle ReferenceParams (Array Location) handleReference
|
||||
| "workspace/symbol" =>
|
||||
handle WorkspaceSymbolParams (Array SymbolInformation) handleWorkspaceSymbol
|
||||
| "textDocument/prepareCallHierarchy" =>
|
||||
handle CallHierarchyPrepareParams (Array CallHierarchyItem) handlePrepareCallHierarchy
|
||||
| "callHierarchy/incomingCalls" =>
|
||||
handle CallHierarchyIncomingCallsParams (Array CallHierarchyIncomingCall)
|
||||
handleCallHierarchyIncomingCalls
|
||||
| "callHierarchy/outgoingCalls" =>
|
||||
handle Lsp.CallHierarchyOutgoingCallsParams (Array CallHierarchyOutgoingCall)
|
||||
handleCallHierarchyOutgoingCalls
|
||||
| "textDocument/prepareRename" =>
|
||||
handle PrepareRenameParams (Option Range) handlePrepareRename
|
||||
| "textDocument/rename" =>
|
||||
handle RenameParams WorkspaceEdit handleRename
|
||||
| _ =>
|
||||
forwardRequestToWorker id method params
|
||||
|
||||
def handleNotification (method : String) (params : Json) : ServerM Unit := do
|
||||
let handle := (fun α [FromJson α] (handler : α → ServerM Unit) => parseParams α params >>= handler)
|
||||
let handle := fun α [FromJson α] (handler : α → ServerM Unit) =>
|
||||
parseParams α params >>= handler
|
||||
match method with
|
||||
| "textDocument/didOpen" => handle _ handleDidOpen
|
||||
| "textDocument/didChange" => handle DidChangeTextDocumentParams handleDidChange
|
||||
| "textDocument/didClose" => handle DidCloseTextDocumentParams handleDidClose
|
||||
| "workspace/didChangeWatchedFiles" => handle DidChangeWatchedFilesParams handleDidChangeWatchedFiles
|
||||
| "$/cancelRequest" => handle CancelParams handleCancelRequest
|
||||
| "$/lean/rpc/connect" => handle RpcConnectParams (forwardNotification method)
|
||||
| "$/lean/rpc/release" => handle RpcReleaseParams (forwardNotification method)
|
||||
| "$/lean/rpc/keepAlive" => handle RpcKeepAliveParams (forwardNotification method)
|
||||
| _ =>
|
||||
if !"$/".isPrefixOf method then -- implementation-dependent notifications can be safely ignored
|
||||
| "textDocument/didOpen" =>
|
||||
handle _ handleDidOpen
|
||||
| "textDocument/didChange" =>
|
||||
handle DidChangeTextDocumentParams handleDidChange
|
||||
| "textDocument/didClose" =>
|
||||
handle DidCloseTextDocumentParams handleDidClose
|
||||
| "workspace/didChangeWatchedFiles" =>
|
||||
handle DidChangeWatchedFilesParams handleDidChangeWatchedFiles
|
||||
| "$/cancelRequest" =>
|
||||
handle CancelParams handleCancelRequest
|
||||
| "$/lean/rpc/connect" =>
|
||||
handle RpcConnectParams (forwardNotification method)
|
||||
| "$/lean/rpc/release" =>
|
||||
handle RpcReleaseParams (forwardNotification method)
|
||||
| "$/lean/rpc/keepAlive" =>
|
||||
handle RpcKeepAliveParams (forwardNotification method)
|
||||
| _ =>
|
||||
-- implementation-dependent notifications can be safely ignored
|
||||
if !"$/".isPrefixOf method then
|
||||
(←read).hLog.putStrLn s!"Got unsupported notification: {method}"
|
||||
end MessageHandling
|
||||
|
||||
|
|
@ -614,7 +798,8 @@ section MainLoop
|
|||
handleCrash fw.doc.uri #[]
|
||||
mainLoop clientTask
|
||||
| WorkerEvent.terminated =>
|
||||
throwServerError "Internal server error: got termination event for worker that should have been removed"
|
||||
throwServerError <| "Internal server error: got termination event for worker that "
|
||||
++ "should have been removed"
|
||||
| .importsChanged =>
|
||||
startFileWorker fw.doc
|
||||
mainLoop clientTask
|
||||
|
|
@ -637,6 +822,7 @@ def mkLeanServerCapabilities : ServerCapabilities := {
|
|||
definitionProvider := true
|
||||
typeDefinitionProvider := true
|
||||
referencesProvider := true
|
||||
callHierarchyProvider := true
|
||||
renameProvider? := some {
|
||||
prepareProvider := true
|
||||
}
|
||||
|
|
@ -677,7 +863,8 @@ def initAndRunWatchdogAux : ServerM Unit := do
|
|||
def findWorkerPath : IO System.FilePath := do
|
||||
let mut workerPath ← IO.appPath
|
||||
if let some path := (←IO.getEnv "LEAN_SYSROOT") then
|
||||
workerPath := System.FilePath.mk path / "bin" / "lean" |>.addExtension System.FilePath.exeExtension
|
||||
workerPath := System.FilePath.mk path / "bin" / "lean"
|
||||
|>.addExtension System.FilePath.exeExtension
|
||||
if let some path := (←IO.getEnv "LEAN_WORKER_PATH") then
|
||||
workerPath := System.FilePath.mk path
|
||||
return workerPath
|
||||
|
|
|
|||
|
|
@ -23,10 +23,10 @@ def usedAndUnusedVariables : Nat :=
|
|||
3
|
||||
x
|
||||
|
||||
def unusedWhereVariable : Nat :=
|
||||
def whereVariable : Nat :=
|
||||
3
|
||||
where
|
||||
x := 5
|
||||
x := 5 -- x is globally available via `whereVariable.x`
|
||||
|
||||
def unusedWhereArgument : Nat :=
|
||||
f 2
|
||||
|
|
|
|||
|
|
@ -1,9 +1,7 @@
|
|||
linterUnusedVariables.lean:16:21-16:22: warning: unused variable `x` [linter.unusedVariables]
|
||||
linterUnusedVariables.lean:17:6-17:7: warning: unused variable `y` [linter.unusedVariables]
|
||||
linterUnusedVariables.lean:22:8-22:9: warning: unused variable `x` [linter.unusedVariables]
|
||||
linterUnusedVariables.lean:29:2-29:3: warning: unused variable `x` [linter.unusedVariables]
|
||||
linterUnusedVariables.lean:34:5-34:6: warning: unused variable `x` [linter.unusedVariables]
|
||||
linterUnusedVariables.lean:39:2-39:3: warning: unused variable `f` [linter.unusedVariables]
|
||||
linterUnusedVariables.lean:39:5-39:6: warning: unused variable `x` [linter.unusedVariables]
|
||||
linterUnusedVariables.lean:42:7-42:8: warning: unused variable `x` [linter.unusedVariables]
|
||||
linterUnusedVariables.lean:45:8-45:9: warning: unused variable `x` [linter.unusedVariables]
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue