Renaming decls using LSP

Stream: lean4

[Johan Commelin]

If I want to rename my lemma xyzzy_foo to xyzzy.bar in all of mathlib, it would be great if this can be done automatically. And maybe I have a list of decls that should be renamed, and I want to do this in batch mode.
How close are we to having such code transformation tools? @Mario Carneiro I think you've mentioned some thoughts on this several times... (-;

[Mario Carneiro]

that's lean4#2462

[Johan Commelin]

Thanks for the pointer! Did you make any progress on issues 1 and 2 in the review comment?

[Damiano Testa]

Johan, while waiting for the "correct" solution would you be interested in a command-line patch?

I think that the ilean files contain information of where each declaration is located in the code: I used that to surgically replace every theorem to lemma. I could look into finding all declaration names as well, if you wanted.

[Johan Commelin]

Hah, if that works, I would certainly be happy to have it!
I think it's great if we can have renaming PRs where the diff is generated by invoking such a command. Makes it much easier to review the PRs if you know that's how they're created.

[Johan Commelin]

And it makes it easier to split PRs into the manual and automatic parts.

[Damiano Testa]

Ok, I'll look into this: it should be easy, since it seems a slight adaptation of what I already had, but I will have to figure out how to deal with name-spacing.

[Damiano Testa]

(Also, this will certainly not take care of docs/comments: those names would have to be inspected by a different means than what I have in mind.)

[Notification Bot]

Damiano Testa has marked this topic as resolved.

[Notification Bot]

Damiano Testa has marked this topic as unresolved.

[Damiano Testa]

Sorry about the misclick! :upside_down:

[Johan Commelin]

Yeah docs/comments is a good point.

[Damiano Testa]

Johan, do you have a concrete case where you would like this replacement to happen?

I have a very preliminary version and it would be good to test it and fix some gross mistakes that it contains!

Right now, I already know that it will do the wrong thing if the declaration is used in dot-notation and if it is called with @.

[Eric Wieser]

I'm hoping that @David Thrane Christiansen's documentation plans will leave us with comments that are recognized by the LSP

[Damiano Testa]

I am testing the replacement Real.tan to Real.Tan.

Except for the namespacing issues, the only other problem in this case is that I use sed to capture patterns and there are lines where there are more than 9 captures... :face_palm:

[Jireh Loreaux]

Related: I just opened #8433 to figure out which declarations were renamed. It's very pedestrian; it only lists all declarations in changed files and computes the diff.

[Johan Commelin]

@Damiano Testa My question was inspired by #8406. A tool like this might make it easier to separate the "renaming" and the "golfing" parts of such PRs.

[Damiano Testa]

Ok, I'll test the change

isAlgebraic_algebraMap -> IsAlgebraic.algebraMap

and see how it performs.

[Damiano Testa]

You can see the progress here: #8437.

I may regret this, but I have made more than one rename while testing the tool.

[Damiano Testa]

This was easy and successful. In hindsight, the only change that had to be manually made for this PR is protecting one of the renamed theorems.

[Damiano Testa]

I tried to keep the git history clean and the changes only affect 15 lines, in case you want to take a look at how the renaming of the declaration works.

[Andrew Yang]

Is there a way to use this script?

[Damiano Testa]

I thought that Mario had a version of the renaming tool written in Lean that was merged soon after I used the bash-one. Otherwise, I can share a version of my string-based one, but likely tomorrow, since I'm no longer at my computer for today.

[Marc Huisinga]

You should be able to right click on an identifier and select "Rename symbol" now.