From fb169268a384200bb133bfdcf4d556a5437dd380 Mon Sep 17 00:00:00 2001 From: Nadja Yang Date: Fri, 24 Apr 2026 12:17:00 -0400 Subject: [PATCH] leanPackages.mathlib: harmonize output with Hydra strictures via artifact pre-densification MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 bbd0655ae828 (2024) ("[intending] to replace the `passthru.data-compressed` derivations that ha[d] accumulated in nixpkgs with something more reusable"), https://github.com/NixOS/nixpkgs/commit/bbd0655ae828b9f1cf39d891b52aa6506394ef46 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"), https://github.com/NixOS/nixpkgs/blob/fc1f8110e84b7a874826eee147170aee85082390/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"), https://github.com/NixOS/nixpkgs/blob/4dc9b83879ce51e180f37acb8e78ededdbf72798/pkgs/by-name/gc/gclient2nix/gclient2nix.py#L162-L167 [1] NixOS Infrastructure Cap., https://github.com/NixOS/infra/blob/170012a4682da0a130f6bc68caf3618743239783/build/hydra.nix#L116 --- .../lean-modules/mathlib/default.nix | 104 ++++++++++++------ pkgs/top-level/lean-packages.nix | 1 + 2 files changed, 70 insertions(+), 35 deletions(-) diff --git a/pkgs/development/lean-modules/mathlib/default.nix b/pkgs/development/lean-modules/mathlib/default.nix index 6c70a6048613..adfce0b79ed6 100644 --- a/pkgs/development/lean-modules/mathlib/default.nix +++ b/pkgs/development/lean-modules/mathlib/default.nix @@ -1,6 +1,8 @@ { lib, buildLakePackage, + runCommand, + xz, fetchFromGitHub, batteries, aesop, @@ -12,43 +14,75 @@ tests, }: -buildLakePackage (finalAttrs: { - pname = "lean4-mathlib"; - # nixpkgs-update: no auto update - version = "4.29.1"; +let + mathlib__archive = buildLakePackage (finalAttrs: { + pname = "lean4-mathlib"; + # nixpkgs-update: no auto update + version = "4.29.1"; - src = fetchFromGitHub { - owner = "leanprover-community"; - repo = "mathlib4"; - tag = "v${finalAttrs.version}"; - hash = "sha256-K/QPTOytsV+OX25xyKlspeB9G0a28IjmJxcUAKXFP9U="; - }; + src = fetchFromGitHub { + owner = "leanprover-community"; + repo = "mathlib4"; + tag = "v${finalAttrs.version}"; + hash = "sha256-K/QPTOytsV+OX25xyKlspeB9G0a28IjmJxcUAKXFP9U="; + }; - leanPackageName = "mathlib"; - leanDeps = [ - batteries - aesop - Qq - proofwidgets - plausible - LeanSearchClient - importGraph - ]; + leanPackageName = "mathlib"; + leanDeps = [ + batteries + aesop + Qq + proofwidgets + plausible + LeanSearchClient + importGraph + ]; - requiredSystemFeatures = [ "big-parallel" ]; + nativeBuildInputs = [ xz ]; - passthru.tests = { - inherit (tests.lake) weak-minimax; - }; + # Compress the installed output into an xz archive so the derivation + # fits Hydra's max_output_size. The user-facing mathlib derivation + # decompresses transparently from this archive, at the de minimis + # compliance cost of nested compression. + postInstall = '' + tar cf - -C "$out" . | xz -T0 > "$TMPDIR/archive.tar.xz" + rm -rf "$out" + mkdir -p "$out" + mv "$TMPDIR/archive.tar.xz" "$out/" + ''; - meta = { - description = "Mathematical library for Lean 4"; - homepage = "https://github.com/leanprover-community/mathlib4"; - license = lib.licenses.asl20; - # Output exceeds Hydra's 4 GiB NAR size limit. Oleans compress well with - # zstd (~70% ratio); a squashfs-packaged output would fit, pending upstream - # support or a raised limit. - hydraPlatforms = [ ]; - maintainers = with lib.maintainers; [ nadja-y ]; - }; -}) + meta = { + description = "Mathematical library for Lean 4"; + homepage = "https://github.com/leanprover-community/mathlib4"; + license = lib.licenses.asl20; + maintainers = with lib.maintainers; [ nadja-y ]; + }; + }); +in + +runCommand mathlib__archive.name + { + nativeBuildInputs = [ xz ]; + passthru = { + inherit mathlib__archive; + inherit (mathlib__archive) + src + version + lakePackageName + lean4 + allLeanDeps + computedLakeDeps + overrideLakeDepsAttrs + ; + tests = { + inherit (tests.lake) weak-minimax; + }; + }; + meta = mathlib__archive.meta // { + hydraPlatforms = [ ]; + }; + } + '' + mkdir -p $out + xz -dT0 < ${mathlib__archive}/archive.tar.xz | tar xf - -C $out + '' diff --git a/pkgs/top-level/lean-packages.nix b/pkgs/top-level/lean-packages.nix index 7bdc715217cb..e52697bf149b 100644 --- a/pkgs/top-level/lean-packages.nix +++ b/pkgs/top-level/lean-packages.nix @@ -21,4 +21,5 @@ lib.makeScope newScope (self: { Cli = self.callPackage ../development/lean-modules/Cli { }; importGraph = self.callPackage ../development/lean-modules/importGraph { }; mathlib = self.callPackage ../development/lean-modules/mathlib { }; + inherit (self.mathlib.passthru) mathlib__archive; })