## Stream: lean4

### Topic: abbreviations in vscode

#### Mario Carneiro (Feb 12 2021 at 05:24):

I could have sworn this worked before, but right now I am not getting replacements on abbreviations like \alpha via the lean 4 vscode extension (leanprover.lean4 v0.0.5). It works fine if I enable the lean 3 extension instead, I've tried disabling other extensions and so on but no luck. I assume this works for others because lean 4 is pretty unwriteable without unicode abbreviations, since a lot of core syntax depends on it

#### Bryan Gin-ge Chen (Feb 12 2021 at 05:36):

It seems to have stopped working for me too (on macOS). Maybe there was something in the recent update of VS Code?

#### Bryan Gin-ge Chen (Feb 12 2021 at 06:46):

Hmm, if I open the VS Code settings tab and then go back to the editor tab, the input starts working again.

#### Bryan Gin-ge Chen (Feb 12 2021 at 06:49):

Actually, just switching back and forth between two file tabs seems to get it working again.

#### Eric Wieser (Feb 12 2021 at 08:50):

I've seen the same behavior in lean 3

#### Gabriel Ebner (Feb 12 2021 at 09:48):

I've just experienced the same issue as well. Thanks for the workaround!

#### Marc Huisinga (Feb 12 2021 at 10:25):

I'm running into the same issue now but the workaround does not seem to work. Huh.

#### Marc Huisinga (Feb 12 2021 at 11:41):

The problem is that this here returns false (I'm still investigating why, the languageId of the document is lean4 and it is in fact matching against lean4): https://github.com/leanprover-community/vscode-lean4/blob/master/src/abbreviation/rewriter/AbbreviationRewriterFeature.ts#L49
also, I believe that if condition three lines above should call .get() on the setting :)

#### Gabriel Ebner (Feb 12 2021 at 11:44):

My first guess is that right after opening a file, the id is still lean before the extension changes it to lean4.

#### Marc Huisinga (Feb 12 2021 at 11:46):

You're right, I was missled by the debugger showing me a later state.

#### Marc Huisinga (Feb 12 2021 at 11:52):

Adding an await to setLean4LanguageId makes it work :)

#### Gabriel Ebner (Feb 12 2021 at 12:06):

The fix is underway to a vscode near you!

#### Marc Huisinga (Feb 12 2021 at 12:08):

The new version will also have support for a simple (non-widget) goal view.

#### Eric Wieser (Feb 12 2021 at 12:56):

Is there an associated fix to the lean3 extension?

#### Marc Huisinga (Feb 12 2021 at 12:57):

The bug that this fixed was specific to vscode-lean4

#### Eric Wieser (Feb 12 2021 at 13:34):

Then I must be seeing a different bug with similar manifestation

#### Marc Huisinga (Feb 13 2021 at 11:17):

Eric Wieser said:

Then I must be seeing a different bug with similar manifestation

I can confirm that after fixing the above issue, abbreviations still sometimes stop working (in vscode-lean4). I'll take a look later.

#### Kevin Buzzard (Feb 14 2021 at 14:56):

Abbreviations have been really weird in Lean 3 recently, although I just spent a while playing around and couldn't reproduce. I'll look out for the issue.

#### Eric Wieser (Feb 14 2021 at 17:17):

This happens for me every time:

• New file, don't save it
• Set syntax lean (3). Type some ascii, goal view works fine
• Type \alpha. No substitution happens.
• Switch to another tab, switch back
• \alpha now works

#### Kevin Buzzard (Feb 14 2021 at 17:49):

I don't see this, it works fine for me (on Ubuntu). Note that I only use VS Code for Lean 3 so I don't know what "set syntax Lean (3)" means.

#### Eric Wieser (Feb 14 2021 at 17:52):

It means "I don't have lean 4 installed in any form"

#### Eric Wieser (Feb 14 2021 at 17:52):

But I'm on windows

#### Marc Huisinga (Feb 18 2021 at 18:55):

I didn't get to looking at the other issue yet, but I think I just ran into another issue with the new abbreviations. Specifically, I undo'd a bunch, looked at some older state of the file and then redo'd a bunch.
At some point during redoing, it stopped at some intermediate state next to an abbreviation I was typing in and eagerly completed the abbreviation (At least I think that's what happened?), which made me lose the rest of the redo history.
It stopped next to a "\n" that I was typing in via "\\n" and eagerly replaced that with "¬".

#### Eric Wieser (May 03 2021 at 10:07):

I've a partial fix to this problem in https://github.com/leanprover/vscode-lean/pull/263

Last updated: May 18 2021 at 23:14 UTC