Zulip Chat Archive

Stream: general

Topic: VS Code - Unicode Input Discussion


view this post on Zulip Henning Dieterichs (Jan 07 2021 at 17:25):

I have some thoughts about unicode-input improvements in VS Code that I would love to discuss (I also opened a Github issue here).

I already opened a PR that rewrites the unicode-abbreviation feature, fixes some bugs and implements eager-replacing (i.e. abbreviations are replaced as soon as they uniquely identify a symbol).

1) Eager Replacing. I often type \<-, \-> and \<->. Unfortunately, there is \<-n, \->n and \<->n which makes those abbreviations not-prefix-free.
I can imagine two fixes for that:
1.1) When \-> is typed, it is temporarily replaced with . When the replaced symbol is extended with n immediately after that, →n gets replaced by
1.2) Like 1.1, but the temporary replacement of non-unique abbreviations only happens after a timeout (like 400ms).

2) Autocompletion. I think it might make sense to implement autocompletion for all available abbreviations. This might conflict with (1.1) though.

3) Context Sensitivity. When there is h₁ around in the current document but no h1 and I type h1 and then hit tab, it might be a cool feature if h1 could be replaced by h₁.

What do you think?
These features shouldn't be too hard to implement on top of my refactoring.

view this post on Zulip Alex J. Best (Jan 07 2021 at 17:50):

You can also type \l for \<- and \r for \-> FYI (its way easier for me at least).

view this post on Zulip Henning Dieterichs (Jan 07 2021 at 18:11):

I'm using the Neo2 keyboard layout in which \, -, > are all on the same layer and nicely distributed among the left and right hand, so it is actually very convenient to type that sequence.

view this post on Zulip Jakob von Raumer (Jan 07 2021 at 18:12):

I always use \to.

view this post on Zulip Yakov Pechersky (Jan 07 2021 at 18:13):

or even \r

view this post on Zulip Jakob von Raumer (Jan 07 2021 at 18:13):

I actually think that the input problem has been solved perfectly by Agda-mode, which for a while I also used for Lean (in emacs)

view this post on Zulip Gabriel Ebner (Jan 07 2021 at 18:24):

Eager replacing.

I think this would be nice. I often feel like the input mode lingers around too long, even after I've typed enough for a unique conversion. I'm thinking of things like \a}.

\->n

You shouldn't type this as it is not idiomatic Lean, there's supposed to be a space after an arrow.

happens after a timeout (like 400ms).

I'm very very strongly against timeouts in keyboard input. What I type shouldn't depend on how fast I type it.

view this post on Zulip Gabriel Ebner (Jan 07 2021 at 18:32):

Context Sensitivity. When there is h₁ around in the current document but no h1 and I type h1 and then hit tab, it might be a cool feature if h1 could be replaced by h₁.

I'm also very strongly against context-sensitivity or other hidden state in keyboard input. What I type shouldn't depend on where I type it, or what I've typed half an hour ago.
However I have nothing against making h1<TAB> convert to h₁ everywhere. (Maybe we could have a command/shortcut that converts an abbreviation even if we're not in input mode and even without a backslash in front.)

view this post on Zulip Gabriel Ebner (Jan 07 2021 at 18:35):

Henning Dieterichs said:

I'm using the Neo2 keyboard layout in which \, -, > are all on the same layer and nicely distributed among the left and right hand, so it is actually very convenient to type that sequence.

Lean users use lots of different keyboard layouts, and I don't want anybody to learn a new keyboard layout just to use Lean. Any input system should work with all keyboard layouts.
This is the reason the leader key (which defaults to backslash) is customizable: Patrick uses , because backslash is hard to type on French keyboards, I've seen Ed use £ (presumably because it's easy to type on a UK keyboard).

view this post on Zulip Gabriel Ebner (Jan 07 2021 at 18:44):

it is temporarily replaced with →

This is indeed how my system-wide input method works, and I find it a bit irritating: https://github.com/gebner/m17n-lean
m17n-lean-convert.mp4 m17n-lean-convert.gif

view this post on Zulip Henning Dieterichs (Jan 07 2021 at 20:57):

You shouldn't type this as it is not idiomatic Lean, there's supposed to be a space after an arrow.

This is an abbreviation for a unicode sequence! It get's expanded to ↛t for example. It is in translations.json currently.

view this post on Zulip Henning Dieterichs (Jan 07 2021 at 21:00):

I'm very very strongly against timeouts in keyboard input. What I type shouldn't depend on how fast I type it.

It would only temporarily transform and the transformation would only be a matter of presentation. If you don't type blind, you wouldn't even notice it, as if it transforms due to the timeout, added characters might lead to a different transformation. Also, if you never use the abbreviation \->n, you wouldn't notice it.

view this post on Zulip Henning Dieterichs (Jan 07 2021 at 21:02):

I'm also very strongly against context-sensitivity or other hidden state in keyboard input. What I type shouldn't depend on where I type it, or what I've typed half an hour ago.

