From bdea40b4edb984318832ebbf14b9a3afac2ff6c1 Mon Sep 17 00:00:00 2001 From: Nadja Yang Date: Wed, 3 Jun 2026 17:04:11 -0400 Subject: [PATCH] leanPackages.mathlib: lgz preprocessing Per-module leantar strips olean structural overhead. See https://github.com/NixOS/nixpkgs/pull/511524#issuecomment-4615610073 --- pkgs/build-support/lake/default.nix | 3 ++ pkgs/by-name/le/leangz/package.nix | 8 ++++- .../lean-modules/mathlib/default.nix | 36 ++++++++++++------- pkgs/development/lean-modules/update.sh | 14 +++----- 4 files changed, 39 insertions(+), 22 deletions(-) diff --git a/pkgs/build-support/lake/default.nix b/pkgs/build-support/lake/default.nix index 48af90f70c6d..e802ec6a9d4e 100644 --- a/pkgs/build-support/lake/default.nix +++ b/pkgs/build-support/lake/default.nix @@ -112,6 +112,7 @@ lib.extendMkDerivation { in { strictDeps = true; + __structuredAttrs = true; nativeBuildInputs = nativeBuildInputs ++ [ lean4 @@ -194,6 +195,8 @@ lib.extendMkDerivation { find "$out/.lake/build/ir" -name '*.setup.json' -delete fi + rm -rf "$out/.lake/config" + # Setup hook propagates LEAN_PATH to downstream packages. mkdir -p "$out/nix-support" cp ${./setup-hook.sh} "$out/nix-support/setup-hook" diff --git a/pkgs/by-name/le/leangz/package.nix b/pkgs/by-name/le/leangz/package.nix index 5af5edd28e53..9d278567070f 100644 --- a/pkgs/by-name/le/leangz/package.nix +++ b/pkgs/by-name/le/leangz/package.nix @@ -2,15 +2,17 @@ lib, rustPlatform, fetchFromGitHub, + versionCheckHook, }: rustPlatform.buildRustPackage (finalAttrs: { pname = "leangz"; + # nixpkgs-update: no auto update version = "0.1.19"; # Should match LEANTAR_VERSION in leanprover/lean4/CMakeLists.txt src = fetchFromGitHub { owner = "digama0"; repo = "leangz"; - rev = "v${finalAttrs.version}"; + tag = "v${finalAttrs.version}"; hash = "sha256-kDvaydStWiJYCmKjoU39tuOQHNw5Zo577GeAvlENO2o="; }; @@ -18,10 +20,14 @@ rustPlatform.buildRustPackage (finalAttrs: { __structuredAttrs = true; + nativeInstallCheckInputs = [ versionCheckHook ]; + doInstallCheck = true; + meta = { description = "Lean 4 .olean file (de)compressor"; homepage = "https://github.com/digama0/leangz"; license = lib.licenses.asl20; maintainers = with lib.maintainers; [ niklashh ]; + mainProgram = "leantar"; }; }) diff --git a/pkgs/development/lean-modules/mathlib/default.nix b/pkgs/development/lean-modules/mathlib/default.nix index aea15d0e06d2..36e3222f0033 100644 --- a/pkgs/development/lean-modules/mathlib/default.nix +++ b/pkgs/development/lean-modules/mathlib/default.nix @@ -2,7 +2,7 @@ lib, buildLakePackage, runCommand, - xz, + leangz, fetchFromGitHub, batteries, aesop, @@ -15,6 +15,8 @@ }: let + leangz-raw = leangz.overrideAttrs { cargoBuildNoDefaultFeatures = true; }; + mathlib__archive = buildLakePackage (finalAttrs: { pname = "lean4-mathlib"; # nixpkgs-update: no auto update @@ -38,17 +40,23 @@ let importGraph ]; - nativeBuildInputs = [ xz ]; + nativeBuildInputs = [ leangz-raw ]; - # 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. + # Per-module lgz preprocessing strips olean structural overhead, + # providing significant compression benefit over a raw xz invocation. + # This also brings the output under Hydra's max_output_size. The + # user-facing mathlib derivation unpacks transparently. postInstall = '' - tar cf - -C "$out" . | xz -T0 > "$TMPDIR/archive.tar.xz" - rm -rf "$out" - mkdir -p "$out" - mv "$TMPDIR/archive.tar.xz" "$out/" + local lib="$out/.lake/build/lib/lean" + local ir="$out/.lake/build/ir" + find "$lib" -name '*.trace' -print0 \ + | xargs -0 -P"$NIX_BUILD_CORES" -I{} bash -c ' + base="''${1%.trace}"; rel="''${base#'"$lib"'/}" + leantar -C "'"$lib"'" -C "'"$ir"'" "$base.ltar" \ + "$rel.trace" "$rel.olean" "$rel.olean.server" "$rel.olean.private" \ + "$rel.ilean" -i 1 "$rel.c" + rm "$base".{trace,olean,olean.server,olean.private,ilean} "'"$ir"'/$rel.c" + ' _ {} ''; meta = { @@ -62,7 +70,7 @@ in runCommand mathlib__archive.name { - nativeBuildInputs = [ xz ]; + nativeBuildInputs = [ leangz-raw ]; passthru = { inherit mathlib__archive; inherit (mathlib__archive) @@ -84,5 +92,9 @@ runCommand mathlib__archive.name } '' mkdir -p $out - xz -dT0 < ${mathlib__archive}/archive.tar.xz | tar xf - -C $out + cp -rT ${mathlib__archive} $out + chmod -R u+w $out + find $out/.lake/build/lib -name '*.ltar' \ + -exec leantar -C $out/.lake/build/lib/lean -C $out/.lake/build/ir -x {} + + find $out/.lake/build/lib -name '*.ltar' -delete '' diff --git a/pkgs/development/lean-modules/update.sh b/pkgs/development/lean-modules/update.sh index 4ba4372b0c4c..76691bb6b475 100755 --- a/pkgs/development/lean-modules/update.sh +++ b/pkgs/development/lean-modules/update.sh @@ -1,19 +1,16 @@ #!/usr/bin/env nix-shell -#!nix-shell -i bash -p nix-update curl jq gh +#!nix-shell -i bash -p curl jq gh -# Usage: ./pkgs/development/lean-modules/update.sh [version] +# Updates the leanPackages dependency tree to match mathlib's +# lake-manifest.json for the current lean4 version. set -euo pipefail -lean4_version="${1:-$(curl -sL https://api.github.com/repos/leanprover/lean4/releases/latest | jq -r '.tag_name' | sed 's/^v//')}" +lean4_version=$(nix eval --raw .#leanPackages.lean4.version 2>/dev/null) dir=$(dirname "$0") FAKE="sha256-AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA=" -old_lean4=$(nix eval --raw .#leanPackages.lean4.version 2>/dev/null || echo "") - -nix-update leanPackages.lean4 --version="$lean4_version" - manifest=$(curl -sL "https://raw.githubusercontent.com/leanprover-community/mathlib4/v${lean4_version}/lake-manifest.json") known_deps="Cli LeanSearchClient Qq aesop batteries importGraph plausible proofwidgets" @@ -97,6 +94,5 @@ sed -i "0,/hash = \"sha256-[^\"]*\"/!{s|hash = \"sha256-[^\"]*\"|hash = \"$FAKE\ newhash=$(prefetch proofwidgets npmDeps) sed -i "s|$FAKE|$newhash|" "$dir/proofwidgets/default.nix" -echo "leanPackages.lean4: $old_lean4 -> $lean4_version" +echo "leanPackages: updated dependency tree for lean4 $lean4_version" echo "https://github.com/leanprover-community/mathlib4/blob/v${lean4_version}/lake-manifest.json" -echo "https://github.com/leanprover/lean4/releases/tag/v${lean4_version}"