doc: add Lean 4 section to languages-frameworks manual

doc/languages-frameworks/index.md

@@ -79,6 +79,7 @@ ios.section.md
 java.section.md
 javascript.section.md
 julia.section.md
+lean4.section.md
 lisp.section.md
 lua.section.md
 maven.section.md

doc/languages-frameworks/lean4.section.md

@@ -0,0 +1,51 @@
+# Lean 4 {#sec-language-lean4}
+
+Lean 4 is a strict functional language with dependent types. `leanPackages` provides the toolchain and a curated set of libraries — including the full mathlib dependency tree — with its own Lean toolchain. A standalone compiler is also available as `pkgs.lean4` for use outside the package set.
+
+## Building Lean 4 projects with `buildLakePackage` {#lean4-buildLakePackage}
+
+```nix
+leanPackages.buildLakePackage {
+  pname = "my-project";
+  version = "0.1.0";
+  src = ./.;
+  leanDeps = with leanPackages; [ mathlib ];
+  lakeHash = null; # all deps nix-managed; set to lib.fakeHash for Lake-managed deps
+}
+```
+
+Dependencies are declared in the lakefile for Lake and in the Nix expression for Nix. `leanDeps` provides Nix-managed libraries whose `.olean` files — the default build artifact of the Lake library facet — are reused without recompilation. `buildLakePackage` injects them via `lake --packages`, which takes precedence over Lake's own dependency resolution, producing a hermetic build.
+
+Sui generis among nixpkgs builders, `buildLakePackage` supports heterogeneous dependency resolution, in that Nix transparently substitutes for upstream-managed dependencies at per-package granularity: Nix-managed dependencies via `leanDeps` and Lake-managed dependencies via `lakeHash` compose in the same derivation. Setting `lakeHash = lib.fakeHash` and building will report the expected hash for a fixed-output derivation that pins what Lake would normally fetch, less Nix-managed dependencies. Nix-managed dependencies take precedence by name — so moving a dependency from `lakeHash` to `leanDeps` will change the expected hash — providing an on-ramp for projects to incrementally adopt nix-managed libraries. Setting `lakeHash = null` (the default) declares that all dependencies are Nix-managed and no fixed-output fetch is performed during the build.
+
+A `lake-manifest.json` is required at the project root. If all dependencies are Nix-managed, an empty manifest suffices:
+
+```json
+{"version":"1.1.0","packagesDir":".lake/packages","packages":[]}
+```
+
+## Development shells {#lean4-dev-shells}
+
+In `nix develop`, the scoped `lean4` and `buildLakePackage` provide the same toolchain used for hermetic builds. Note that Lake's normal dependency resolution is available in the shell — Lake may fetch dependencies not covered by `leanDeps` from the network, as is standard for Nix development shells.
+
+## The `leanPackages` scope {#lean4-leanPackages}
+
+`leanPackages` is a `lib.makeScope` with its own `lean4`. Overriding it propagates to all packages and to `buildLakePackage`:
+
+```nix
+leanPackages.overrideScope (
+  self: super: {
+    lean4 = myCustomLean4;
+  }
+)
+```
+
+The `lean4` supplied by `leanPackages` is binary-patched to ensure that the Lean language server discovers the wrapped `lake` rather than an unwrapped one. This is necessary because Lake's `serve` subcommand has a vexing invocation pattern: it derives `LAKE` from `IO.appPath` and unconditionally sets it in the spawned environment, bypassing any wrapper. The binary patch rewrites store path references so that this discovery mechanism finds the correct binary, enabling LSP integration — including the InfoView, which requires Lean-specific protocol extensions — without improper mutation of the user's project directory.
+
+Note that `leanPackages.lean4` supplants Lake's built-in cache invalidation for dependencies in `/nix/store/`, deferring entirely to Nix's bespoke dependency model. Lake's trace validation — which checks compiler "hash," platform, and package identity — is gracefully subsumed by guarantees Nix already provides. Cache coherence responsibilities are delegated to the orchestrator of streamlined Nix integration.
+
+For Emacs, `emacsPackages.nael` and `emacsPackages.nael-lsp` (eglot-based and lsp-mode-based respectively, available via MELPA) provide Lean 4 support including proof state display via eldoc. For VSCode (unfree) / VSCodium, `vscode-extensions.leanprover.lean4` is available. Editor packages discover the toolchain from `PATH`.
+
+## Relationship to earlier Lean 4 Nix support {#lean4-history}
+
+Users familiar with the per-module derivation approach (2020–2025) should note that `buildLakePackage` follows a different architecture. The earlier integration discovered dependencies at evaluation time via import-from-derivation — an ambitious attempt to reconcile declarative package management with fine-grained build semantics, ultimately undermined by Nix's own evaluation model. It was [removed upstream](https://github.com/leanprover/lean4/commit/535435955b482176e8d62a54deebcacdec0827db). `buildLakePackage` treats Lake as a build driver and uses Nix for package-level boundaries, while `nix develop` and `nix-shell` achieve feature parity with the vanilla Lake development experience.

doc/redirects.json

@@ -3576,6 +3576,9 @@
   "sec-language-java": [
     "index.html#sec-language-java"
   ],
+  "sec-language-lean4": [
+    "index.html#sec-language-lean4"
+  ],
   "language-javascript": [
     "index.html#language-javascript"
   ],
@@ -3744,6 +3747,18 @@
   "julia-withpackage-arguments": [
     "index.html#julia-withpackage-arguments"
   ],
+  "lean4-buildLakePackage": [
+    "index.html#lean4-buildLakePackage"
+  ],
+  "lean4-dev-shells": [
+    "index.html#lean4-dev-shells"
+  ],
+  "lean4-history": [
+    "index.html#lean4-history"
+  ],
+  "lean4-leanPackages": [
+    "index.html#lean4-leanPackages"
+  ],
   "lisp": [
     "index.html#lisp"
   ],