leanPackages.mathlib: harmonize output with Hydra strictures via artifact pre-densification

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"),
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

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
+  ''

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;
 })