leansed

Stream: general

[Johan Commelin]

How hard would it be to write a leansed? I want to tell lean: hey, update all my source code files so that submodule.subtype is now called submodule.incl everywhere.

[Oliver Nash]

We need JetBrains to divert some effort away from Arend and write a Lean Resharper.

[Mario Carneiro]

Well, vscode has built in support for renames of various kinds, the hard part is getting the relevant info out of lean

[Reid Barton]

Just query server mode for the identifier at every position and check which point to submodule.subtype. It should only take several hours

[Reid Barton]

Or, just change it and fix the breakage

[Mario Carneiro]

Didn't @Jason Rute do a test like this?

[Jason Rute]

Yes, I can confirm it takes a several hours to run over mathlib (or more like a whole day). Although, you don’t need to look at every character for this use case which would speed it up. It might only take as much time as it takes to compile your project. Also the server sometimes acts weird when information is nested. It might point to the tactic and not to the relevant decl.

[Jason Rute]

I still have to fix some bugs in the Lean server python tool, but after that you could give it a try. (But it would probably just be faster to search for all instance of subtype and check each individually. Yet it is more fun to build a tool.)

[Patrick Massot]

Well, you can combine both approaches. You can grep for some word, and then using the Lean server to hunt down false positives.

[Mario Carneiro]

I usually find false negatives to be the harder problem

[Mario Carneiro]

when you use e.g. dot notation to apply a function it can be very hard to find if it otherwise has a common name like .add or.to_fun

[Mario Carneiro]

or .1

[Jason Rute]

It’s that a false positive?

[Johan Commelin]

If it runs in < 10 hours on my box, I'm happy. It means I can fire up such a refactor task in 3 minutes before I go to bed, and it should be almost finished by the time I've done my breakfast and morning workout.

[Mario Carneiro]

I mean if you are looking for subtype.val, you will have a hard time finding a use via x.1 unless you ask lean

[Johan Commelin]

That's a lot better than the Read-Edit-Fix-Compile-loop

[Jason Rute]

Ok. I need to finish these PRs (there was some discussion about the design of the tests and then I got into other projects :oh_no: ) and then probably give you an example for you to get started.