Give leanPackages its own lean4, independent of pkgs.lean4. Binary-
patch the toolchain so the language server discovers the wrapped lake
despite lake serve deriving LAKE from IO.appPath unconditionally.
Supplant Lake's config trace validation for /nix/store/ dependencies,
deferring cache coherence to Nix.
Migrate Nix-managed dependency injection from package-overrides.json
to lake --packages. Patch Cli to pre-build static library for
downstream executables. Add recurseIntoAttrs for Hydra.
Upstream accepted FetchContent for mimalloc vendoring:
a145b9c11a
Verifies that buildLakePackage works with nix-only deps (no
lake-manifest.json). Builds a proof of the weak minimax inequality
from Mathlib.Order.CompleteLattice.Basic using leanDeps = [ mathlib ].
Lean 4 package set providing the mathlib dependency tree:
batteries, aesop, Qq, proofwidgets, plausible, LeanSearchClient,
Cli, importGraph, and mathlib itself.
All lockstep packages are versioned with lean4. ProofWidgets and
LeanSearchClient follow their own versioning, pinned via mathlib's
lake-manifest.json.
Includes update.sh which updates all packages to match the lean4
version in nixpkgs, with a dependency-set check to detect upstream
changes.
