refactoring definition and theorem names

Stream: lean4

[Paige Thomas]

Is there a way to automatically propagate the renaming of a definition or theorem throughout an entire project? The refactor command in Visual Code doesn't seem to work for this, so I change one name at a time, rebuild after each, and fix it where it breaks. If I do a replace in all files, it doesn't take the semantics of what a definition or theorem is into account.

[Chris Bailey]

My experience has been that the right-click option "rename symbol" works quite well, have you tried that instead of refactor?

[Paige Thomas]

Oh, I meant that, instead of the literal "refactor" command. I've had trouble with it in the past, but I can give it another try.

[Paige Thomas]

It doesn't seem to work for at least the case Formula_.free_var_set -> Formula_.free_var_set_test. Maybe because it is an extension of the Formula_ definition?

[Paige Thomas]

It goes from

def Formula_.free_var_set : Formula_ → Finset VarName_
  | pred_const_ _ xs => xs.toFinset
  | pred_var_ _ xs => xs.toFinset
  | eq_ x y => {x, y}
  | true_ => ∅
  | false_ => ∅
  | not_ phi => phi.free_var_set
  | imp_ phi psi => phi.free_var_set ∪ psi.free_var_set
  | and_ phi psi => phi.free_var_set ∪ psi.free_var_set
  | or_ phi psi => phi.free_var_set ∪ psi.free_var_set
  | iff_ phi psi => phi.free_var_set ∪ psi.free_var_set
  | forall_ x phi => phi.free_var_set \ {x}
  | exists_ x phi => phi.free_var_set \ {x}
  | def_ _ xs => xs.toFinset

to

def Formula_.free_var_set_test : Formula_ → Finset VarName_
  | pred_const_ _ xs => xs.toFinset
  | pred_var_ _ xs => xs.toFinset
  | eq_ x y => {x, y}
  | true_ => ∅
  | false_ => ∅
  | not_ phi => phi.Formula_.free_var_set_test
  | imp_ phi psi => phi.Formula_.free_var_set_test ∪ psi.Formula_.free_var_set_test
  | and_ phi psi => phi.Formula_.free_var_set_test ∪ psi.Formula_.free_var_set_test
  | or_ phi psi => phi.Formula_.free_var_set_test ∪ psi.Formula_.free_var_set_test
  | iff_ phi psi => phi.Formula_.free_var_set_test ∪ psi.Formula_.free_var_set_test
  | forall_ x phi => phi.Formula_.free_var_set_test \ {x}
  | exists_ x phi => phi.Formula_.free_var_set_test \ {x}
  | def_ _ xs => xs.toFinset

[Chris Bailey]

Oh that's interesting. Yeah for names with more than one segment it does seem to handle subsequent invocations via dot notation poorly, I'm so used to opening namespace Foo right after the base definition.

[Paige Thomas]

If I try to rename just the suffix in for example psi.free_var_set, the Formula_.free_var_set becomes free_var_set_test.

[Paige Thomas]

Would this have to be addressed in Visual Code itself?

[Chris Bailey]

I would assume the behavior of the rename action is governed by a combination of the lean vscode extension and the lsp stuff that's built in to lean (in the Lean.Lsp namespace), and not vscode itself.

[Chris Bailey]

It's a client/server architecture, so I think the Lean LSP gets a message along the lines of "user requests rename(<foo>, <bar>) @ <loc>" and the language server (rather than the editor) is responsible for working out the contents of the message to send back reflecting the actual change.

[Paige Thomas]

I see.

[Mario Carneiro]

This is a known limitation of the current implementation, it doesn't have the context it needs to be able to do the replacement correctly. It's probably worth filing a bug anyway, but it is not an easy fix, it requires more data to be stored in ilean files