Zulip Chat Archive

Stream: lean4

Topic: abbreviations in vscode


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Feb 12 2021 at 08:50):

I've seen the same behavior in lean 3

view this post on Zulip Gabriel Ebner (Feb 12 2021 at 09:48):

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

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip Marc Huisinga (Feb 12 2021 at 11:46):

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

view this post on Zulip Marc Huisinga (Feb 12 2021 at 11:52):

Adding an await to setLean4LanguageId makes it work :)

view this post on Zulip Gabriel Ebner (Feb 12 2021 at 12:06):

The fix is underway to a vscode near you!

view this post on Zulip Marc Huisinga (Feb 12 2021 at 12:08):

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

view this post on Zulip Eric Wieser (Feb 12 2021 at 12:56):

Is there an associated fix to the lean3 extension?

view this post on Zulip Marc Huisinga (Feb 12 2021 at 12:57):

The bug that this fixed was specific to vscode-lean4

view this post on Zulip Eric Wieser (Feb 12 2021 at 13:34):

Then I must be seeing a different bug with similar manifestation

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Feb 14 2021 at 17:52):

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

view this post on Zulip Eric Wieser (Feb 14 2021 at 17:52):

But I'm on windows

view this post on Zulip 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 "¬".

view this post on Zulip 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