Unicode math input via OS instead of editor

Stream: Editors & UIs

[Castedo Ellerman]

I have updated documentation on how to input Unicode math symbols on GNOME at https://vim.castedo.com/math-input/

This particular page is relavent to anyone hoping to input math into any application, including editors (like Vim 9) that are not the recommended ones for Lean.

If folks would like this material somewhere else on the web, I'm happy to move/copy it to other locations.

I've only documented the desktop environment I use. If someone would like to add documentation for their non-GNOME or non-Linux system, please feel free to contact me.

The page might be useful as a "cheat-sheet" for those taking this approach. If anybody has suggestions on how to make it a better cheat sheet, please feel free to share. (I'm adding symbols as I use them making my way through the "Logic and Mechanized Reasoning" and "Functional Programming in Lean" textbooks.)

[Johan Commelin]

Related: https://github.com/gebner/m17n-lean

[Patrick Massot]

Trying to follow the link https://vim.castedo.com/math-input/ I’m asked my gitlab credentials. I guess this is not intended?

[Castedo Ellerman]

Definitely not intended. This is a bit embarrassing. Thanks for catching that! I will fix. Not sure yet how soon though.

[Castedo Ellerman]

Johan Commelin said:

Related: https://github.com/gebner/m17n-lean

Thanks! I will add that to the documentation. @Gabriel Ebner Any idea how many people are using gebner/m17n-lean?

[Castedo Ellerman]

The GitLab credentials issue is fixed now. https://vim.castedo.com does not ask for gitlab sign-in now. There was a default setting in GitLab I had not flipped to public access and I didn't realized it.

[Johan Commelin]

Gabriel is no longer active in the community, but I think at least a handful of people were/are using that setup.

[Patrick Massot]

What is the point of those complicated methods depending on Gnome compared to just using XCompose, and maybe some custom keymap if desired?

[Castedo Ellerman]

Patrick Massot said:

those complicated methods

Do you mean the complexity of set up or the complexity of switching keyboard and typing the key sequences?

[Castedo Ellerman]

The set up is of equal complexity as how I setup my Spanish/International keyboard on GNOME, which I don't consider very complicated. For complexity of input, it also doesn't strike me as very complicated. I'm usually in my "math keyword", but if I'm not, I just hit Window-Space. And then I know LaTeX so I find the latex commands very easy to remember e.g., I just type '\alpha` and I get α.

[Castedo Ellerman]

XCompose appears to be a X Window solution so I suspect that work on Wayland. At least in the Fedora world, X Window seems to be gettin dropped and it's Wayland only by default.

[Castedo Ellerman]

For custom keymaps, that sounds complicated to me.

[Castedo Ellerman]

But I'm happy to add links/mention to these other ways of OS support for math input! Currently GNOME/I-Bus seems to be a nice setup but I'm happy to help other find other solutions.

[Castedo Ellerman]

Maybe I should add some screen shots to how this works with GNOME/I-Bus.

[Castedo Ellerman]

Or like just some explanation on how one acutally types in say ∀ α ∈ ℤ etc... which is \forall \alpha \in \setZ

[Patrick Massot]

The complexity is having instructions depending on the window manager.

[Castedo Ellerman]

By complexity you mean the instructions? In other words, an instruction page with "here are 15 different OS/desktop/window manager setups, choose yours" vs simplicity of "install VS Code extension, done"?

[Castedo Ellerman]

I'm not following what A vs B we are comparing in terms of complexity.

[Johan Commelin]

Yes, apart from the Wayland vs X issue, a solution involving XCompose just works "everywhere" on the Linux desktop.

[Castedo Ellerman]

Sounds like some Linux folks are happy with XCompose. I'm reading up on it now and I'll add something to the math-input page to mention and point to XCompose. Here is a GH issue to track this addition: https://github.com/castedo/vim9-lean/issues/1

[Castedo Ellerman]

I'm assuming tracking issues is GitHub rather than GitLab makes it x1000 times more likely for people to particpate. I'll be writing details /thoughts in that GH issue.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

On Mac I have been using a globally registered input method with the same abbreviations as vscode-lean4. See https://gist.github.com/Banus/37c78e3f1abb50338fb10aefb929e1f4 .

[Julian Berman]

Oh nice, that looks really good, I'll have to try it later myself.

[Snir Broshi]

That's very cool, but I find it awkward to switch languages to use symbols.
Did anyone on macOS try to use Raycast's snippets / Hammerspoon / Karabiner-Elements for this?

[Eric Paul]

I'm using Espanso for this on mac to replace my \something sequences into symbols. I have it disabled for vscode and the web editor as otherwise it conflicts with Lean's normal unicode input.
(Here's my espanso config with the Lean abbreviations added in case it is helpful.)

[Snir Broshi]

Thank you! I installed Espanso and configured it to let me use all the Lean abbreviations on Zulip & GitHub, using Nix home-manager. When I rebuild Nix it fetches the current abbreviations and creates an Espanso config:

# place inside the Home Manager config
# requires building with `--impure`
services = {
  espanso = {
    enable = true;
    configs = {
      default = {
        enable = false;
        show_icon = false;
        search_shortcut = "off";
      };
      specific = {
        filter_exec = "Chrome|Zulip";
        enable = true;
      };
    };
    matches.default.matches =
      let
        url = "https://raw.githubusercontent.com/leanprover/vscode-lean4/refs/heads/master/lean4-unicode-input/src/abbreviations.json";
        leanAbbrevs = builtins.fromJSON (builtins.readFile (builtins.fetchurl url));
        leanEspansoAbbrevs = map (k: { trigger = "\\" + k + " "; replace = leanAbbrevs.${k} + " "; }) (builtins.attrNames leanAbbrevs);
      in [
        { trigger = ":hello"; replace = "world"; }
      ] ++ leanEspansoAbbrevs;
  };
};

[Castedo Ellerman]

I'm not really sure what :octopus: really means, but I'm pretty sure it's a compliment. :sweat_smile:
@Snir Broshi if you put that online (like in a gist) I'll link to it. I'm adding a section for Espanso.

[Castedo Ellerman]

Looks like Espanso has a package system and @Johannes C. Mayer has made one for Lean: https://hub.espanso.org/lean-symbols

[Snir Broshi]

Oh cool! Though it's 2 years old at this point, maybe we should update it
https://github.com/espanso/hub/tree/main/packages/lean-symbols/1.0.0

[Castedo Ellerman]

Math is timeless and eternal; 2 years is nothing. :wink:

[Castedo Ellerman]

Thank y'all for your questions and suggestions! It really helped identify missing info. I have made a major update to the page about OS-level keyboard input:
https://vim.castedo.com/math-input/
Feedback welcome. This page should probably get moved to some community page. It's not vim specific.

[Castedo Ellerman]

Now that I have educated myself more about XCompose, I can better answer previous questions. I'm happy add more pointers and tips about ~/.XCompose files if X11 fans want to share them.

Patrick Massot said:

What is the point of those complicated methods depending on Gnome compared to just using XCompose, and maybe some custom keymap if desired?

I've now added info about XCompose and separate top-level "Linux with X11" vs "Linux with Wayland" sections. I hope this shunts readers to one or the other for simplicity. I've also, hopefully, made it more clear the relationship between Wayland, IBus, m17n, and Gnome. The only instructions that are specific to Gnome are some UI steps.

The complexity is having instructions depending on the window manager.

The page now has the non-XCompose instructions depending on IBus. The complexity of IBus replacing XKB is unavoidable.

Johan Commelin said:

Yes, apart from the Wayland vs X issue, a solution involving XCompose just works "everywhere" on the Linux desktop.

Agreed, XCompose works on all X11 installs. But on Wayland your millage is going vary a lot depending on how many X11 corner cases will be supported by a Wayland distro. For example, on RHEL 10 the XCompose dead keys seem to be abandoned on RHEL 10 and I can not type α via XCompose. It's not a simple situation.