Rename action simply kills namespaces

Stream: general

[Moritz R]

Currently the LSP rename action (invoced by pressing F2 or Right-Click -> Rename Symbol is in a poor state.
Renaming a namespaced Definition myfun to myfun2 will replace everything with myfun2, regardless of wether it was used as myfun, Namespace1.myfun or Namespace2.Namespace1.myfun, therefore breaking code everywhere.

Consider the following concrete examples

/- Renaming `myfun` at the definition breaks all of the other usages below. -/

namespace Outernamespace
namespace Innernamespace

def myfun (x : Nat) : Nat := x * 5

end Innernamespace
end Outernamespace


-- Scenario 1: Fully Qualified Usage
def testFull : Nat :=
  Outernamespace.Innernamespace.myfun 10


-- Scenario 2: Partially Qualified Usage (opening the outer namespace)
section PartialOpen

open Outernamespace

def testPartial : Nat :=
  Innernamespace.myfun 20

end PartialOpen


-- Scenario 3: Unqualified Usage (opening the exact namespace)
section FullOpen

open Outernamespace.Innernamespace

def testUnqualified : Nat :=
  myfun 30
end FullOpen


-- Scenario 4: Usage within the same namespace hierarchy
namespace Outernamespace
  def testInternal : Nat :=
    Innernamespace.myfun 40
end Outernamespace


-- Scenario 5: Usage via export
namespace Wrapper
  export Outernamespace.Innernamespace (myfun)
end Wrapper

def testExported : Nat :=
  Wrapper.myfun 50





/-- Rename `Button` here. It breaks the definition below. -/
inductive Button where
  | primary
  | secondary

def myButton : Button :=
  Button.primary

There is a Lean issue existing for this since 2023 and i really think this deserves more attention.
Renaming lemmas and definitions is a very important part of maintaining and writing new APIs and as such a core editing experience.
I think a slightly more robust solution would save us lots of time fixing renamings every day every user.

[Moritz R]

At this point, would new upvotes on this issue give it any new attention?

[Patrick Massot]

Let me state a bold conjecture: I think the Lean team is actually aware of this issue.

[Kevin Buzzard]

The issue has been triaged as P-medium so probably it's behind the 44 P-high issues.

[Moritz R]

Maybe i just want to argue that it should be a P-high then ;)

[Kevin Buzzard]

Right, but it is the FRO who is making these decisions, and probably without any new evidence to change their previous decision, it will stay at P-medium. One person saying "actually I agree" probably isn't enough to swing it. Just give the issue a thumbs up and try and encourage others to do so.

[Marc Huisinga]

This particular issue is in my backlog, and it is currently lower priority than the auto-formatter for Lean that I am working on :-)
After the code formatter, if nothing else comes up, we will invest more time into refining code action support in core and re-thinking the renaming mechanism will be a part of that.