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)
Lean binaries derive sysroot from IO.appPath; patch all of them
rather than just lean and lake. Add cadical to symlinkJoin paths
instead of bundling a copy via INSTALL_CADICAL.
ed10debb3c
Strip ephemeral setup.json build artifacts from library outputs.
These are produced per-module during compilation and not included
in upstream cache distributions
(https://github.com/NixOS/nixpkgs/issues/510957).
Disable Hydra builds for mathlib since the output exceeds the NAR
size limit.
Pre-build static library for batteries so downstream executables
can link against it.
Refactor update.sh to pin each dependency to the rev from mathlib's
lake-manifest.json.
By default, lean4's cmake copies the cadical binary from PATH to its
build output directory. Disabling this behavior does not keep Lean from
using cadical.
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.
