nixos/nixpkgs.git - Nix Packages collection

Age	Commit message (Collapse)	Author
2026-04-01	leanPackages: structural reimagining — own toolchain, lake --packages, ↵	Nadja Yang
	Hydra visibility 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
2026-03-21	leanPackages: init at 4.28.0	Nadja Yang
	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.