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

@@ -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"

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

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

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}"