nixos/nixpkgs.git/pkgs/development/lean-modules/importGraph/default.nix, branch master Nix Packages collection leanPackages: structural reimagining — own toolchain, lake --packages, Hydra visibility 2026-04-01T15:13:44+00:00 Nadja Yang nadja@njy.dev 2026-03-28T17:53:22+00:00 3c2a3b804d85fde7c4c00a2cdc2da85bd75743e5 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: https://github.com/leanprover/lean4/commit/a145b9c11a0fe38fd4c921024a7376c99cc34bd2 
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:
https://github.com/leanprover/lean4/commit/a145b9c11a0fe38fd4c921024a7376c99cc34bd2
leanPackages: init at 4.28.0 2026-03-21T21:52:54+00:00 Nadja Yang git@njy.dev 2026-03-08T18:45:26+00:00 84206e18a3e959616861aaf5d71649556d1bcca5 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. 
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.