Rejecting an unwieldy originalist interpretation of the max_output_size
infrastructure mandate [1] — which, by checking NAR size pre-compression,
might be read to foreclose in-NAR densification — this commit resolves
the tension between binary cache availability and statutory size
discipline through equitable artifact pre-densification.
Specifically, we execute xz compression during the postInstall phase
of an intermediate derivation, coupled with a non-Hydra wrapper that
decompresses the payload transparently. This insulates end-users from
the underlying .tar.xz monolith while satisfying the strict procedural
requirements of the build farm's sensors.
We acknowledge reservations regarding the broader applicability of the
unorthodox pattern incepted herein.
See also Jakštys, commit msg. to bbd0655ae8 (2024) ("[intending]
to replace the `passthru.data-compressed` derivations that ha[d]
accumulated in nixpkgs with something more reusable"),
bbd0655ae8
Cf. Luna Nova, hipblaslt/default.nix ll. 113-114 (2026) (patching
hipblaslt C++ runtime to transparently decompress zstd-compressed
.dat files, as "required to keep [the] output under [H]ydra size
limit"), fc1f8110e8/pkgs/development/rocm-modules/hipblaslt/default.nix (L113-L114)
Cf. SuperSandro2000, Review of NixOS/nixpkgs#511524 (this PR) (2026)
("[w]hy not compress the well compressable [.olean] files in nix
with zstd?") (in dicta; a fortiori),
https://github.com/NixOS/nixpkgs/pull/511524#discussion_r3137725277
But cf. Yureka, gclient2nix.py ll. 162-167 (2025) (characterizing
recompression as "bypassing the size limit (making it count the
compressed instead of uncompressed size) rather than complying with
it"), 4dc9b83879/pkgs/by-name/gc/gclient2nix/gclient2nix.py (L162-L167)
[1] NixOS Infrastructure Cap., 170012a468/build/hydra.nix (L116)
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
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.
