propose removing module docstring code suggestion

Stream: mathlib4

[Kim Morrison]

I propose removing the module docstring code suggestion that Mathlib adds in https://github.com/leanprover-community/mathlib4/blob/nightly-testing-2024-04-21/.vscode/module-docstring.code-snippets?rgh-link-date=2024-04-22T14%3A09%3A02Z

It is nice, I guess, but I have had this trigger on do<enter> 100x times as often as it has been useful to me.

[Patrick Massot]

Do you know you can tell VSCode to not apply suggestions on enter? This is the first thing I set when I see a new VSCode, even before disabling the minimap.

[Kim Morrison]

I don't like setting any customisations, personally, so as to dog food the new user experience.

That prompts the question --- should we include "no suggestions on enter" in Mathlib's VSCode settings file?

[Kim Morrison]

(Further question -- should lake new create such a file??)

[Kevin Buzzard]

no suggestions on enter is also the first thing I do after getting Lean up and running on a new computer

[Patrick Massot]

Note that I don’t care about the module docstring snippet, I’m only astonished that anyone can use VSCode without setting this option in the first few minutes (and without having to buy a new computer per day because of rage destruction entailed by not setting this option).

[Kim Morrison]

It sounds like you are advocating for including this in Mathlib's .vscode/settings.json! :-)

[Kim Morrison]

#12749

[Kim Morrison]

