Don't depend on lsp-mode (by splitting into multiple packages?)

[mekeor]

Problem / Goal

lean4-mode currently depends on lsp-mode. But there is this fork by @bustercopley and this fork by myself, each of which do not depend on lsp-mode (but rather use Emacs' built-in Eglot as LSP client).

Allowing users to choose Eglot as LSP client is tracked in this issue. A first step in this direction would be the removal of the hard dependency on lsp-mode.

Implementation Suggestion: Split into Multiple Packages

In order to achieve this, I suggest to split lean4-mode into two packages:

• A package called lean4-mode which does not depend on lsp-mode and which would, in the first step, not support LSP-backed features at all.
• A package called lean4-lsp-mode (or similar) which would depend on lsp-mode and, when installed, would (via autoloading) enable LSP-backed features via lsp-mode.

Since the only reason for the current lean4-mode to depend on the package magit-section comprises solely of the implementation of Lean4 Info View, which is a "LSP-backed feature", lean4-mode would not depend on magit-section, but lean4-lsp-mode would.

Multi-Package Repository

It's not uncommon for Git repositories to contain multiple Elpa packages. This can, e.g., be done with *-pkg.el files. Additionally, we could also reflect the fact that the repository contains multiple packages in the directory structure, for example:

.
├── lean4-lsp-mode/
└── lean4-mode/

Breaking Changes for Current Users?

This implementation would come with some breaking changes for current users of lean4-mode who want it to work just like like it currently does:

• They would need to install another package, namely lean4-lsp-mode.
• Since some identifiers (of variables and functions) would be renamed, they might need to adapt these renamings in their Emacs initialization file.

Blocking Melpa

Note that this issue is the current reason why lean4-mode hasn't been added to MELPA as you can read in this comment and as it has been requested in this issue.