Math input with XCompose

For a comparison of XCompose vs. IBus, see the Linux section.

Setup

Step 1: Save a ~/.XCompose file

Download this .XCompose file and save it to ~/.XCompose:

cd
curl -O http://lean.castedo.com/math-input/xcompose/.XCompose

You will probably need to restart your Wayland and/or X Window input system. Logging out and logging back into your desktop session is an easy, but inconvenient, way to do this. On Wayland with IBus you can just run ibus restart.

Step 2: Enable a compose key

This step is not required on some Linux desktops that are not GNOME Desktop on Wayland, such as older X11 distros.

On GNOME Desktop

Go to Settings > Keyboard > Special Character Entry > Compose Key, enable Compose Key, and choose which key will become the compose key.

Warning

Depending on your distro, you may encounter issues with less common XKB compose key sequences like dead keys. The ~/.XCompose file provided on this page does not use dead keys. Major Linux distros such as Ubuntu, Debian, RHEL, CentOS, and Fedora support ~/.XCompose files, but their migration to Wayland has caused some X11 functionality to break. For example, using XKB <dead_greek> does not seem to work in RHEL 10, even though most compose key sequences do work.

How to use

To input ∀α, type:

compose A L L enter compose A enter

Updates to .XCompose

See this Zulip Topic for the Lean script by Anthony Wang, and the keysymdef.h file used by it, to generate a new .XCompose file for Lean.

History

The X Window System (X11) has been the windowing system used by Linux for decades. X11 uses the X keyboard extension (XKB) for keyboard input. Major Linux distros such as Ubuntu, Debian, RHEL, CentOS, and Fedora, and desktop environments GNOME and KDE have transitioned to, or are in the process of transitioning to, Wayland. Although Wayland is backward compatible with most X11 features, it is not fully backward compatible with all X11 features.