Refactoring tool

Stream: lean4

[Patrick Massot]

I'm curious to know where we are with refactoring tools. How far are we from having a tool that could make https://github.com/leanprover/lean4/commit/8335a82aedc280c0396d14192b607b8f6770fc9f mostly automatic (I'm talking about fixing all files, not the modification to src/Lean/MetavarContext.lean). Is it already automatic? Will it be automatic soon?

[Henrik Böving]

I think having a general refactoring tool for Lean 4 is quite hard given the fact how insanely we can influence the way a Lean file works as a user. For example if I change the name of a method but it is used within a macro or worse an elaborator how would one implement a tool that can detect this?

Though I'm guessing it is quite possible to write refactor tools specific to certain DSLs like do notation but I am not aware of any work on this.

[Patrick Massot]

We could still have a "best effort" tool.

[Gabriel Ebner]

I change the name of a method but it is used within a macro or worse an elaborator

Note that syntax quotations are just regular syntax, so any rewriting would presumably apply to them as well. Names like ``foo could be automatically changed as well (which works as long as the signature is the same).

[Gabriel Ebner]

What you could do today is insert a Syntax.replaceM call here: https://github.com/leanprover/lean4/blob/005b8aa9515ab21e8d4a6325fdd52276df24dd5d/script/reformat.lean#L69

stx.replaceM fun
  | `(isMVarDelayedAssigned $mvarId) => some <$> `($(mvarId).isMVarDelayedAssigned)
  |  _ => none

But that would format all files with the current pretty-printer. There are three problems with that (off the top of my head):

1. Changes the formatting (i.e. huge diff).
2. You might not like the result.
3. Fails on some syntax (I believe `(tk%$blah) makes it abort).

We're close, but there's still some way to go. I believe Sebastian has Lars working on that.

[Henrik Böving]

While this works for here the approach is not general to Lean right? (even without user macros/elabs) for example if we have some function, say fromArray in a namespace, say Std.HashSet.fromArray and we want to replace that things get harder because maybe the same name could also come from other namespaces so you have to keep track of what namespaces are open. Or also with the .fromArray notation you'd have to know the expected type to actually know whether you want to replace the function call or not.

[Gabriel Ebner]

That's the nice thing: expected types, etc. are stored in the info tree. So the rewriting tool could theoretically skip the rewrite if the expected type is wrong (avoid issues with coercions), or even try to re-elaborate the whole command after rewriting.