Lean unicode Chrome extension

Stream: general

[Arthur Paulino]

I'm building a Chrome extension that will allow us to use unicode characters here on Zulip (or on other sites if we want).

It's still WIP, but it already works with "\" as escaping key. Press "alt" twice to toggle it on/off.
https://github.com/arthurpaulino/chrome-lean-unicode

Note: not on store yet

[Jason Rute]

Can it be configured to only be turned on for Zulip?

[Arthur Paulino]

Yeah, that's the current configuration (you can see it on the manifest file)

[Arthur Paulino]

The configurable settings will be:

• The escaping character
• Whether to have it activated by default or not when visiting the Tulip website

[Bolton Bailey]

This would be nice for leaving comments in PRs on Github too

[Arthur Paulino]

Once I learn how to make the popup for the settings, adding those configurations will be pretty easy

[Kevin Buzzard]

BTW I have no idea how but thanks to @Eric Wieser I can write ℝ on my Android phone on the Zulip app with \R

[Eric Wieser]

The Zulip thread describing how can be found by searching zulip for "UDM" (I can't work out how to get a thread link from mobile)

[Stuart Presnell]

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

[Arthur Paulino]

/poll If you're intending to use the extension, please let me know the escaping character (so I can avoid bugs in the regex)
\
,
.
;

[Arthur Paulino]

(deleted)

[Wojciech Nawrocki]

It's worth mentioning also that for those on Linux, an option for system-wide Lean abbreviations is Gabriel's m17n-lean.

[Arthur Paulino]

Gabriel's solution just gave me an idea for a system wide cross platform (except for smartphones) solution using Python and pynput.

But I am already satisfied with the options we have available (unless a real need appears)

[Arthur Paulino]

The first version of the extension is ready!
https://github.com/arthurpaulino/chrome-lean-unicode
Instructions in the README. Please do report bugs, behavior changes and/or feature requests as issues
image.png

[Filippo A. E. Nuccio]

Hi Arthur, very nice! Will it work also in the Zulip app or only accessing Zulip website on Chrome?

[Arthur Paulino]

Only in Chrome. If you're on a smartphone, Eric's solution might work better

[Floris van Doorn]

It works like a charm for me! :tada:

[Oliver Nash]

Thank you very much for doing this @Arthur Paulino Great work!

Is there any hope of something similar for us Firefox users who refuse to use Chrome?

[Floris van Doorn]

And in the search box for VSCode :smile:

[Arthur Paulino]

Oliver Nash said:

Thank you very much for doing this Arthur Paulino Great work!

Is there any hope of something similar for us Firefox users who refuse to use Chrome?

Oh, I have no idea how to make it work in Firefox. Actually I had no idea how to make it work in Chrome either. It was my first extension :joy:
Would totally appreciate some help in expanding it tho!

BTW: I don't use Chrome exactly. I use Chromium and it works nicely for me

[Arthur Paulino]

Floris van Doorn said:

And in the search box for VSCode :smile:

The only idea that comes to my mind to make it work in multiple applications like that is some kind of system app of its own (as opposed to a browser extension).

As I said before, I do have an idea using a Python script that reads input with a lib called pynput.

[Gabriel Ebner]

If you're looking for system-wide support, there's m17n-lean. It works in vscode, the terminal, browsers, etc. It's Linux-only though, I'm not sure what the best approach is for Windows/Mac.

[Vincent Beffara]

Something like https://espanso.org/ seems to be flexible enough

[Eric Rodriguez]

I use WinCompose (not quite equivalent) in Windows, I haven't figured out a Mac alternative yet (although I haven't spent the full time trying to get m17n-lean work)

[Julian Berman]

I'd look into karabiner for macOS, it may be able to do this and is a standardish thing people use for low level keyboard things.

[Gabriel Ebner]

We should put a list with links to all these extensions on the website. Is your WinCompose plugin public?

[Eric Rodriguez]

I don't really use a plugin, I turn off a couple features that make like <compose> a* into å and instead make it \alpha (there's overlapping keybinds by default), but otherwise much the default. I'll try and post the full setup when I'm back to my Windows PC

[Arthur Paulino]

Nice to have so many options, although I think it would be better if we had a default solution for the community that works on any OS or any app (terminal, browser, vscode etc). Question is: who would be willing to develop/maintain/support it? I would :+1:

[Arthur Paulino]

The solution I'm thinking is using pynput to monitor and control the keyboard. When a replaceable string is observed, the script simulates the user hitting backspace really fast a certain number of times and then typing out the corresponding unicode character. Does it sound too hacky? In theory, looks pretty easy to get it going (I have previous experience using pynput)

[Arthur Paulino]

This solution is simpler and more lightweight than the chrome extension I developed

[Gabriel Ebner]

