Rename code action doesn't work with dot notation

Stream: lean4

[Yury G. Kudryashov]

I've tried to rename a lemma using "rename" code action. Both old and new names were namespaced (say, MyProperty.old_name and MyProperty.new_name). It was used as h.old_name later in the file. This occurrence was replaced with h.MyProperty.new_name. Is it a known bug?

P.S.: I'm using Emacs, but I assume that this is implemented in the server, so should not depend on the client.

[Mario Carneiro]

yes, this is a known limitation owing to the fact that the info tree doesn't store enough information to calculate the correct text without recompiling the whole project

[Yury G. Kudryashov]

Thanks for the explanation.

[Patrick Massot]

I’m sure this will be fixed in the near future.