mirror of
https://github.com/NixOS/nixpkgs.git
synced 2026-06-05 21:03:40 +00:00
fb169268a3
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. tobbd0655ae8(2024) ("[intending] to replace the `passthru.data-compressed` derivations that ha[d] accumulated in nixpkgs with something more reusable"),bbd0655ae8Cf. 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)
26 lines
1.1 KiB
Nix
26 lines
1.1 KiB
Nix
# Lean 4 package set with its own toolchain (independent of pkgs.lean4).
|
|
#
|
|
# Override the toolchain for the entire set:
|
|
# leanPackages.overrideScope (self: super: { lean4 = lean4-custom; })
|
|
{
|
|
lib,
|
|
newScope,
|
|
}:
|
|
|
|
lib.makeScope newScope (self: {
|
|
lean4 = self.callPackage ../development/lean-modules/lean4 { };
|
|
|
|
buildLakePackage = self.callPackage ../build-support/lake { };
|
|
|
|
batteries = self.callPackage ../development/lean-modules/batteries { };
|
|
aesop = self.callPackage ../development/lean-modules/aesop { };
|
|
Qq = self.callPackage ../development/lean-modules/Qq { };
|
|
proofwidgets = self.callPackage ../development/lean-modules/proofwidgets { };
|
|
plausible = self.callPackage ../development/lean-modules/plausible { };
|
|
LeanSearchClient = self.callPackage ../development/lean-modules/LeanSearchClient { };
|
|
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;
|
|
})
|