Add support for eglot language server

[sgpthomas]

I prefer to use the eglot language server implementation over lsp-mode. It would be nice to have an option to set which language server to use, or to make the mode independent of the language server.

[odanoburu]

Are you open to a PR adding this? Usually packages don't need to depend on lsp-mode or eglot directly, but I guess Lean's interactivity might make it necessary. It does seem like eglot's more bare-bones features might make it harder to support; if anyone has tried it before and knows any pitfalls I'd be happy to read about it!

[Kha]

Are you open to a PR adding this?

Sure!

[akirak]

I've had a look at the source of this package, but lean4-fringe.el and lean4-info.el are tightly integrated with lsp-mode, while the other parts of the package would work without lsp (after slight modifications). It looks hard to rewrite the two files to support eglot. It would be nice if they were provided as a separate package (like lean4-lsp), while the main package were agnostic to lsp client.

I have already made an experiment to separate the two files out (see https://github.com/akirak/lean4-mode/commits/modular). It works without lsp, but I haven't tried if it works with eglot yet.

[odanoburu]

@akirak I think the way to go would be to have lsp as an optional dependency, so that we don't need to have separate packages for distribution, as in https://github.com/alphapapa/emacs-package-dev-handbook#optional-support

I've done something similar to you for my personal use and it fit the bill, but it's not fit as a contribution since it removed a lot of features (I didn't have the time to make something abstracting out lsp-mode)

[akirak]

@odanoburu The basic lsp integration should be part of lsp-mode (in clients directory), because that's what other languages appear to do. Regarding other advanced features that depend on lsp-mode, you could move them into lsp-mode, like yaml does, but I think it depends on how you would want to develop and maintain them.

It would be possible to have lsp as an optional dependency. You will probably want to continue using those lsp features while waiting for registration to MELPA, so gradual transition (i.e. first making lsp support optional and then moving into the repository of lsp) may be a good idea.

[librarianmage]

I'd be extremely grateful if support was added :)

[urkud]

What's so cool about eglot (never tried, so asking) that it beats Lean info view and orange bars?

[librarianmage]

@urkud I prefer eglot over lsp-mode for a few reasons, but one of my primary reasons is that it integrates more with various Emacs functionality instead of creating its own stuff

[leahneukirchen]

One significant reason could be that eglot is included in Emacs 29.1 and later.

I don't think that the info display is an advanced feature, however, it's pretty essential to use Lean.

[m4lvin]

On Zulip this was mentioned but not here, so maybe it's good to add a link: The fork by @bustercopley works well enough with eglot: https://github.com/bustercopley/lean4-mode

[leahneukirchen]

On a quick test, this works great. Thanks for pointing it out!

[zmberber]

Just here to voice my support for adding eglot support, and making that the default, for all of the reasons mentioned above by others. The fork by @bustercopley is cool!

I have no idea how "deep" the lsp-mode dependency goes. Even though the fork works, I assume it is not as easy as just merging that fork and have everything be fine from a design standpoint, and also that would probably mean an immediate design shift for the developers of lean4-mode.el. Which I would actually like, but it is probably not that simple.

I wish for this project to advance, and I love the idea of having lsp-mode.el as an optional dependency.

[mekeor]

I forked bustercopley/lean4-mode, called it Nael and made it more minimalist by sticking to Emacs' built-in facilities like Eglot but also ElDoc and Project.

(Nael is currently available at codeberg.org/mekeor/nael but if it gets renamed, its new name and URL should be mentioned in this PR to Melpa.)

For convenience, I'll copy-paste the Comparison section from Nael's readme here:

• Nael does not depend on third-party lsp-mode. Instead, you can optionally use Nael together with Emacs' built-in LSP-client Eglot.
• Nael does not offer any special buffer for information on the current goal etc. Instead, Nael introduces two ElDoc documentation functions which will show up in the usual ElDoc buffer.
• Nael does not offer any special mechanism to detect the current project. Instead, it introduces Lakefiles as Project root markers.
• Nael does not offer any special command to build the current project. Instead, it configures the built-in project-compile command to work.
• Nael does not offer any special input-method. Instead, you may use the built-in TeX input-method or the unicode-math from the external unicode-math-input package.
• Nael does not solely use the Apache-2 license. Instead, it is licensed partly under Apache-2, and partly under GPLv3+. Altogether, you can treat Nael as if it was under GPLv3+ since that's the stricter license.

When opened a PR to Melpa to add Nael, I was asked if we should rename Nael to "lean-mode" and what I think about lean4-mode and its long-lasting open Melpa-PR. I wrote some of my thoughts down about that in this comment: https://github.com/melpa/melpa/pull/9098#issuecomment-2230656747

I'm sorry that I just forked lean4-mode without contacting the leanprover-community first. To be honest, I didn't have the patience to tackle all the deficiencies that I saw in the code base one by one, with separate PRs each.

To me it seems to Do The Right Thing, we should bring back the improvements from Nael to lean4-mode. But for this purpose, we'd need to discuss many things. (For instance, we'd need to discuss if we want to keep a Lean Info View or integration into ElDoc suffices even if we'd need to sacrifice a minor feature.) The whole process would require a lot communication, decision makin, refactoring, coding and time.

Writing down this comment itself has been insightful for me. The more I think about it, the more I'm willing to sacrifice myself for bringing back Nael's modularity and humility to lean4-mode.

Let me know about your feelings, desires, angers, wishes, concerns, plans and idea in regard to these topics. :D

[zmberber]

omg that is really awesome! i'll definitely try it out, thank you so much!