feat: rename request handler #2462
Conversation
|
How does this handle a rename that starts with namespace Foo
def bar := sorry
end Foo
example := Foo.barand renames |
|
It's not particularly clever about namespaces, it will replace all occurrences of things that resolve to namespace Foo
def _root_.Baz.bar := sorry
end Foo
example := _root_.Baz.barProbably you don't want to be using |
|
Does that mean that in namespace Foo
def bar := sorry
end Foo
open Foo
example := barrenaming |
|
renaming |
|
Just noting that this would be a super helpful feature for refactoring mathlib |
github-actions
bot
added
the
toolchain-available
|
leanprover-community-mathlib4-bot
added
the
builds-mathlib
|
the error looks very strange, likely intermittent, and looks similar to this zulip issue |
|
Yes, the failing test is most likely intermittent. Sebastian is looking into it. |
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 implements a request handler for the
textDocument/renameLSP request, enabling renames via F2. It handles both local renames (e.g.let x := 1; xtolet y := 1; y) as well as global renames (definitions).Unfortunately it does not work for "orphan" files outside a project, as it uses ilean data for the current file and this does not seem to be saved for orphan files. As a result, the test file does not work, although one can manually test the implementation against a project such as mathlib. (This issue already exists for the "references" request, e.g. ctrl click on the first
xinlet x := 1; xtakes you to the second one only if you are not in an orphan file.)