What other things are you doing with Lean on a new computer that everyone should be sharing in? (I think we'll leave the minimap, I agree, but that feels like a personal choice.)

[Patrick Massot]

The mini map is a completely different kind of setting. I think it is useless and wastes space but it doesn't make VSCode unusable like accepting suggestions on enter.

[Kevin Buzzard]

The minimap is the only other global config change I make as well (probably out of habit more than anything else) (assuming autoImplicit etc is being done in my lakefile).

[Mario Carneiro]

I would like us to revert #12749. I wasn't sure about it at the time, but this is messing with my muscle memory and the choice to put it in .vscode/settings.json makes it impossible to disable locally AFAICT without hitting conflicts on this file

[Yaël Dillies]

I agree. It's really bad to my muscle memory as well

[Sébastien Gouëzel]

Please don't. It's definitely an improvement, and we will all be used to it in a few days.

[Mario Carneiro]

perhaps we should instead put it in the new user setup instructions

[Mario Carneiro]

this is a personal choice

[Mario Carneiro]

the people who advocated for it are AFAICT all people who had it on already beforehand

[Mario Carneiro]

If you like it and find it to be an improvement you can put it in your user settings. The converse doesn't work - putting this in the project settings means there is no opt out

[Frédéric Dupuis]

I just learned about this option now, and the default behavior has annoyed me for four years.

[Mario Carneiro]

I have no problem with having this be a default option. But that's not what .vscode/settings.json is

[Mario Carneiro]

(unless I missed something)

[Sébastien Gouëzel]

I didn't have it either, I didn't know the option, and it had been annoying me for years.

[Richard Osborn]

I would like it to stay off for the web editor if this affects it.

[Patrick Massot]

There is clearly a VSCode deficiency here, so we need a trade-off. And I think that making sure new (and not so new from what I read here) users get the sane behavior is clearly the right decision. Maybe there is something that can be done in the Lean extension but I guess this is pretty low priority.

[Arthur Paulino]

Wait, why is .vscode tracked by Git at all?

[Arthur Paulino]

Here's an idea: the Lean 4 extension can be responsible for adding a default .vscode/settings.json if that file doesn't exist yet. There can be a configuration to opt out of that so the extension does nothing.

Either way, .vscode is for local preferences and git tracking it will likely lead to diverse members committing to preferences they don't like. This should be a complete non-issue

Edit: what Patrick said

[Mario Carneiro]

Arthur Paulino said:

Either way, .vscode is for local preferences and git tracking it will likely lead to diverse members committing to preferences they don't like. This should be a complete non-issue

Right, this is my argument. .vscode/settings.json should only include project wide settings like line lengths, tabs/spaces, etc. There is a fundamental issue with storing any user preferences here which are not unanimously approved, which is that you can't override them. As long as they aren't mentioned in the file it's possible for people to pick their preference. I think it would be better to have a page for suggested preference options which people can copy into their user settings if they agree.

[Floris van Doorn]

I was not aware that these settings are not overrideable by individual users. That makes this issue more complicated. I would really like to make this the default behavior without any set-up from new users. Is there any way to do that while making it overridable?

[Floris van Doorn]

I just saw: https://code.visualstudio.com/docs/getstarted/settings#_settings-precedence
There seems to a long list of items that have a higher precedence than the workspace settings. Can you use Language-specific user settings to override the workspace setting?

[Brendan Seamas Murphy]

Thirding that it's bad to have this kind of setting be a project default period. I would go further and say it's strange to have .vscode/settings.json tracked at all! Things like 100 column lines or tab count can be caught by the linter or code review

[Brendan Seamas Murphy]

I'm finding this change very disruptive, I constantly use enter-autocomplete

[Mario Carneiro]

Things like 100 column lines or tab count can be caught by the linter or code review

well yes, we have linters and code review for that, but the reason they are in the settings is to catch the issues before they are PR'd

[Johan Commelin]

Floris van Doorn said:

I just saw: https://code.visualstudio.com/docs/getstarted/settings#_settings-precedence
There seems to a long list of items that have a higher precedence than the workspace settings. Can you use Language-specific user settings to override the workspace setting?

@Mario Carneiro @Brendan Seamas Murphy Does this :up: work?

[Filippo A. E. Nuccio]

Patrick Massot said:

There is clearly a VSCode deficiency here, so we need a trade-off. And I think that making sure new (and not so new from what I read here) users get the sane behavior is clearly the right decision. Maybe there is something that can be done in the Lean extension but I guess this is pretty low priority.

I disagree, expecially about the "clearly". Why can't we let everybody do what they prefer with their keyboard?

[Shreyas Srinivas]

Yes please. Pushing editor settings like this is highly intrusive. Every user has their own muscle memory and we tune our settings accordingly. Changing them can be jarring

[Filippo A. E. Nuccio]

Patrick Massot said:

Note that I don’t care about the module docstring snippet, I’m only astonished that anyone can use VSCode without setting this option in the first few minutes (and without having to buy a new computer per day because of rage destruction entailed by not setting this option).

@Patrick Massot I find your comment a bit hard. I am happy with the old option, and you are happy with the new one. It takes both of us 2 sec to set our VSCode as we prefer, and we would both be happy. In this way (or in the reverse one), one would be happy and the other would be sad. What are we gaining here?

[Kevin Buzzard]

I suspect Patrick's argument is that for beginners this is typically a bad option, so we want it off by default and then experts can turn it on. Unfortunately it seems that the method we used to do this is not good because experts are having trouble turning it on without making git upset.

[Filippo A. E. Nuccio]

The problem I see is that beginners might be lean beginners, but not VSCode beginners, so they might already be using VSCode with another setting. And using the same program with two different muscle memories according to what kind of work you are doing can be really painful. Imagine if your TeX shortcuts depended on whether you are typing an assessment or a research paper...

[Shanghe Chen]

Hi I came across from here. Yeah VSCode's auto suggest is not very intelligent and sometimes suffers from performance issues. But turning it on can make typing long variable names and lemmas some kind easier, and avoid some typos I think. A way to customize this may be per user per workspace config in vscode, but sadly it seems still not supported yet vscode#15909

[Patrick Massot]

I agree that VSCode has a really serious issue here, and there does not seem to be a nice solution. So this change should probably be reverted after making sure that the Lean extension displays a very clear message when it installs, hopefully even a button to set sane defaults for the user. Something like: we will now update your VSCode settings to make it usable, please check this box if you do not want this.

[Filippo A. E. Nuccio]

Yes, this seems to be a very reasonable way to go.

[Patrick Massot]

And I’ll be very curious to see someone using VSCode without being allowed to use the Enter key. What is the workflow? Did you train your muscles to hit Escape and then Enter every time you want a new line?

[Filippo A. E. Nuccio]

But wouldn't this take a while to be implemented?

[Filippo A. E. Nuccio]

Patrick Massot said:

And I’ll be very curious to see someone using VSCode without being allowed to use the Enter key. What is the workflow? Did you train your muscles to hit Escape and then Enter every time you want a new line?

Yes, whenever I have a suggestion, I type esc+enter; if there is no suggestion, enter alone works.

[Patrick Massot]

I don’t think it would take a while. @Marc Huisinga is really really good at VSCode extension writing now.

[Patrick Massot]

Remember that many users actually look at their keyboard when typing, so they would have to use Esc-Enter everytime. And also the suggestion can popup a fraction of seconds before you hit enter.

[Filippo A. E. Nuccio]

I see, and I can even go as far as agreeing with you that one might want to suggest not to do this; but imposing it seems a bit too much, especially for users who might have developed this habit either from a long time or from a different language.

[Patrick Massot]

I understand. When Kim pushed that commit I did not realize this was impossible to override by users. Again this is a very weird decision from VSCode to make it impossible to have project default settings.

[Ruben Van de Velde]

My brain agrees that enter isn't great, but my fingers don't :(

[Shanghe Chen]

Patrick Massot 发言道：

And I’ll be very curious to see someone using VSCode without being allowed to use the Enter key. What is the workflow? Did you train your muscles to hit Escape and then Enter every time you want a new line?

Oh for me I am using the vscodevim extension and hence I hit esc all the times.

[Patrick Massot]

Do you hit esc to create a new line while typing?

[Shanghe Chen]

Nope I find that mainly I am using vim's shortkeys for creating new line, first pressing esc to normal mode, and then pressing o... And my esc/ctrl is bound to the capslock: tapping capslock for esc and holding capslock and in the same time for ctrl (maybe this is quite personal though...) Yeah without this the enter/esc issue may be annoying...

[Kevin Buzzard]

Just to remind people in this thread of Eric's comment above saying that it would be better not to revert the commit which made the change (because that commit did other things too) and just make a new commit which undid the specific change which has upset the esc-lovers amongst us. (edit: this is nonsense)

[Johan Commelin]

Johan Commelin said:

Floris van Doorn said:

I just saw: https://code.visualstudio.com/docs/getstarted/settings#_settings-precedence
There seems to a long list of items that have a higher precedence than the workspace settings. Can you use Language-specific user settings to override the workspace setting?

Mario Carneiro Brendan Seamas Murphy Does this :up: work?

Did anybody test this?

[Marc Huisinga]

Patrick Massot said:

I agree that VSCode has a really serious issue here, and there does not seem to be a nice solution. So this change should probably be reverted after making sure that the Lean extension displays a very clear message when it installs, hopefully even a button to set sane defaults for the user. Something like: we will now update your VSCode settings to make it usable, please check this box if you do not want this.

I generally don't consider these kinds of one-off notifications to be a good idea. The manual will mention this setting, but I also don't think that all users are as bothered by the default behavior as you are.

To me, the main culprit here was the module docstring suggestion that got in the way whenever you were just about to press Enter.

Johan Commelin said:

Johan Commelin said:

Floris van Doorn said:

I just saw: https://code.visualstudio.com/docs/getstarted/settings#_settings-precedence
There seems to a long list of items that have a higher precedence than the workspace settings. Can you use Language-specific user settings to override the workspace setting?

Mario Carneiro Brendan Seamas Murphy Does this :up: work?

Did anybody test this?

It probably does, but I still don't think that it's a good idea to mess with user settings in a way that is difficult to opt-out of.

[Eric Wieser]

Kevin Buzzard said:

Just to remind people in this thread of Eric's comment above saying that it would be better not to revert the commit which made the change (because that commit did other things too) and just make a new commit which undid the specific change which has upset the esc-lovers amongst us.

Which comment? (Or maybe, which Eric?)

[Eric Wieser]

Patrick Massot said:

Did you train your muscles to hit Escape and then Enter every time you want a new line?

I hit Ctrl+Z if I trigger a suggestion by accident

[Kevin Buzzard]

Sorry Eric, I must have conflated this with another issue. Clearly the PR just makes the one change and can be reverted if necessary

[Kevin Buzzard]

I claim that at some point recently you said "don't revert the PR, it does several other things too" and I assumed we were talking about this one

[Eric Wieser]

Marc Huisinga said:

To me, the main culprit here was the module docstring suggestion that got in the way whenever you were just about to press Enter.

Can we fix this by adding a snippet for do? Or by having the language server offer it as a keyword completion?

[Filippo A. E. Nuccio]

All in al, is it OK if I open a PR reverting this change? @Kim Morrison @Patrick Massot ?

[Kim Morrison]

I mean, I'm personally opposed to reverting because it is so disruptive to have enter keep pasting in nonsense in my file, and I would like to save others from this experience, but by all means open a PR. :-)

[Kim Morrison]

Also -- if we decide that this is something that needs to be voted on, we have to make sure that we properly sample from beginners, rather than from loud people on zulip. :-)

[Filippo A. E. Nuccio]

Kim Morrison said:

Also -- if we decide that this is something that needs to be voted on, we have to make sure that we properly sample from beginners, rather than from loud people on zulip. :-)

