Proposal
Would you be open to a pull request that splits leanprover.lean4 into multiple smaller extensions?
- leanprover.lean4-online: contains functionality that requires external communication, like installing and updating lean/elan/libs. And Loogle. (Possibly splitting further into "loogle" and "installer".)
- leanprover.lean4-toml: split out lakefile.toml schema validation, which currently depends on Even Better TOML.
- leanprover.lean4-core: everything else
- leanprover.lean4: this becomes an extension pack to bundle the prior extensions.
leanprover.lean4 today is a single extension that mixes:
- Always-needed functionality — language client, infoview, hover, abbreviation input, gutter, project info, manual viewer, setup diagnostics.
- Network-touching auto-installer — elan-init download, OS dep installs, GitHub release queries.
- Network-touching project operations —
lake update, lake exe cache get, lake resolve-deps, "Download Project" (git clone).
- A webview talking to an online service — Loogle (
loogle.lean-lang.org).
- A hard
extensionDependencies on tamasfe.even-better-toml for the lakefile.toml JSON schema contribution.
Settings stay under the shared lean4.* namespace — each sub-extension reads the subset it needs, so existing configs keep working unchanged.
For ordinary users this is fine. For users that are security-conscious or use Lean at a company that blocks such things, it's not.
The clean fix is to give users opt-out granularity at the extension level. The umbrella pack reuses the existing leanprover.lean4 marketplace ID, so existing installs upgrade transparently and the default user experience is identical.
Related issues
Splitting out Even Better TOML has been discussed before. #706 proposed dropping it, but was closed because
Not shipping language server support for lakefile.toml by default is not an option. Even Better Toml provides auto-completion (including docs for each option) in lakefile.toml, which is essential for discoverability.
I believe including support as a separate extension satisfies this need.
Issue #787 discusses replacing it with Tombi, and possibly using an extension pack.
Community Feedback
I have not brought this up on Lean Zulip because I wasn't able to find other discussions relating to the design of this extension and think the refactor I'm proposing is orthogonal to Lean itself. But I'm happy to do so if you prefer.
Proposal
Would you be open to a pull request that splits
leanprover.lean4into multiple smaller extensions?leanprover.lean4today is a single extension that mixes:lake update,lake exe cache get,lake resolve-deps, "Download Project" (git clone).loogle.lean-lang.org).extensionDependenciesontamasfe.even-better-tomlfor thelakefile.tomlJSON schema contribution.Settings stay under the shared
lean4.*namespace — each sub-extension reads the subset it needs, so existing configs keep working unchanged.For ordinary users this is fine. For users that are security-conscious or use Lean at a company that blocks such things, it's not.
The clean fix is to give users opt-out granularity at the extension level. The umbrella pack reuses the existing
leanprover.lean4marketplace ID, so existing installs upgrade transparently and the default user experience is identical.Related issues
Splitting out Even Better TOML has been discussed before. #706 proposed dropping it, but was closed because
I believe including support as a separate extension satisfies this need.
Issue #787 discusses replacing it with Tombi, and possibly using an extension pack.
Community Feedback
I have not brought this up on Lean Zulip because I wasn't able to find other discussions relating to the design of this extension and think the refactor I'm proposing is orthogonal to Lean itself. But I'm happy to do so if you prefer.