Mass edit tools

Stream: mathlib4

[Yaël Dillies]

Now that a single declaration can be spelled differently in lemma statements and lemma names, we really need mass edit tools. Is anybody working on something like this?

[Eric Rodriguez]

what do you mean by this?

[Yaël Dillies]

I mean a way to rename a declaration everywhere at once, and if possible in lemma names too.

[Eric Rodriguez]

Oh, I see. I mean, there should just be two names, right? So ctrl+shift+f with those two names should do a good job of it

[Henrik Böving]

This is in theory a feature that an LSP server can supply to your editor (apart from the "also rename in lemmata" part), it is just not implement yet in Lean 4. Maybe the LSP people would be interested in adding support for this?

[Yaël Dillies]

If it can't rename the lemmas, can it at least somehow flag the lemmas whose statement was changed because of the rename? Then one can go through them one by one, which is already magnitudes better to what we have in Lean 3.

[Henrik Böving]

Hmm, the LSP standard says (https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_rename) that upon a rename request the server can answer with an arbitrary WorkspaceEdit so it could in theory put some text on the lemmas whose statement was influenced I guess?

It could of course also attempt to change the name of the lemma itself, I'm just unsure whether it would get that right so consistently that it would be desirable given the naming convention.

[Yaël Dillies]

Yes, that sounds perfect.