RFC: Split into multiple extensions; use extension pack to bundle

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.

Start by mapping the existing leanprover.lean4 extension and its extensionDependencies, then review how the listed always-needed, network, Loogle, and TOML capabilities are currently packaged. Define boundaries and dependency behavior for online, toml, core, and the umbrella extension; done means existing installs and settings remain compatible while users can opt out of network and TOML functionality. No files or tests are named, so locate the relevant packaging entry points first.