VS Code - Unicode Input Discussion

Stream: general

[Henning Dieterichs]

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.

[Alex J. Best]

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

[Henning Dieterichs]

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.

[Jakob von Raumer]

I always use \to.

[Yakov Pechersky]

or even \r

[Jakob von Raumer]

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)

[Gabriel Ebner]

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.

[Gabriel Ebner]

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.)

[Gabriel Ebner]

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).

[Gabriel Ebner]

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

[Henning Dieterichs]

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.

[Henning Dieterichs]

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.

[Henning Dieterichs]

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.

[Henning Dieterichs]

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 ;)

[Henning Dieterichs]

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?

[Henning Dieterichs]

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.

[Gabriel Ebner]

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.

[Alex Peattie]

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

[Patrick Massot]

@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.

[Patrick Massot]

Now the VScode extension put subscript 0 everywhere.

[Patrick Massot]

For people with default input leader: try typing \ .

[Patrick Massot]

(That's backslash followed by a space).

[Patrick Massot]

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

[Bryan Gin-ge Chen]

@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

[Marc Huisinga]

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

[Bryan Gin-ge Chen]

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

[Yakov Pechersky]

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 \

[Patrick Massot]

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

[Henning Dieterichs]

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

[Henning Dieterichs]

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.

[Henning Dieterichs]

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 \\.

[Bryan Gin-ge Chen]

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

[Henning Dieterichs]

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.

[Johan Commelin]

@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 , ...

[Mario Carneiro]

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

[Gabriel Ebner]

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?

[Gabriel Ebner]

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

[Patrick Massot]

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.

[Patrick Massot]

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.

[Henning Dieterichs]

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

[Henning Dieterichs]

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.

[Henning Dieterichs]

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.

[Alex Peattie]

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?

[Patrick Massot]

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

[Kevin Buzzard]

you misspelt emacs

[Patrick Massot]

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?

[Alex Peattie]

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"