VSCode extension for Lean code actions

Stream: general

[Mario Carneiro]

Have you considered upstreaming this to vscode-lean4?

[Scott Morrison]

auto-import and rename in vscode-lean4 would be awesome

[Denis Gorbachev]

Mario Carneiro said:

Have you considered upstreaming this to vscode-lean4?

Yes, I'd love to. Who is the right person to talk with regarding upstreaming?

[Notification Bot]

3 messages were moved here from #announce > VSCode extension for Lean code actions by Scott Morrison.

[Scott Morrison]

@Wojciech Nawrocki and @Gabriel Ebner have done most of the recent work on the extension.

I think you can just start making PRs. (Preferably separate PRs for separate actions, to ease review.)

[Denis Gorbachev]

I'll send a preliminary PR to discuss the merge :ok:

[Floris van Doorn]

Some feature requests that I think would be very nice:

• "clean up" code by looking at open namespaces / (scoped) notation and using that to shorten names / use the notation. Example:
  Example using mathlib:

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

namespace Real
noncomputable def tau := 2 * Real.pi
/- using the command gives:
noncomputable def tau := 2 * π
-/
end Real

• Look at namespaces / scoped notations that could be opened to shorten parts of the code. Example:

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

noncomputable def tau := 2 * Real.pi
/- using the command gives:
open Real in
noncomputable def tau := 2 * π
-/

• Use variables declared in the file and reuse those variables assuming those variables have the same type / binder type and associated type-classes, potentially by renaming the variable. Example:

variable {α β : Type _} [Add β]

def foo {γ : Type _} [Add γ] (x : γ) : γ := x + x
/- using the command gives:
def foo (x : β) : β := x + x
-/