I think it would be pretty jarring to have simulated backspace presses. For example what happens if you move the cursor using the mouse between typing \alph and a?

[Arthur Paulino]

moving the mouse (or rather, clicking with the mouse) would cancel/reset the buffering (it's possible to monitor the mouse too). But yeah, good catch

[Arthur Paulino]

I guess I can only find out by making a simple PoC and experimenting with it

[Gabriel Ebner]

works on any OS or any app

I don't think that's technically feasible. E.g. the pynput approach that you've described won't work on android (since you can't capture the keyboard input).

It's important to use the same set of abbreviations for all the plugins, but we're doing that already by copying the abbreviations.json file.

[Arthur Paulino]

Good point! For smartphones it's pretty much uncharted territory. Because there's Android and iOS

[Arthur Paulino]

(Although Eric found a solution for Android)

[Alexander Bentkamp]

Vincent Beffara said:

Something like https://espanso.org/ seems to be flexible enough

@Arthur Paulino This seems to do exactly what you want. I runs on Win, Mac, Linux. I guess you'd just have to write a configuration file.

[Arthur Paulino]

Oh, they even have some sort of store: https://hub.espanso.org/

[Vincent Beffara]

I use it, it's great. Sample configuration file:

matches:
  - trigger: "/s/"
    replace: "{ sorry }"

(very useful for lean ...)

[Vincent Beffara]

Generating the whole list from the one in m17n-lean for instance would be a one-line sed command. The only issue I'm not sure about is choosing the trigger character not to interfere with other software, typically for LaTeX, but in any case switching it on and off is very quick with a hotkey.

[Arthur Paulino]

Toggle Key
There are times when you may want to disable espanso to avoid an unwanted expansion. This can be easily accomplished by quickly double pressing the ALT key ( Option on MacOS ). You should then see a notification showing "Espanso disabled".
At this point, espanso will be disabled and will not expand any match. To re-enable it, double press the ALT key again.

[Arthur Paulino]

Funny that they chose the same method that I did: hitting ALT twice
(more precisely, I chose the same method that they did because they did it first :joy: )

[Arthur Paulino]

The only issue that I see is that there's no concept of "escaping key". It's all based on matches so people that use different escaping keys for unicode would have to have different configuration files

[Kevin Buzzard]

This would be really helpful for me. I'm not techy enough to get Gabriel's solution working on my laptop but right now I'm writing Lean code in rst files and constantly having to cut and paste from VS Code lean scratch files.

Writing this it occurs to me that it's worth asking whether it's easy to make \alpha work in rst files in e.g. VS Code.

[Arthur Paulino]

Ideally the extension would ask for more file extensions for which the abbreviations would be triggered so the user could add txt, rst, md etc. But I don't know if that's easy either

[Julian Berman]

@Kevin Buzzard I think Gabriel seems to have left instructions for how to do so here -- https://github.com/leanprover/vscode-lean/issues/278#issuecomment-889720492

[Julian Berman]

(Add rst instead of agda obviously)

[Patrick Massot]

Vincent Beffara said:

I use it, it's great. Sample configuration file:

matches:
  - trigger: "/s/"
    replace: "{ sorry }"

(very useful for lean ...)

VScode already have you covered here. You can define as many code snippets as you want.

[Arthur Paulino]

Would it not be possible to make the abbreviation part a separate git repository, then include it as a submodule here as well as upload it as a separate plugin? Then new users to Lean would have it no harder to install the plugin, and people who want to use ergonomic unicode input can install it as a separate plugin and use it in whatever language the choose.

I think that's a neat idea. Writing unicode and communicating with Lean server seem like separate scopes enough to be in different plugins. It would also avoid duplication of code for doing the same thing in the Lean 3 and Lean 4 extensions.

[Alex J. Best]

Patrick Massot said:

Vincent Beffara said:

I use it, it's great. Sample configuration file:

matches:
  - trigger: "/s/"
    replace: "{ sorry }"

(very useful for lean ...)

VScode already have you covered here. You can define as many code snippets as you want.

You can also add extra completions to the lean extension in the vscode settings.json e.g.

    "lean.input.customTranslations": {"so": "{ sorry }"},

makes \so complete to {sorry}

[Patrick Massot]

The snippet mechanism is a more powerful version: https://code.visualstudio.com/docs/editor/userdefinedsnippets

[Patrick Massot]

but indeed a custom translation is enough for that sorry thing

[Vincent Beffara]

I should probably learn to use vscode a bit better ... It still makes sense to have a global option in order to type lean code in the zulip app, in email or whatever, even if it is less powerful

[Arthur Paulino]

Updates: I tried my approach and there were two problems:

• Simulating backspace is mysteriously slow and makes the OS stutter a bit, which is rather annoying
• pynput triggers recent macOS' security system and requires root to run (thanks for the heads up @Julian Berman!)
  My goal was to make something simpler, more focused and convenient for our use case, but it seems like those who want a system wide solution will have a better chance with the other alternatives posted above :point_up:

[Henrik Böving]

What I do when I wanna type lean code up in a non Emacs text field is use a slightly modified version of https://github.com/tecosaur/emacs-everywhere that just instantly drops me to some lean file in a lake project I have laying around just for this where I can type either my lean code or with the power of the lean input method just normal utf-8 in a lean comment, then I close it and what was in the buffer gets automatically copied to my clipboard so I can just paste it here. Maybe you could implement something similar with vscode? This seems a lot easier and more general purpose than having an extesion specific to one browser and you get all the benefits of a full lean editor for free.

The only extra thing apart from the plugin (and my slight mod to make it lean specific) was that I had to register a custom keybinding in my window manager that opens my emacs in this specific state. I know from the readme that this is possible on both linux and macos but I dont have any clue about windows so maybe thats a dealbreaker here.

[Arthur Paulino]

That's one possibility, yeah. But it's one step further away. I wrote the extension because I got tired of switching windows to type an "α" or a "→" (and also because I had never written one so I wanted to learn how). I wanted something as natural as possible.

[Julian Berman]

If we're making a longer list I'll also throw in fire.nvim :) -- which will make every <input> element in your browser run a little embedded neovim, which you can then use lean.nvim's abbreviations for. That should work cross-platform in any browser at least (I've certainly used it not for Lean but just in general e.g. to write code in GitHub comments).

