VSCode completion on brackets

Stream: lean4

[Jakob von Raumer]

VSCode now proposes me to auto-complete b) to Mathlib.Notation3.«termExpand_binders%(_=>_)_,_» :exhausted: and similar for other characters followed by a closing bracket. That's especially annoying because there's lots of places where I'd like to have a line break after a closing bracket and always accidentally tricker the replacement. Is anyone else experiencing this?

[Marc Huisinga]

Mathlib users probably don't encounter this issue because it sets the auto-completion button to be Tab instead of Enter.

This particular issue is probably due to the language server telling VS Code that the completion lists we give it are complete to minimize latency, and so VS Code doesn't re-request the completion list when you type ), and instead filters the previous completion list by b). I.e. the Mathlib.Notation3.«termExpand_binders%(_=>_)_,_» completion was likely already there before, and now VS Code just continues displaying it when you type ).

I'm a bit surprised that VS Code doesn't respect the word boundary tokens that we set for Lean here, though. I would have imagined that when it encounters a character that isn't part of a word, it will re-request the completions, but apparently it doesn't.

I'll have to think about this one for a bit :sweat_smile:

[Jakob von Raumer]

Ahh, setting it to Tab will actually be good enough for me, I'll hardly press Tab after a closing bracket :grinning_face_with_smiling_eyes:

[Marc Huisinga]

I'm still not entirely happy with that solution though, since it's quite difficult for people to figure out that Tab triggers auto-completion.

I do have a solution for the similar keyword completion issue (e.g. you type do and just as you want to press Enter, the completion menu pops up and you trigger the do completion instead) in mind that I'd like to implement in the future, but I'm not sure about this example yet.

[Marc Huisinga]

Tracked at lean4#8430.

[Kevin Buzzard]

There is a VS Code setting to get you out of this "enter randomly autocompletes in Lean files" hell and I always have to ask @Patrick Massot what it is (sorry to ping you twice today Patrick -- I just scrolled back through years of our messages but my search is too weak to find the DM when you told me how to switch it off in 2021 or so)

[Marc Huisinga]

@Kevin Buzzard You might find the section on auto-completion in the VS Code extension manual helpful: https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/manual/manual.md#auto-completion

[Patrick Massot]

Yes, the VSCode extension manual says it:

This behavior can be disabled by setting the 'Accept Suggestion On Enter' configuration option to 'off'.