(note: this can get trickier if you use type-classes that have more than 1 argument, like docs#Module)

I would love to use a "move definition" command that uses all of the above features!

[Filippo A. E. Nuccio]

I very much agree with the first and the third, while the second might be a bit trickier, because sometimes one really needs only one declaration and it is not worth it opening the namespace to avoid ambiguity.

[Denis Gorbachev]

@Floris van Doorn @Filippo A. E. Nuccio Thank you for suggestions - I've added new issues to the repo

[Scott Morrison]

We should not merge typescript code that is parsing Lean source to the vscode extension. This won't be maintainable; parsing needs to be done Lean natively.

[Julian Berman]

Is the plan really to merge new code actions to the VSCode extension? Rather than Std or somewhere else?

[Denis Gorbachev]

New command released: "Set argument style"

Demo

Before:

(α : Type u)

After:

{α : Type u}

Notes:

• The command supports four argument styles: explicit, implicit strong, implicit weak, typeclass ((), {}, ⦃⦄, []).

Extension links:

• Install
• Docs
• Report a bug
• Request a feature

[Denis Gorbachev]

Agreed, it's better to execute the code actions on the server, in the LSP file worker.

[Sebastian Ullrich]

Julian Berman said:

Is the plan really to merge new code actions to the VSCode extension? Rather than Std or somewhere else?

If they are implemented in Lean, they should of course go into a Lean package, yes

[Eric Wieser]

Denis Gorbachev said:

New command released: "Set argument style"

does this also change all the callers?

[Mario Carneiro]

These don't actually seem to be code actions though in the technical sense, these are extension commands

[Denis Gorbachev]

Julian Berman said:

Is the plan really to merge new code actions to the VSCode extension? Rather than Std or somewhere else?

Ideally, the extension should provide a frontend for the code actions, which should be executed on the server.

Whether to merge to core extension or not - see https://github.com/leanprover/vscode-lean4/issues/316

[Denis Gorbachev]

Eric Wieser said:

Denis Gorbachev said:

New command released: "Set argument style"

does this also change all the callers?

No, sorry - it simply changes the argument in the definition.

I agree this is suboptimal.

Who's interested in forming a Code Actions Working Group? Together, we could implement the proper code actions that handle all edge cases & work natively within the LSP server.

[Mario Carneiro]

At least the rename action seems to be relatively easy to implement in the server

[Mario Carneiro]

TBH it is unclear why it doesn't already exist

[Denis Gorbachev]

Mario Carneiro said:

At least the rename action seems to be relatively easy to implement in the server

Yeah, that would be great!

[Mario Carneiro]

I think the procedure would be to make a PR to the appropriate repository (lean core, std, or vscode-lean4), they each have their own contribution process

[Mario Carneiro]

a rename action would go in core

[Mario Carneiro]

auto-import too

[Mario Carneiro]

most actual code actions would go in std

[Denis Gorbachev]

P.S. The "final boss" is the "Move definition" command. There are lots of nuances related to namespace and open that should be handled when moving the definition from one file to another. Discussed here: https://github.com/DenisGorbachev/vscode-lean4-code-actions/issues/10

[Mario Carneiro]

and more involved text manipulation or things that need dropdowns / additional info would be in the extension

[Denis Gorbachev]

Agree

[Eric Wieser]

Denis Gorbachev said:

P.S. The "final boss" is the "Move definition" command.

This doesn't seem very valuable to me. Code actions are most useful when tens of files need to be changed in sync. Cut-and-pasting a single definition doesn't really meet that threshold.

[Mario Carneiro]

if it can actually solve those "final boss" issues it could be valuable

[Mario Carneiro]

but I'm not sure it's worth the effort

[Damiano Testa]

Eric Wieser said:

Denis Gorbachev said:

New command released: "Set argument style"

does this also change all the callers?

With respect to this, I've been using Bracketeer that has a key combination cycling through (), [], {} only. Even so, I find it incredibly useful, since I very rarely use strict implicits. So, if this code action improved on this, I would be very happy!

[Denis Gorbachev]

Eric Wieser said:

Denis Gorbachev said:

P.S. The "final boss" is the "Move definition" command.

This doesn't seem very valuable to me. Code actions are most useful when tens of files need to be changed in sync. Cut-and-pasting a single definition doesn't really meet that threshold.

What about moving the definition that is used in tens of other files? (we'll need to update the imports)

[Denis Gorbachev]

Damiano Testa said:

Eric Wieser said:

Denis Gorbachev said:

New command released: "Set argument style"

does this also change all the callers?

With respect to this, I've been using Bracketeer that has a key combination cycling through (), [], {} only. Even so, I find it incredibly useful, since I very rarely use strict implicits. So, if this code action improved on this, I would be very happy!

Ah snap, Bracketeer looks like a better solution! (it also has a "Remove brackets" action)

But you're right - it doesn't support weak implicit args.

[Denis Gorbachev]

(deleted)

[Mario Carneiro]

Mario Carneiro said:

At least the rename action seems to be relatively easy to implement in the server

TBH it is unclear why it doesn't already exist

I put up a rename implementation at lean4#2462

[Denis Gorbachev]

Thanks a lot Mario! I'll switch to your implementation as soon as it's merged

[Floris van Doorn]

Eric Wieser said:

This doesn't seem very valuable to me. Code actions are most useful when tens of files need to be changed in sync. Cut-and-pasting a single definition doesn't really meet that threshold.

Moving a lemma from a new file to an existing mathlib file is a huge pain IMO, since the lemma usually breaks after just copy-and-pasting: the target location has different namespaces open, different declared variable names, etc. In Lean 3 it was a big annoyance. Also, if you paste results to multiple different files, then in Lean 3 you'd have to recompile a large part of the library to see if there are any errors after copy-pasting, so I usually just sent it off to Github CI and hoped for the best.

Having a "copy-paste" function that doesn't create errors 99% of the time would be very nice.

[Denis Gorbachev]

New action: Update imports on file rename

Demo

Example:

If you rename Some/File.lean to Another/Name.lean, it will update import Some.File to import Another.Name in every file in the workspace.

Extension links:

• Install
• Docs
• Report a bug
• Request a feature