[Yaël Dillies]

Could it behave more like the VScode extension by allowing partial matches? For example, I have to type an excruciating \backcong to get ≌ instead of the already long \backc.

[Arthur Paulino]

Do you mean the chrome extension?

[Yaël Dillies]

Yes :)

[Arthur Paulino]

Sure

[Arthur Paulino]

I'm making it robust to typos. For instance, if you type \sqry, sqrt is still the longest match (three characters) so it's gonna replace the entire thing by √

[Arthur Paulino]

oops (testing)

[Alex J. Best]

Copying the logic of the vscode extension for matches seems like a good idea to me. Seeing as its written in some flavour of javascript can you just reuse the exact code? (maybe you are already doing this)

[Yaël Dillies]

Yeah, I don't care what it does exactly as long as it does the same as the VScode extension.

[Arthur Paulino]

Okay, you can update your extension https://github.com/arthurpaulino/chrome-lean-unicode
The behavior is slightly different for partial matches, but I think it makes more sense this way.

With the extension, if you type \ba it replaces it with ≌ for you. In VS Code, it's replaced with ∽ (idk why)

[Yaël Dillies]

\backsim? Both make sense, I guess

[Julian Berman]

I believe it finds the shortest extension of what you typed

[Julian Berman]

(Which, backsim is shorter than backcong)

[Julian Berman]

lean.nvim does what VSCode does here too

[Julian Berman]

I see the commit says you're doing longest, right? I think that will have weird behavior for e.g. \a no? That does alpha in other places, but now will do some very long thing starting with a

[Julian Berman]

Oh -- never mind, there's independently an abbreviation for "a", so that one will work

[Julian Berman]

But some other similar example I suspect will be wrong

[Arthur Paulino]

Right, backsim.
But about the "longest", it's the longest match between what you type and the abbreviations available, not the longest of the matches of equal length

[Yaël Dillies]

I'm gonna add \~== for ≌ because I find it especially painful to write.

[Arthur Paulino]

For \ba, the extension picked backcong simply because of the order of visiting. All other abbreviations that start with ba have the same match length so none of them were able to beat the first one. This is easily adjustable if anyone wants this behavior though

[Arthur Paulino]

Ah, wait. This can be flawed. If you type \xy for an abbreviation xy and then the algorithm visits xyz first, it's gonna pick it because xy can't beat it. So it's actually necessary to pick the shortest abbreviation among those of maximal match length

[Arthur Paulino]

Extension updated again :+1:
Thanks for the input!

[Yaël Dillies]

Don't worry! You'll get a lot more \qed.

[Arthur Paulino]

Hi everyone,
I just fixed a bug that made the extension trigger on every URL if you tried to add another URL.
If you use the extension, please update it to the most updated version on master: https://github.com/arthurpaulino/chrome-lean-unicode

[Gabriel Ebner]

I've submitted a PR to the espanso hub: https://github.com/espanso/hub/pull/50 (source repo: https://github.com/gebner/espanso-lean)

[Arthur Paulino]

https://github.com/arthurpaulino/chrome-lean-unicode has been updated with the latest abbreviations. If you're using it, you can update it