Input method not activated after switching to buffer with the relevant major mode

[Nasrudin]

What happened?

The input method (“Lean”) for major mode lean4-mode triggers autocompletion for various unicode symbols, and doesn’t activate by default when I open a Lean4 buffer/project; I have to do M-x toggle-input-method to activate it for every Lean4 buffer where I want the input method.

Per this stackoverflow answer, I’d like to fix that by triggering (activate-input-method "Lean") in any buffer where lean4-mode is the major mode. In my config.el, I have

(after! lean4-mode
  (add-hook 'lean4-mode-hook
    (lambda ()
      (activate-input-method "Lean"))))

This does not appear to cause any change to the input method or trigger any errors or logs that I can see in Messages.

What did you expect to happen?

I expect the input method to change when I switch to any buffer with the lean4-mode major mode.

Steps to reproduce

0. Enable lean with +lsp in init.el.
1. Setup lean4-mode, per repo instructions appropriate for your emacs/doom-emacs/system config.
2. Add the hook above to config.el
3. Create a Lean4 project.
4. Open a Lean4 file in that project and either look for the Lean input method symbol in the modeline (Π) or attempt to trigger autocompletion.

If autocomplete is working, then there should be a Π in the modeline and e.g. \alpha should autocomplete to α. If the Lean input method is not active, there will be no Π in the modeline and \alpha will simply remain as-is in the buffer.

System information

Loading data dump...