Document the pitfall of modifying `lean4-mode-hook` before Lean4-Mode has been loaded

[JLimperg]

Version 1.1.2 of lean4-mode has been broken for me in Doom Emacs for some time due to the following error.

Setup

I'm running Doom Emacs with the lean4-mode config from the README and the latest lsp-mode. If you can't reproduce, I'll be happy to provide more specific info.

Failure

When loading a Lean file, lean4-mode seems to start properly (no errors in Messages, no error buffers). However, LSP does not start: there's no semantic syntax highlighting, no type-checking, etc. Attempting to open the infoview results in an LSP error indicating that the LSP session does not support the plainGoal method.

Additional Info

I bisected the issue down to commit 78caecefb862f1e38daff7b7cc983651e2b726eb. Reverting this commit, like here, fixes the issue.

[lzy0505]

I can confirm both the issue and the fix.

[Thrithralas]

I encountered this issue recently too, but only when hooking 'lean4-mode-hook using add-hook!. I'm not familiar with lisp or hooks as much as I'd like to, but seemingly lsp is started inside the hook, which is overwritten(?) if add-hook! is used.

This can be circumvented by either manually starting lsp-mode or adding (lsp) at the end of the hook:

(add-hook! 'lean4-mode-hook
  ;; do whatever your hook is supposed to do here
  (lsp))

[mekeor]

Unfortunately, I wasn't able to set up Doom Emacs independently from my preexisting Emacs configuration. In other words, I couldn't get Doom running and I'm thus not able to reproduce this bug.

Can anyone provide more details or any hints why the function lsp, which is the single default member of the lean4-mode-hook variable defined in lean4-settings.el, is not called when lean4-mode is called?

[Thrithralas]

I've checked the value of the hook before and after using add-hook! in Doom (via apropos) with the following hook in my config:

(add-hook! 'lean4-mode-hook
    (setq comment-line-break-function nil))

• Before: (lsp)
• After: (#[(&rest _) ((setq comment-line-break-function nil)) (t)])

I can achieve a similar result by not using the macro, but using add-hook conventionally like so:

(add-hook 'lean4-mode-hook (lambda ()
  (setq comment-line-break-function nil)))

• After: (#[nil ((setq comment-line-break-function nil)) (t)])

I can't test it without doom emacs, as I would have to uninstall and reinstall doom, so I can't be sure if this exhibits the same behavior outside of it, but I'll try to cooperate however I can. Again, I'm not sure if this information is helpful or not in the first place, I'm not familiar with lisp or hooks.

[mekeor]

This issue probably occurs because your Emacs evaluates (add-hook 'lean4-mode-hook ...) from your init.el before it evaluates (defcustom lean4-mode-hook ...) from lean4-settings.el.

Please let me know if any of these approaches fixes the issue for you, corresponding to the style you maintain in your init.el:

• Put (require 'lean4-mode) before (add-hook 'lean4-mode-hook ...).
• Put (add-hook ...) inside (with-eval-after-load 'lean4-mode ...) or so.
• If you use use-package, put (add-hook ...) in the :config section of (use-package lean4-mode ... :config ...). Note that the :hook section would not do the job, as it is sugar for the :init phase, i.e. before lean4-mode feature is loaded.

(Thanks to bpalmer at #emacs:libera.chat for insights.)

[Thrithralas]

The first two both work flawlessly, the third one isn't applicable for me at least. In addition, I'd like to add that it also works if you wrap it in Doom's after! macro:

(after! lean4-mode
  (add-hook! 'lean4-mode-hook
    ...)
)

[mekeor]

Thanks for the feedback. I think the best solution to this problem is to change the readme/manual and also mention it in the "Common Pitfalls" chapter. What do you think?

[Thrithralas]

I do believe that this should be highlighted somewhere, yes. I think adding it to common pitfalls is a great idea, though I do wonder, is this issue not fixable? This does not seem to be a problem with other major modes.

[mekeor]

Other major modes don't have lsp command as member of the initial value of their -mode-hook variable. For Lean4-Mode this is currently the case because it deeply depends on lsp-mode. This might change in the future.

[mekeor]

In fact, the -mode-hook variable of most major modes is initialized to nil.

I think for Lean4-Mode, it makes sense to use lean4-mode-hook as an entry point for modularity and customizability. Even in the long run, its initialization value might be non-nil, that is, it might include sane, but easily customizable defaults.