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.

[Michael Stoll]

I was using this feature in #12635 to rename (e.g.) Filter.tendsto.exp to Filter.Tendsto.rexp, and I noticed two shortcomings, the first more serious than the second:

• it seems not to play well with dot notation (it finds the correct instances to replace, but replaces h.exp by h.Filter.Tendsto.rexp (which results in an error) rather than h.rexp);
• it does not take into account open namespaces (replacing Tendsto.exp in a context where Filter is open by Filter.Tendsto.rexp).

The second one does not affect the correctness of the result, but makes the code longer, whereas the first one requires manual intervention.

I have no idea how this works, so I don't know how easy it is to fix.

[Yaël Dillies]

Yes, I think I already raised that somewhere. The issue is that the LSP command has conception of namespaces. It just that said name is from colon this to colon that on said line, but doesn't know what namespaces the calls assumed were open

[Yaël Dillies]

I think the correct algorithm would be "If user renames A to B by clicking F2 inside namespace C, replace each occurrence D of C.A (fully qualified name) in namespace E by 'C.B with the longest common prefix of E and C.B"

[Kim Morrison]

@Michael Stoll, would you mind opening (separate) issues for these two?

[Mario Carneiro]

Note, a 'proper' global rename is within scope of the lake exe refactor project I've been planning for a while now. (The way it works: it elaborates every file, then calls a custom code hook which does elaborator-aware syntax replacements. Pro: it can make intelligent edits with the right context; Con: it takes as long as a full build to run.)

[Michael Stoll]

A comment in lean4#2462 says

... but the output is just naive text substitution, it just puts whatever you say as the replacement text.

which I assume explains the behavior I observed. There is already an issue lean4#2936 "Renaming does not correctly deal with namespaces", which seems related to my second point above. Should I still open an issue for the first point?

[Yaël Dillies]

Another issue is that the ileans do not get updated after a rename. This means that you can perform at most one rename that changes the length of a declaration name before rebuilding if you don't want your project to be mangled.

[Michael Rothgang]

Yaël Dillies said:

Another issue is that the ileans do not get updated after a rename. This means that you can perform at most one rename that changes the length of a declaration name before rebuilding if you don't want your project to be mangled.

This is why I don't use F2 for doing batch-renames any more.

[Yaël Dillies]

It's really quite incapacitating :frowning:

[Mario Carneiro]

I guess we could update ileans "blindly", but it's probably hit-or-miss

[Mario Carneiro]

updating ileans intelligently puts you back in the same ballpark as lake exe refactor i.e. full rebuild