How to type unicode characters in Zulip?

Stream: Zulip meta

[Ching-Tsun Chou]

In Zulip, how do I type unicode characters common in Lean code? Currently I copy-and-paste from VScode, which is rather laborious and inelegant.

[Kevin Buzzard]

I've been using Zulip since 2018 and on PC I've been copy-and-pasting from VSCode all that time. On mobile I have in the past used a hack due to Eric Wieser which enables me to type the usual shortcuts on mobile like \le and have them display correctly, but I just got a new phone and I'm yet to find the thread where Eric explained how to get it all working.

[Jireh Loreaux]

If you're on Linux, then you can use an input method like FCITX with the m17n system and Gabriel Ebner's lean-m17n

[Yaël Dillies]

Here's what I use: https://github.com/arthurpaulino/chrome-lean-unicode

[Damiano Testa]

I believe that Kevin was referring to this post:

https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Unicode.20input.20on.20android

[Patrick Massot]

Note that simply using the compose key mechanism already allows a lot (and should work with much configuration on any Unix I guess).

[Patrick Massot]

You can also customize your keyboard layout to bring the most common unicode symbols directly to some key combination, for instance using https://github.com/OneDeadKey/kalamine.

[Ching-Tsun Chou]

Thanks to all who replied! As a Mac user, I find the Chrome extension that Yaël pointed to to be the most convenient. It works: α β ∑ Σ ↦

[Patrick Massot]

That’s nice, but note this will work only in your browser (and only a very privacy-hostile one). The other solutions would work everywhere.

[Ching-Tsun Chou]

Actually I want this capability only in Zulip and VScode. I usually use Safari and access Zulip in Safari. (I never found the stand-alone Zulip app to be worth the trouble.) Now I just use Chrome to run Zulip exclusively. The extension takes less than 5 min to set up and just works.