abbreviations in vscode

Stream: lean4

[Mario Carneiro]

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]

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]

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]

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

[Eric Wieser]

I've seen the same behavior in lean 3

[Gabriel Ebner]

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

[Marc Huisinga]

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

[Marc Huisinga]

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]

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

[Marc Huisinga]

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

[Marc Huisinga]

Adding an await to setLean4LanguageId makes it work :)

[Gabriel Ebner]

The fix is underway to a vscode near you!

[Marc Huisinga]

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

[Eric Wieser]

Is there an associated fix to the lean3 extension?

[Marc Huisinga]

The bug that this fixed was specific to vscode-lean4

[Eric Wieser]

Then I must be seeing a different bug with similar manifestation

[Marc Huisinga]

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]

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]

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]

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]

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

[Eric Wieser]

But I'm on windows

[Marc Huisinga]

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]

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

[Chris Lovett]

Are people still seeing the bug with \ not working sometimes in latest version of vscore-lean4 ? I can't seem to repro the bug. Looking at the code I can force a similar repro if I force this.dontTrackNewAbbr to get stuck a "true" in AbbreviationRewriter1.ts , which is what I suspect is happening, but looking at the code there is a try catch protecting that flag so I don't see how it can get stuck on. Switching active files back and forth completely reconstructs AbbreviationRewriter which is why that is a workaround. So I need a repro. In the meantime, this PR might help get more info if someone does fine a repro: https://github.com/leanprover-community/vscode-lean4/pull/35

[Arthur Paulino]

I use ; to escape unicode. Recently, when I've been encountering this problem, not even resetting VS Code solves it (it used to when \ was my escaping character). But I want to mention a weird workaround that I found.

The workaround is simply expanding the extensions menu and clicking on the lean4 extension.

image.png

Then I can just close the extension tab and it starts working again

[Gabriel Ebner]

this problem

I think I lost tracked of the issues in this thread. Can you explain the issue more clearly, ideally with steps to reproduce it?

[Arthur Paulino]

The problem is that escaping unicode suddenly stops working. For instance, when you want to type α then you type \ and a and it just stays as \a.

Unfortunately, I still haven't figured out a way to reproduce it. So I thought that a diagnosis by workaround might give us some clue about what's going on. For some reason, simply clicking on the lean4 extension icon solves it (until it happens again)

[Chris Lovett]

@Arthur Paulino you would have to type \ and a and space to get the abbreviation to activate to α.

But can you try disabling all other extensions you have loaded in VS code and see if it still repro's in that kind of pristine environment?

[Chris Lovett]

For example, I'm seeing a lot of uncaught exceptions from other extensions while typing inside a Lean source file, especially the github copilot extension... so I'm wondering if there's some bad extension that is confusing things here...

[Arthur Paulino]

Chris Lovett said:

Arthur Paulino you would have to type \ and a and space to get the abbreviation to activate to α.

But can you try disabling all other extensions you have loaded in VS code and see if it still repro's in that kind of pristine environment?

I'm aware of how you'd trigger the abbreviation, but I don't have other extensions except for one that makes certain characters glow in another color