Status of this project and relation to `nael-mode`

[dschrempf]

Hello!

What is the status of lean4-mode, and how does it relate to nael-mode?

In my experience, nael-mode worked much better than lean4-mode, and given the small size of our community I suggest focussing on one project. However, there may be things I don't know about. You tell me!

[dschrempf]

Until development picks up again: I suggest using nael-mode. It works well and is actively developed!

[t-c-acc]

Hello!

What is the status of lean4-mode, and how does it relate to nael-mode?

In my experience, nael-mode worked much better than lean4-mode, and given the small size of our community I suggest focussing on one project. However, there may be things I don't know about. You tell me!

I thought nael-mode was abandoned in favour of lean4-mode. Does it currently work with egolt instead of lsp-mode?

I am an Emacs user (mainly Auctex...), and I do not want to get into configuring lsp-mode, and I have downloaded VSCodium (disgusting :P) to learn Lean...

[dschrempf]

nael-mode works with eglot, and is maintained! I can recommend using it!

[mekeor]

What is the status of lean4-mode, and how does it relate to nael-mode?

Here's the story: First, there was lean4-mode. Since people wanted Eglot-support, they built forks. I forked lean4-mode too, and radically refactored it with focus on minimalism, modularity and integration into Emacs core. I called my fork Nael. I regarded it as proof of concept.

Later, I decided to contribute to lean4-mode itself. It was hard to get in touch with the maintainer. But with personal connections, I finally got write-access to the repository. I even archived/obsoleted Nael.

Unfortunately, my development on lean4-mode was decelerated by slow feedback-loops for PRs. From my perspective, lean4-mode is not maintained.

I thought nael-mode was abandoned in favour of lean4-mode. Does it currently work with egolt instead of lsp-mode?

As a consequence, I re-activated Nael. I'm currently working actively on it, but I cannot promise to maintain it in the long run. It works fine for me, with no LSP, with Eglot, or with lsp-mode.