Yes, this I very much agree with. What I find somewhat unbalanced is that by reverting every user will be entitled to set up VSCode as they wish, whereas as it is now we are all obliged to follow a common rule

[Kim Morrison]

Whereas I would spin it as: where we are now, beginners (who would obviously never touch the default settings) get a usable experience, whereas if we revert experts can avoid changing their habits. :-)

[Marc Huisinga]

Eric Wieser said:

Marc Huisinga said:

To me, the main culprit here was the module docstring suggestion that got in the way whenever you were just about to press Enter.

Can we fix this by adding a snippet for do? Or by having the language server offer it as a keyword completion?

The keyword completion approach with keyword snippets being at the top of the list would be my preferred solution for #3623, but it's difficult to do right now due to how the completion mechanism works at the moment. I want to eventually rework it in the future.

Adding a couple of built-in keyword snippets for keywords that are typically used to terminate lines in Mathlib would definitely be worth an experiment.

[Filippo A. E. Nuccio]

Kim Morrison said:

Whereas I would spin it as: where we are now, beginners (who would obviously never touch the default settings) get a usable experience, whereas if we revert experts can avoid changing their habits. :-)

I see, on the other hand there might very well be experienced VSCode users who are new to mathlib and are used to that setting. This would mean that they have to use VSCode depending on what they are coding....

