Refactorings for Lean code

Stream: job postings

[Denis Gorbachev]

Hi!

Is anyone interested in doing a paid project implementing refactorings for Lean code? Specifically:

• Move the definition to another file
• Rename a local variable
• Auto-import a definition

I hope those functions would be helpful for every Lean programmer, and I'm willing to pay for the implementation.

[Scott Morrison]

You might be interested in the #find_home and #minimize_imports commands. Unfortunately both are buggy at the point, but fixing them is on my to-do list.

[Scott Morrison]

Hopefully they could be helpful to drive actual VSCode code actions.

[Bolton Bailey]

I would like there to be some kind of "extract lemma" code action which takes the proof state at a particular point, and creates a new sorried lemma immediately above the theorem in question with all of the hypotheses as arguments and the goal as a conclusion.

[Kayla Thomas]

(deleted)

[Kayla Thomas]

(deleted)

[Kayla Thomas]

Bolton Bailey said:

I would like there to be some kind of "extract lemma" code action which takes the proof state at a particular point, and creates a new sorried lemma immediately above the theorem in question with all of the hypotheses as arguments and the goal as a conclusion.

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/ExtractGoal.html#extractGoal

[Denis Gorbachev]

PSA: The Lean 4 Code Actions is now available on VSCode marketplace: https://marketplace.visualstudio.com/items?itemName=denis-gorbachev.lean4-code-actions

[Eric Wieser]

regarding the sibling package https://marketplace.visualstudio.com/items?itemName=denis-gorbachev.lean4-language-configuration; making ` an auto-closing bracket is likely pretty annoying for meta code, where the unmatched `(tactic| foo ) is common

[Denis Gorbachev]

Yes, that's exactly the reason it's in a separate extension.

The rationale for making ` an auto-closing bracket was to simplify writing docstrings in Markdown, where two backticks wrap the inline code. Ideally, the IDE should auto-close ` in docstrings but not in actual code.

Not sure how to resolve this - feel free to suggest.

[Eric Wieser]

Ideally you would add it here

[Eric Wieser]

Aha, I've tracked it down to https://github.com/microsoft/vscode/issues/133397

[Denis Gorbachev]

Yeah, still an open issue...

[Denis Gorbachev]

Eric Wieser said:

Ideally you would add it here

We only have access to LanguageConfiguration from 'vscode' package, and autoClosingPairs are deprecated there.

I've already extracted whatever was possible to extract to code in languageConfiguration.ts