It wouldn't be a hidden state, it would be based on what appears in the document. It is like simp whose behavior also depends on the content of the current document. Intellisense also does something like this, except that an autocompletion list pops up.

view this post on Zulip Henning Dieterichs (Jan 07 2021 at 21:04):

Lean users use lots of different keyboard layouts, and I don't want anybody to learn a new keyboard layout just to use Lean. Any input system should work with all keyboard layouts.

I, as a user of a keyboard layout that only a couple of thousand people use, cannot agree more! I just wanted to respond to "its way easier for me at least" and do some Neo2 advertisement ;)

view this post on Zulip Henning Dieterichs (Jan 07 2021 at 21:06):

Gabriel Ebner said:

it is temporarily replaced with →

This is indeed how my system-wide input method works, and I find it a bit irritating: https://github.com/gebner/m17n-lean
m17n-lean-convert.mp4 m17n-lean-convert.gif

Interesting! What system is this? Do you use this system also in VS Code, if you use VS Code? If there was some delay until the presentation changes, would you find it less confusing?

view this post on Zulip Henning Dieterichs (Jan 07 2021 at 21:08):

Jakob von Raumer said:

I actually think that the input problem has been solved perfectly by Agda-mode, which for a while I also used for Lean (in emacs)

Can you share a recording or point to a demo video? Also, VS Code has some limitations. You cannot really override the rendering or do fancy stuff, you actually need to replace the text and carefully track any changes.

view this post on Zulip Gabriel Ebner (Jan 07 2021 at 21:39):

I think I misunderstood you with \->n. If you meant that the display changes from \ to \- to to , then I find the last step a bit irritating. Another very common one is \to, which changes from \ to to .

If you don't type blind, [...]

But I do!

Interesting! What system is this?

There is a longer description at the link I posted. This is an input method. Typically you use input methods for languages like Japanese/Chinese/etc. where it's infeasible to have one key per character, e.g. you type jidouteirisyoumei and you get 自動定理証明. This works in every application, terminal, etc. At least on linux it's fairly easy to add "table-based" input methods where you just need to provide a file with all the translations. That's what I did for lean and now I can switch to Lean input using a key shortcut. (There are also other approaches using xmodmap, etc.)

Do you use this system also in VS Code, if you use VS Code?

No, I find the vscode implementation to be more ergonomic.

If there was some delay until the presentation changes, would you find it less confusing?

Yes, I'd definitely find it less confusing. As long as it doesn't affect the end result.

view this post on Zulip Alex Peattie (Jan 08 2021 at 11:53):

Henning Dieterichs said:

I'm also very strongly against context-sensitivity or other hidden state in keyboard input. What I type shouldn't depend on where I type it, or what I've typed half an hour ago.

It wouldn't be a hidden state, it would be based on what appears in the document. It is like simp whose behavior also depends on the content of the current document. Intellisense also does something like this, except that an autocompletion list pops up.

simp behaves on the current tactic state rather that what's "around" the cursor right? I think I would suggest either:

  • A "normal" unicode expansion of h1, h2 etc. to h₁, h₂ as Gabriel mentioned
  • A more robust feature to autocomplete variable names (with unicode awareness) based on what's present in the current scope/tactic state. I think this would need coordination between the Lean server & VSCode (a la widget view) rather than something that can be done purely in VSCode

view this post on Zulip Patrick Massot (Jan 19 2021 at 22:11):

@Gabriel Ebner and @Henning Dieterichs I didn't follow closely what happened here but unfortunately the input feature of the VScode extension is now unusable.

view this post on Zulip Patrick Massot (Jan 19 2021 at 22:14):

Now the VScode extension put subscript 0 everywhere.

view this post on Zulip Patrick Massot (Jan 19 2021 at 22:15):

For people with default input leader: try typing \ .

view this post on Zulip Patrick Massot (Jan 19 2021 at 22:15):

