rename a declaration

Stream: general

[Johan Commelin]

How hard would it be to ask Lean to replace all occurences of foo.bar.xyzzy with baz.quux? This should also work of the namespace foo, foo.bar, and/or baz has been opened...

[Mario Carneiro]

nope

[Johan Commelin]

Hmmm.... it's "Mario nope" hard. That's unfortunate.

[Johan Commelin]

We have the hover information, and olean files know everything about source locations. So I was hoping that we could run some substitution over the source files...

[Mario Carneiro]

you might be able to exploit go to definition support, but that's exactly the sort of thing that not having an external parser causes

[Mario Carneiro]

It will require some new lean API

[Sebastian Ullrich]

I've actually given some thought to how to do such refactorings in the Lean 3 parser, even without a concrete syntax tree. You could change the scanner to output each read token to some output stream before reading the next token from the input, which gives the parser (which does name resolution in Lean 3) a chance to modify that token before calling into the scanner again...

[Mario Carneiro]

Could it send the data to vscode instead? I know vscode / LSP has a rename option, and it seems like file editing is better done there