VSCode autocompleting `by` to `by_contra`

Stream: new members

[Bbbbbbbbba]

Does anyone else run into the problem where VSCode is too eager to autocomplete by to by_contra? Is there a way to fix this?

[Jakub Nowak]

I also ran into this problem. I usually just use neovim which doesn't have this problem. Maybe it's possible to configure VSCode to disable autocompletion on clicking "Enter" and only autocomplete on "Tab" (or "Ctrl+Y" like in neovim :P).

[Weiyi Wang]

Maybe it's possible to configure VSCode to disable autocompletion on clicking "Enter" and only autocomplete on "Tab" (or "Ctrl+Y" like in neovim :P).

Yes, I found this in vscode settings after complaining the same thing somewhere

[Shreyas Srinivas]

It is possible. But that is different from the underlying issue that vscode's first suggestion isn't by itself which would fix the issue. This is a recent problem

[Jakub Nowak]

Hm, is completion in VSCode smart enough to know that when I write e.g. let abc<cursor here> it knows that it shouldn't try to autocomplete abc (because it's a new identifier)?

[Snir Broshi]

The completion collects suggestions from multiple sources, one of which is the LSP, and I think Lean is smart enough to know it isn't defined yet. But then there's also suggestions of existing words in the document, which will suggest abc, but it should be low in the list.

[Snir Broshi]

This is what I usually get:

image.png

The "abc" logo next to them means they're just words collected from open documents and not from the LSP

[Snir Broshi]

The solution is to have the LSP always suggest all of Lean's keywords, then they should beat these suggestions

[Robin Arnez]

There is also the VS code option "Editor: Word Based Suggestions" that you can disable if you just don't want the "abc" suggestions

[Jakub Nowak]

We could make it smarter than just suggesting all possible keywords. It could only suggest keywords that make sense at where the cursor is. So in definition, after :=, that would be only keywords that are the beginning of some `term syntax.

[Snir Broshi]

idk how to check which keywords make sense at a point, so adding all of them seems like a good start

[Snir Broshi]

I think this is the function that suggests completion items

[Jakub Nowak]

Regardless, disabling autocompletion on Enter seems like a good idea. But maybe I'm biased because of what I'm used to.

[Shreyas Srinivas]

This was actually discussed on the mathlib channel where for a while mathlib forced this setting on you. The conclusion was that everybody has their own muscle memory and one person's preferences can't be forced onto another

[Shreyas Srinivas]

I have used autocomplete on enter for a long time and until the last 3-4 months it was perfectly fine. The issue is definitely some change in the way autocomplete lists suggestions (including not listing by itself when it is a perfectly valid token.

[Snir Broshi]

I believe no one would be opposed to autocompleting keywords

[Snir Broshi]

But I'm not sure how to get a list of all the keywords using meta code (without hardcoding them)

[Jakub Nowak]

I am a bit opposed, fearing it might clutter autocompletion window.

[Snir Broshi]

It would always be below everything else other than the word suggestions, what do you fear it cluttering specifically?

[Jakub Nowak]

But I would need to see an implementation to have an opinion. If we can have keywords listed below other suggestions, but above text suggestions (what vscode calls "abc"), then I think I'm fine.

[Jakub Nowak]

image.png
I do get keyword suggestions in neovim though.
Although, by_contra is listed first anyway. xd

[Marc Huisinga]

Completing b in VS Code will also yield keyword completions in VS Code. The problem with triggering auto-completion on by is that we don't have a CompletionInfo for keywords (and in fact we may actually want to complete it as an identifier instead). Could you open a bug report in core?