[Filippo A. E. Nuccio]

Moreover, it seems to me that it should be important to keep things pertaining to mathlib (eg. the 100 characters limit, which is a library thing) from users' experience: they are unrelated, no?

[Marc Huisinga]

Kim Morrison said:

Whereas I would spin it as: where we are now, beginners (who would obviously never touch the default settings) get a usable experience, whereas if we revert experts can avoid changing their habits. :-)

By the way, I'm very skeptical of this claim. In my mind, with the default setting off, a total beginner who is not used to IDEs will see the completion popup panel, try to select an entry with the arrow keys and Enter because that's the universal button to make progress in user interfaces, see that it doesn't work and then fall back to selecting entries by taking the hands off the keyboard and using the mouse.
I don't think that Tab is at all an intuitive shortcut for beginners, and I suspect that this is probably why most IDEs use Enter for completions, despite the fact that it sometimes gets in the way.

[Mario Carneiro]

:this: I have witnessed this before

[Kim Morrison]

Okay, I can see that I am outvoted here. If we can separately fix the do<enter> issue I will be completely happy.

[Andrew Yang]

Does adding a snippet that triggers on do that pastes do work?

[Mario Carneiro]

As I said, I think we should have a page for suggested settings, and the extension can even guide people to it. I don't think it should change settings just by installing it though, I know a lot of people (on the "linux power-user" side of the spectrum) who find that kind of behavior to be distasteful

[Mario Carneiro]

having keyword completions in general would help I think

[Kim Morrison]

I want a solution that ensures that the vanilla install of the VSCode extension allows you to type do<enter>.

[Mario Carneiro]

what even causes the autocomplete to trigger in this example?

[Mario Carneiro]

I just tried typing def foo := do<enter> and no autocomplete was triggered

[Andrew Yang]

I think it was changed to "module docstring" instead of "docstring"?

[Mario Carneiro]

that doesn't help, it still has d and o in that order

[Kim Morrison]

oh, but enter no longer selects it!

[Kim Morrison]

module docstring appears in the dropdown, but perhaps enter only works if you're typing a prefix?

[Kim Morrison]

So maybe problem solved at this point. (after we revert)

[Mario Carneiro]

my understanding was that autocomplete only auto-triggers on things like .

[Mario Carneiro]

if you manually trigger autocomplete I think it's fine if <enter> selects the result

[Mario Carneiro]

it's only the auto-autocomplete that is disruptive for people just typing with their eyes off the screen

[Kim Morrison]

No, with what I think I default settings, typing def foo := do<enter> gives me:

def foo := /-!
# CategoryTheory

## Main definitions

* `FooBar`

## Main statements

* `fooBar_unique`

## Notation



## Implementation details



## References

* [F. Bar, *Quuxes*][bibkey]

## Tags

Foobars, barfoos
-/

[Kim Morrison]

(requires a slight pause before the <enter>)

[Mario Carneiro]

did you test that? I can't replicate (I haven't changed things from the mathlib current default but that should only affect the selection key), no popup appears

[Kim Morrison]

Yes, just did it several times.

[Mario Carneiro]

what character causes the popup?

[Kim Morrison]

As soon as I type the d a pop-up appears, once I type o "module docstring" is at the top of the list, and then enter pastes a screen full of garbage...

[Mario Carneiro]

aha, I think this is the reason I'm not seeing those popups

  "editor.quickSuggestions": {
    "comments": "off",
    "strings": "off",
    "other": "off"
  },

maybe we should put this in the suggestions...

[Kim Morrison]

Suggestions won't solve anything for most people?

[Kim Morrison]

(I don't set any custom settings specifically to make sure I'm not hiding bad experiences for new users.)

[Mario Carneiro]

Is it possible to have language-specific default settings for lean4 lang?

[Andrew Yang]

Andrew Yang said:

Does adding a snippet that triggers on do that pastes do work?

Does changing the start of module-docstring.code-snippets to the following work? (It works for me)