(That's backslash followed by a space).

view this post on Zulip Patrick Massot (Jan 19 2021 at 22:19):

Note: I'm super grateful that people work on the VScode extension, but here I would say there is some emergency for me.

view this post on Zulip Bryan Gin-ge Chen (Jan 19 2021 at 22:20):

@Patrick Massot if you need to roll back to an earlier version before a fix lands, you can install manually from the GitHub releases: e.g. https://github.com/leanprover/vscode-lean/releases/tag/v0.16.20

view this post on Zulip Marc Huisinga (Jan 19 2021 at 22:21):

@Patrick Massot Does setting lean.input.eagerReplacementEnabled to false in your config help (as a quickfix)?

view this post on Zulip Bryan Gin-ge Chen (Jan 19 2021 at 22:22):

Oh, there's also "install another version" if you click on the little gear icon: Screen-Shot-2021-01-19-at-5.21.42-PM.png

view this post on Zulip Yakov Pechersky (Jan 19 2021 at 22:22):

Marc Huisinga said:

Patrick Massot Does setting lean.input.eagerReplacementEnabled to false in your config help (as a quickfix)?

I've unclicked the checkbox in Settings, but the keeps popping up if I mistype \

view this post on Zulip Patrick Massot (Jan 19 2021 at 22:24):

Thanks Marc and Bryan. Bryan's idea fixed this issue for me.

view this post on Zulip Henning Dieterichs (Jan 19 2021 at 22:48):

This is strange. I tested this thoroughly. Sorry for the inconvenience this brought. I need to look into it tomorrow.

view this post on Zulip Henning Dieterichs (Jan 19 2021 at 22:54):

I see the problem now which I guess is some kind of a specification issue. There is no empty abbreviation and no abbreviation that just contains the space, so when you type \ it tries the best it can - it looks for the shortest abbreviation that extends your typed abbreviation. Since your typed abbreviation is empty, it just takes a one character abbreviation. This happens to be \0.

view this post on Zulip Henning Dieterichs (Jan 19 2021 at 22:58):

If you specify the empty abbreviation in abbreviation.json (or as a custom abbreviation), I guess you can change this behavior. I have to test this out tomorrow. What do you want to happen when you type \ ? What happened before my change? If you want to type just the backslash, you can also type \\.

view this post on Zulip Bryan Gin-ge Chen (Jan 19 2021 at 23:00):

Before the change typing \ would cause the underline to go away and \ would remain.

view this post on Zulip Henning Dieterichs (Jan 19 2021 at 23:09):

Then this should be fixed by defining an abbreviation "" for "\". You should be able to do this with a custom abbreviation before this is fixed by an update.

view this post on Zulip Johan Commelin (Jan 20 2021 at 03:31):

@Henning Dieterichs but Patrick is typing , , because he's using a different leader key that is more convenient on French keyboards. I'm pretty sure he would like to have , turn into , ...

view this post on Zulip Mario Carneiro (Jan 20 2021 at 04:09):

@Henning Dieterichs The obvious solution is that if the abbreviation is empty then it cancels the replacement instead of "trying its best"

view this post on Zulip Gabriel Ebner (Jan 20 2021 at 08:51):

This should now be fixed in 0.16.22. I'm not sure what we can do to avoid this issues in the future. @Patrick Massot Is downgrading to an older version acceptable to you when it happens again in the future? Should we document this workaround somewhere?

view this post on Zulip Gabriel Ebner (Jan 20 2021 at 08:58):

You can also do ctrl+shift+p "disable auto updating" if you'd rather update the extensions on your own pace.

view this post on Zulip Patrick Massot (Jan 20 2021 at 09:12):

It works, thanks! I don't want to disable auto-updating, this is the first time in three years when I'm unhappy with an update. I'm not sure there is anything we can do except if someone is ready to spend a lot of time understanding how to unit test such bugs.

view this post on Zulip Patrick Massot (Jan 20 2021 at 09:18):

And I can also confirm Johan's intuition that I want , to type , . Henning, there is nothing sacred about \, it just happens to be a mostly useless character that is stupidly easy to access on a US keyboard, that's why it has been chosen by Knuth for TeX. People who designed the French keyboard didn't foresee this and they quite reasonably put \ in a less prominent position needing a combination of keys.

view this post on Zulip Henning Dieterichs (Jan 20 2021 at 13:55):

I fixed this issue here: https://github.com/leanprover/vscode-lean/pull/254

view this post on Zulip Henning Dieterichs (Jan 20 2021 at 15:17):

if someone is ready to spend a lot of time understanding how to unit test such bugs.

I think unit tests shouldn't be that hard to setup! I probably won't find much time soon, but in general I'm open to help.

view this post on Zulip Henning Dieterichs (Jan 20 2021 at 15:22):

I'm not sure there is anything we can do

With github actions, a lot of stuff could be automatized. I use to have an "insiders" build for one of my vs-code extensions that gets published on each commit to master. Both the insiders and the stable build are available in the marketplace - it is easy to switch between them. I usually wait some weeks until I release an insiders build as stable.

view this post on Zulip Alex Peattie (Jan 24 2021 at 11:07):

Another possible bug related to these changes - the abbreviations seem to be happening anytime I'm in VS Code, even if I'm not in the Lean language mode (i.e. editing a .lean file) :thinking: ... Are others seeing this behaviour too?

view this post on Zulip Patrick Massot (Jan 24 2021 at 11:08):

Why would we be using VScode to edit anything but Lean code while vim exists??

view this post on Zulip Kevin Buzzard (Jan 24 2021 at 11:19):

you misspelt emacs

view this post on Zulip Patrick Massot (Jan 24 2021 at 11:20):

I was waiting for such an heretic comment. Alex, why would we need you to use VS Code to edit anything but Lean file while we already have the emacs people to fight?

view this post on Zulip Alex Peattie (Jan 24 2021 at 11:25):

Haha! I propose a new theorem: "as an online discussion about text editors grows longer, the probability of an argument about Vim vs. Emacs approaches 1"


Last updated: May 16 2021 at 22:14 UTC