{
    "Do notation": {
        "scope": "lean4",
        "prefix": "do",
        "body": ["do"]
    },
    "Module docstring for mathlib": {

[Michael Rothgang]

Marc Huisinga said:

Kim Morrison said:

Whereas I would spin it as: where we are now, beginners (who would obviously never touch the default settings) get a usable experience, whereas if we revert experts can avoid changing their habits. :-)

By the way, I'm very skeptical of this claim. In my mind, with the default setting off, a total beginner who is not used to IDEs will see the completion popup panel, try to select an entry with the arrow keys and Enter because that's the universal button to make progress in user interfaces, see that it doesn't work and then fall back to selecting entries by taking the hands off the keyboard and using the mouse.
I don't think that Tab is at all an intuitive shortcut for beginners, and I suspect that this is probably why most IDEs use Enter for completions, despite the fact that it sometimes gets in the way.

I just encountered this exact problem last week (trying to use enter for suggestions - with Mario sitting next to me and telling me to use tab). I can re-train my brain, but let me state that I found this behaviour surprising.
(I don't use suggestions much so far, so at the moment I don't have a horse in this race.)

[Marc Huisinga]

Mario Carneiro said:

Is it possible to have language-specific default settings for lean4 lang?

Yes this is possible, but note that this would disable all automatic identifier completions and (outside of dot completion) users would always have to use Ctrl+Space to trigger completion.

[Filippo A. E. Nuccio]

What I find surprising is mixing user settings with library settings. Even if we fix this very problem at hand, I would like that in a year time we don't find that setting a dark theme, for instance, is graved in stone in the json "since it is better for your eyes". It is very fine to propose suggestions, but there are things that should be free even for new users, who are adults (or almost...), after all.

[Mario Carneiro]

I don't remember setting this setting but I guess I must have found it unhelpful, at least with the state of identifier completion at the time (it's really slow, so having it automatically pop up too late is kind of the worst possible situation)

[Marc Huisinga]

Mario Carneiro said:

I don't remember setting this setting but I guess I must have found it unhelpful, at least with the state of identifier completion at the time (it's really slow, so having it automatically pop up too late is kind of the worst possible situation)

I made it a bit faster a while ago.

[Johan Commelin]

@Filippo A. E. Nuccio It is still possible to override these settings as a user, right? Floris pointed to docs on how to do this.

[Johan Commelin]

In general, I don't care too much where this lands. Exactly because people can still customize however they want.

I think I lean slightly towards the Massot-Morrison camp in this debate.

[Johan Commelin]

Certainly, if it wasn't possible to override this setting, then I would think it is a bad move. But expert VScode users can do whatever they want... so I don't see why this is a big deal.

[Filippo A. E. Nuccio]

Johan Commelin said:

Filippo A. E. Nuccio It is still possible to override these settings as a user, right? Floris pointed to docs on how to do this.

Do you mean the list https://code.visualstudio.com/docs/getstarted/settings#_settings-precedence? This would need to be at any rate inserted in the json, right?

[Filippo A. E. Nuccio]

At any rate my point would rather be to avoid interfering with users' setting in the mathlib json, the two things look unrelated.

[Johan Commelin]

Filippo A. E. Nuccio said:

Johan Commelin said:

Filippo A. E. Nuccio It is still possible to override these settings as a user, right? Floris pointed to docs on how to do this.

Do you mean the list https://code.visualstudio.com/docs/getstarted/settings#_settings-precedence? This would need to be at any rate inserted in the json, right?

Yes... but all VScode settings are handled by json, so I don't see why this is a problem

[Filippo A. E. Nuccio]

Ah, I probably understand Floris' suggestion better: to specify as user-specific language setting the behaviour of enter, that will override global workspace settings.

[Johan Commelin]

Yes. Users can always override any "community setting".

[Filippo A. E. Nuccio]

This might fix locally, but I insist with my idea that the json contained in the mathlib library should not mess up with users' settings concerning VSCode experience.

[Mario Carneiro]

I still think this would be better as a language-specific default rather than a mathlib-specific workspace setting. Currently, the new user experience is that <enter> accepts autocomplete in other languages and in lean projects other than mathlib, but in mathlib this doesn't work, and this is not good for people who switch between mathlib and other (lean) projects.

[Johan Commelin]

That seems sensible to me.

[Filippo A. E. Nuccio]

But this would break Floris' workaround, as language-specific workspace settings overridd user's ones and are at the top of the priority list...

[Mario Carneiro]

no, the list is read the other way around, high priority is at the bottom

[Filippo A. E. Nuccio]

Yes, I agree and Language-specific workspace settings is almost at the end.

[Mario Carneiro]

but it does mean that the user would have to edit these settings as language-specific, i.e. in "[lean4]": { ... }

[Marc Huisinga]

Mario Carneiro said:

I still think this would be better as a language-specific default rather than a mathlib-specific workspace setting. Currently, the new user experience is that <enter> accepts autocomplete in other languages and in lean projects other than mathlib, but in mathlib this doesn't work, and this is not good for people who switch between mathlib and other (lean) projects.

I won't disable 'Enter' as a shortcut to accept completions globally for all Lean users, and I'm not interested in globally removing regular completions from auto-triggering at this point.

To override a language default that is provided by the VS Code extension, users need to know:

• That there is a precedence of settings, and what that precedence is
• That the Lean 4 VS Code extension is meddling with their regular user settings
• That there is a notion of a language user setting distinct from regular user settings that can override the language default setting
• How to set the language user setting, either by using special syntax in the (nowadays for most users obscure) settings.json, or by using the tiny "Filter settings" button in the settings UI that actually doesn't filter but switches the settings editor into an entirely different language-specific mode (I had to look this up because I couldn't find it in the UI myself)

I don't consider this to be a reasonable UX to provide to users.

[Mario Carneiro]

(To be clear I meant it would be better than having mathlib alone do it. I would prefer it's not done at all)

[Filippo A. E. Nuccio]

@Mario Carneiro Just to be sure, do you prefer to set it as Language-defult setting (that is overridden by User language-specific setting) or as Workspace language-specific setting, which is not?

[Marc Huisinga]

My specific suggestion for mathlib would be to change the prefix of the module docstring snippet, or to try out adding additional keyword snippets that do the right thing when pressing Enter.

[Mario Carneiro]

Filippo A. E. Nuccio said:

Mario Carneiro Just to be sure, do you prefer to set it as Language-defult setting (that is overridden by User language-specific setting) or as Workspace language-specific setting, which is not?

A workspace language-specific setting would be like mathlib adding a "[lean4]": { ... } block in the settings.json file. There is no need for this since mathlib is basically all lean code anyway, and it would make the problem here even worse, so no I'm not suggesting that.

[Arthur Paulino]

I just want to reiterate that whichever solution involves git tracking local/personal preferences for any software, VS Code clearly included, can't possibly be on the right path.

Even a Lake script that just spits out those (ideally gitignored) settings would be a better solution IMO. There goes a lake run vscode_settings

[Kim Morrison]

Andrew Yang said:

Andrew Yang said:

Does adding a snippet that triggers on do that pastes do work?

Does changing the start of module-docstring.code-snippets to the following work? (It works for me)

{
    "Do notation": {
        "scope": "lean4",
        "prefix": "do",
        "body": ["do"]
    },
    "Module docstring for mathlib": {

Can someone PR this? It seems like a fine solution.

[Andrew Yang]

Kim Morrison said:

Can someone PR this? It seems like a fine solution.

#13163

[Kim Morrison]

Any objections?

[Eric Wieser]

Does it work? I'd be slightly worried that you would have to write do\n\n to get do\n

[Mauricio Collares]

Arthur Paulino said:

I just want to reiterate that whichever solution involves git tracking local/personal preferences for any software, VS Code clearly included, can't possibly be on the right path.

Even a Lake script that just spits out those (ideally gitignored) settings would be a better solution IMO. There goes a lake run vscode_settings

In emacs, you can have project preferences in (git-tracked) .dir-locals.el and overrides in a separate (non-git-tracked) .dir-locals-2.el in the same directory. Project preferences are fine, VS Code just didn't think this through very well.

[Kim Morrison]

Eric Wieser said:

Does it work? I'd be slightly worried that you would have to write do\n\n to get do\n

Works for me! Just one enter, which does select from the drop down, but seems to give the same net experience as if the drop down weren't there.

[Arthur Paulino]

@Mauricio Collares There are project preferences (like spaces vs tabs) and interaction preferences, let me call them that way (like how you choose to interact with the LSP, your shortcuts etc). One kind of settings results in concretely different files, and the other is just about how you interact with your coding tool. So while your points are valid to attest that emacs is superior in this aspect, the analogy doesn't fit 100%

[Mauricio Collares]

I see your point, sorry for not getting it at first. I guess Mathlib blurs this distinction a bit because the "stereotypical Mathlib user" is a mathematician that doesn't use VS Code for anything else.

[Richard Osborn]

Can we please have live.lean-lang.org NOT use Enter for completions? I find it silly to expect someone to type Esc, Enter to type a newline. I understand using Enter for completions is fine in many languages, but it's totally unpredictable when lean's language server will suggest completions.

[Marc Huisinga]

Richard Osborn said:

Can we please have live.lean-lang.org NOT use Enter for completions? I find it silly to expect someone to type Esc, Enter to type a newline. I understand using Enter for completions is fine in many languages, but it's totally unpredictable when lean's language server will suggest completions.

Other languages offer completions in a very similar manner to the Lean language server, so I'm not sure what you're getting at here. For example, when I enter a W in a Typescript file and wait for a moment, it offers me all identifiers starting with W.

[Kim Morrison]

It seems Richard is in the Massot-Morrison camp, also staring across of gulf of mutual incomprehension at how <enter> is meant to work. :-)

[Richard Osborn]

Typescript has ; delimited expressions. This means the autocompletion will never trigger when you want to type a newline. Lean doesn't have a syntax which allows for this separation.
Personally, I don't care about the .vscode file, but making live.lean-lang.org hard to use seems counterproductive.

[Eric Wieser]

Is there an upstream tracking issue in vscode? If the behavior is truly incomprehensible to some of us, it seems like this should be raised upstream

[Marc Huisinga]

Richard Osborn said:

Typescript has ; delimited expressions. This means the autocompletion will never trigger when you want to type a newline. Lean doesn't have a syntax which allows for this separation.
Personally, I don't care about the .vscode file, but making live.lean-lang.org hard to use seems counterproductive.

Huh? My Typescript files certainly don't contain any semicolons. My pretty-printer ensures that those get removed, and this is true for many Typescript projects.

It's true however that most languages (including Typescript) have keyword completions or keyword snippets at the top of the completion list, and we have already established that this would be the desired solution for this issue.

[Marc Huisinga]

but making live.lean-lang.org hard to use seems counterproductive

As you can see in this very thread, I don't think it is at all established that exclusively using Tab for completions will make the web editor easier to use, so I find this claim confusing. People who have used a regular IDE in the past will be confused because it does not match their muscle memory and absolute beginners will be confused as well because they don't know what key to use to accept completions.

[Richard Osborn]

Personally, I believe you should be able to type what you want without having to visually parse what the editor is doing. That isn't the case if lean uses Enter for completions. Plenty of programming languages are designed syntactically so that autocompletions won't trigger when you want to type a newline. Lean isn't one of those languages.

[Damiano Testa]

I am a little embarrassed to confess that, until I read this thread, I did not know that Tab would have done what I got used to do with Enter. This makes the change slightly less troublesome for me: in the meantime, I have been living with a modified, Git-tracked settings.json file and trying not to commit it in my PRs...

[Shreyas Srinivas]

I don't remember the last time I used <enter> to start a newline

[Joachim Breitner]

I
do

[Ruben Van de Velde]

Wait, what do you use?

[Shreyas Srinivas]

Word wrap

[Kim Morrison]

In code? This is just a silly claim, sorry.

[Shreyas Srinivas]

In code

[Shreyas Srinivas]

I have been writing programs for 10 years now, and at least since I used sublime and atom, the word wrap has been doing a perfectly fine job

[Richard Osborn]

We're talking about VSCode

[Shreyas Srinivas]

In vscode, it is better, especially with code formatting tools

[Richard Osborn]

Lean doesn't have a code formatter. This is an unproductive tangent.

[Shreyas Srinivas]

The point is most newcomers who have used a recent text editor are not used to hitting enter at every line.

[Shreyas Srinivas]

Maybe when formatting code or using some languages like haskell.

[Ruben Van de Velde]

Anyway, I'm not sure this is the most productive direction for the conversion :)

[Shreyas Srinivas]

Okay, maybe I subconsciously use enter without thinking, but for many people accustomed to modern editors and IDEs, we are also conscious about not hitting <enter> if we don't want an autocompletion. Unlike some users here, I use <space> + <backspace> in quick succession.

[Richard Osborn]

Right. Needing silly workarounds to just type Enter is exactly the problem. Again, I realize plenty of languages don't have this problem, but lean certainly does.

[Richard Osborn]

What makes it worse, is that you essentially have to type Esc, Enter or some other keyboard incantation every time or wait a second at the end of each line to check if autocompletion has something to say.

[Shreyas Srinivas]

That being said, if you have been using editors for sometime, there are quite a few such workarounds that are muscle memory. Ctrl + Z, Alt + Z, Esc, Ctrl + ~, Ctrl + S, etc, so this is not unique to lean. As a long time vscode user, when there is an autocompletion menu and I can't hit enter to use it, I am going to find that a stumbling block. I am not exactly an expert as far as lean is concerned (far from it), so I would say this is definitely not an experts vs beginners issue.

[Shreyas Srinivas]

I think leaving it to users with an option makes sense, both for the extension and the web editor (for which the option could be persisted with a cookie).

[Patrick Massot]

This conversation makes me really sad. I wish half the energy spent defending VSCode’s crazy UX could be spent on improving Lean support in actual editors like emacs or vi.

[Filippo A. E. Nuccio]

Since I was somewhat part if this conversation, let me stress that I am not personally defending VSCode UX, I was simply advocating for everyone being free to chose what they want.

[Patrick Massot]

Filippo, I think you typed your answer while I was editing my message.

[Patrick Massot]

I edited it because I realized it was not saying what I wanted to say.

[Filippo A. E. Nuccio]

Patrick Massot said:

Filippo, I think you typed your answer while I was editing my message.

True, and I apologize. Let me modify my message accordingly.

[Patrick Massot]

No need to apologize, it’s my mistake.

[Richard Osborn]

If the web editor can be changed to allow people to choose their preference and have that persist, then great. Until then, I believe it should turn off Enter for autocomplete (and realistically it should be the default for new users too). I do have sympathy for those who learned to code in VSCode with its impractical defaults, but it would be nice if we didn't indoctrinate new users with bad habits.

[Shreyas Srinivas]

Firstly, I don't think there is any consensus that this is a bad VSCode default. UX preferences can be highly personal choices. Secondly, the best person to answer questions about the web editor might be @Jon Eugster.

[Jon Eugster]

sorry, this is a long thread and I've only skimmed it. Here are the available editor options: monaco editor options, and they are set here for lean4web. What's the name of the option to disable Enter as accepting suggestions?

[Jon Eugster]

ah acceptSuggestionOnEnter

[Shreyas Srinivas]

@Jon Eugster : I would suggest request making it a configurable persistent option.

[Jon Eugster]

295261 and 1ed09c should turn acceptSuggestionOnEnter off by default and add an option to turn it on in the settings.

If you have other suggestions how the default experience should be, I'm very open to tweak any of the settings from the link above.

(I'll read the entire thread later to see people's opinions, but I feel having it turned off by default is the more natural choice, especially because on a mobile, it's almost impossible to type otherwise)

[Mitchell Lee]

If we're going to prevent do from autocompleting to module docstring, can we also prevent by from autocompleting to Bornology?

[Mitchell Lee]

Or Asymptotics.IsBigO.trans_eventuallyEq or whatever it is nowadays

[Yaël Dillies]

Patrick Massot said:

Do you hit esc to create a new line while typing?

Do you hit Ctrl + Z on every single one-letter word you type? That's a genuine question: Since tab is also used for moving inside code snippets, I find myself having my \left(\frac kn\right) (almost silently) turned into \left(\frac kN\right) because vscode decided to "autocomplete" n to N.

[Patrick Massot]

Why would you type that in VSCode? It looks like TeX code.

[Eric Wieser]

I'm looking really hard and those two strings are the same; is that a typo, or am I blind?

[Kevin Buzzard]

I was working under the assumption that the second one should be frac kN

[Brendan Seamas Murphy]

Patrick Massot said:

Why would you type that in VSCode? It looks like TeX code.

I use VSCode as my editor for writing TeX, maybe Yaël does too?

[Eric Wieser]

(for what it's worth, lean turns \frac into ¼...)

[Yaël Dillies]

Yep, Brendan is exactly right

[Filippo A. E. Nuccio]

Yaël Dillies said:

Yep, Brendan is exactly right

Me too, when especially when I want a smooth git interaction

[Ruben Van de Velde]

It took a while, but I'm getting used to <tab> for autocompletion

[Damiano Testa]

Same for me, actually.

[Eric Wieser]

Andrew Yang said:

Kim Morrison said:

Can someone PR this? It seems like a fine solution.

#13163

Does this change mean we can now revert #12749? Anyone who has adjusted their muscle memory can always turn the setting on globally in vscode, but it sounds like the main painpoint of the original behavior has been addressed.

[Robert Maxton]

I both greatly dislike the setting itself (touch typing is a vital skill, if we're going to unilaterally impose learning new skills on users then typing 'esc-enter' is a much better skill to impose) and also the idea that mathlib should even be making decisions like this. "New" users who discover Lean don't seem likely to me to be new to typing or even coding in general, so they will have their own habits and preferences and there is no need to interfere with them.

[Robert Maxton]

In general I rarely "write code" in any language in the way I speak English; I navigate auto-suggestions and auto-completes and use what completions are available as a continuous tracker that what I am doing is sane, and if the method I'm looking for doesn't show up as a suggestion that is usually a sign that I'm not working with the type I think I am.

To me much of the point of an IDE is letting me work on the token or keyword level, within the logic of the language, rather than the level of individual letters and through the logic of the interface.

[Kim Morrison]

I think the only problem here is no one making the PR.

[Shreyas Srinivas]

I am using the online editor right now and it is becoming painful everytime I get an autocomplete suggestion and pressing <Enter> inserts a newline instead of inserting the suggestion.

[Eric Wieser]

@Shreyas Srinivas, you can change the options in the web editor