From 590ccdb420036ed0ab6bffde991b13f98ec0fe14 Mon Sep 17 00:00:00 2001
From: Nadja Yang <nadja@njy.dev>
Date: Wed, 3 Jun 2026 14:01:07 -0400
Subject: [PATCH 1/8] leanPackages: partially revert
 https://github.com/NixOS/nixpkgs/pull/526718/commits/a26b66330f6fa572e7005ee2a1eb031093456e6e

In favor of https://github.com/NixOS/nixpkgs/pull/511524
(https://github.com/NixOS/nixpkgs/pull/511524/commits/72b8bcfd8ef837cfddc1cacc0bd4c7b8b3998e59).

Retains pkgs.lean4 at 4.30.0.
---
 pkgs/development/lean-modules/Cli/default.nix | 11 ++++------
 .../lean-modules/LeanSearchClient/default.nix |  5 +----
 pkgs/development/lean-modules/Qq/default.nix  | 11 ++++------
 .../lean-modules/aesop/default.nix            | 11 ++++------
 .../lean-modules/batteries/default.nix        | 21 ++++---------------
 .../lean-modules/importGraph/default.nix      | 11 ++++------
 .../lean-modules/lean4/default.nix            | 16 +++++---------
 .../lean-modules/mathlib/default.nix          | 11 ++++------
 .../lean-modules/plausible/default.nix        | 11 ++++------
 .../lean-modules/proofwidgets/default.nix     |  5 +----
 10 files changed, 35 insertions(+), 78 deletions(-)

diff --git a/pkgs/development/lean-modules/Cli/default.nix b/pkgs/development/lean-modules/Cli/default.nix
index 07476219fea2..d3bc495ee9cf 100644
--- a/pkgs/development/lean-modules/Cli/default.nix
+++ b/pkgs/development/lean-modules/Cli/default.nix
@@ -6,13 +6,13 @@
 
 buildLakePackage {
   pname = "lean4-cli";
-  version = "4.30.0";
+  version = "4.29.0";
 
   src = fetchFromGitHub {
     owner = "leanprover";
     repo = "lean4-cli";
-    tag = "v4.30.0";
-    hash = "sha256-oMaqHvWlEfk1601JfNKPvkGIWgMW6tiF7Mej7g63vh0=";
+    tag = "v4.29.0";
+    hash = "sha256-jCUl4sXVmwtYPuQecEUFH6mwFzPaQY7au4624EOiWjk=";
   };
 
   leanPackageName = "Cli";
@@ -31,9 +31,6 @@ buildLakePackage {
     description = "Command-line argument parser for Lean 4";
     homepage = "https://github.com/leanprover/lean4-cli";
     license = lib.licenses.mit;
-    maintainers = with lib.maintainers; [
-      nadja-y
-      niklashh
-    ];
+    maintainers = with lib.maintainers; [ nadja-y ];
   };
 }
diff --git a/pkgs/development/lean-modules/LeanSearchClient/default.nix b/pkgs/development/lean-modules/LeanSearchClient/default.nix
index da6eaf0263d0..b7e25b5ecbd0 100644
--- a/pkgs/development/lean-modules/LeanSearchClient/default.nix
+++ b/pkgs/development/lean-modules/LeanSearchClient/default.nix
@@ -22,9 +22,6 @@ buildLakePackage {
     description = "Lean 4 client for LeanSearch and Moogle proof search";
     homepage = "https://github.com/leanprover-community/LeanSearchClient";
     license = lib.licenses.asl20;
-    maintainers = with lib.maintainers; [
-      nadja-y
-      niklashh
-    ];
+    maintainers = with lib.maintainers; [ nadja-y ];
   };
 }
diff --git a/pkgs/development/lean-modules/Qq/default.nix b/pkgs/development/lean-modules/Qq/default.nix
index a91693775347..6feb6fa51916 100644
--- a/pkgs/development/lean-modules/Qq/default.nix
+++ b/pkgs/development/lean-modules/Qq/default.nix
@@ -6,13 +6,13 @@
 
 buildLakePackage {
   pname = "lean4-Qq";
-  version = "4.30.0";
+  version = "4.29.0";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "quote4";
-    tag = "v4.30.0";
-    hash = "sha256-jVsRw/R7D7HmsE7vQvVeDXcnVerlcDBOrhf9FJJiXkY=";
+    tag = "v4.29.0";
+    hash = "sha256-pNY5hv1nJbreCfU4EewIHCpiryIBv1ghWibrUW8vnQ0=";
   };
 
   leanPackageName = "Qq";
@@ -21,9 +21,6 @@ buildLakePackage {
     description = "Lean 4 compile-time quote and antiquote macros for metaprogramming";
     homepage = "https://github.com/leanprover-community/quote4";
     license = lib.licenses.asl20;
-    maintainers = with lib.maintainers; [
-      nadja-y
-      niklashh
-    ];
+    maintainers = with lib.maintainers; [ nadja-y ];
   };
 }
diff --git a/pkgs/development/lean-modules/aesop/default.nix b/pkgs/development/lean-modules/aesop/default.nix
index f71d9e7c9f47..7d8ad308741a 100644
--- a/pkgs/development/lean-modules/aesop/default.nix
+++ b/pkgs/development/lean-modules/aesop/default.nix
@@ -7,13 +7,13 @@
 
 buildLakePackage {
   pname = "lean4-aesop";
-  version = "4.30.0";
+  version = "4.29.0";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "aesop";
-    tag = "v4.30.0";
-    hash = "sha256-7PhQVMdiYImuzRYdf0Kgw3JYS4nBLfILXxyhFH8Zag0=";
+    tag = "v4.29.0";
+    hash = "sha256-CNwxNig8OWjtfQRYyRnM/HGBn2oaNX5qP9CVT2eWNlg=";
   };
 
   leanPackageName = "aesop";
@@ -23,9 +23,6 @@ buildLakePackage {
     description = "White-box automation for Lean 4";
     homepage = "https://github.com/leanprover-community/aesop";
     license = lib.licenses.asl20;
-    maintainers = with lib.maintainers; [
-      nadja-y
-      niklashh
-    ];
+    maintainers = with lib.maintainers; [ nadja-y ];
   };
 }
diff --git a/pkgs/development/lean-modules/batteries/default.nix b/pkgs/development/lean-modules/batteries/default.nix
index 3e06e945f9fa..9fdb1efd8686 100644
--- a/pkgs/development/lean-modules/batteries/default.nix
+++ b/pkgs/development/lean-modules/batteries/default.nix
@@ -6,34 +6,21 @@
 
 buildLakePackage {
   pname = "lean4-batteries";
-  version = "4.30.0";
+  version = "4.29.0";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "batteries";
-    tag = "v4.30.0";
-    hash = "sha256-OOcKCQEgnn9zkkwjHOovMb/IprNomTDufLOfEXs7hFU=";
+    tag = "v4.29.0";
+    hash = "sha256-sEIDi2i2FaLTgKYWt/kzqPrjMdf+bFURfhw6ZZWBawQ=";
   };
 
   leanPackageName = "batteries";
 
-  # Pre-build static library for downstream executables.
-  # TODO: upstream this to batteries
-  postPatch = ''
-    substituteInPlace lakefile.toml \
-      --replace-fail '[[lean_lib]]
-    name = "Batteries"' '[[lean_lib]]
-    name = "Batteries"
-    defaultFacets = ["static"]'
-  '';
-
   meta = {
     description = "The batteries-included extended library for Lean 4";
     homepage = "https://github.com/leanprover-community/batteries";
     license = lib.licenses.asl20;
-    maintainers = with lib.maintainers; [
-      nadja-y
-      niklashh
-    ];
+    maintainers = with lib.maintainers; [ nadja-y ];
   };
 }
diff --git a/pkgs/development/lean-modules/importGraph/default.nix b/pkgs/development/lean-modules/importGraph/default.nix
index 6692a5f99ec2..4da481fd5a16 100644
--- a/pkgs/development/lean-modules/importGraph/default.nix
+++ b/pkgs/development/lean-modules/importGraph/default.nix
@@ -7,13 +7,13 @@
 
 buildLakePackage {
   pname = "lean4-importGraph";
-  version = "4.30.0";
+  version = "4.29.0";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "import-graph";
-    tag = "v4.30.0";
-    hash = "sha256-V3bGQxTNs2G4MqaVxRb6WED1a7VaHfEo1HgBNqPipz8=";
+    tag = "v4.29.0";
+    hash = "sha256-tqdO2qyWiJzEbK0yuu4+tiOXTEg9XJfGnI7z6Jh/abg=";
   };
 
   leanPackageName = "importGraph";
@@ -23,9 +23,6 @@ buildLakePackage {
     description = "Tools to analyse and visualise Lean 4 import structures";
     homepage = "https://github.com/leanprover-community/import-graph";
     license = lib.licenses.asl20;
-    maintainers = with lib.maintainers; [
-      nadja-y
-      niklashh
-    ];
+    maintainers = with lib.maintainers; [ nadja-y ];
   };
 }
diff --git a/pkgs/development/lean-modules/lean4/default.nix b/pkgs/development/lean-modules/lean4/default.nix
index 2e1c9b2f3c02..7ba6dd5170f4 100644
--- a/pkgs/development/lean-modules/lean4/default.nix
+++ b/pkgs/development/lean-modules/lean4/default.nix
@@ -8,18 +8,16 @@
   git,
   gmp,
   cadical,
-  leangz,
   pkg-config,
   libuv,
   perl,
   testers,
 }:
-let
-  cadical' = cadical.override { version = "2.1.3"; };
 
+let
   lean4 = stdenv.mkDerivation (finalAttrs: {
     pname = "lean4";
-    version = "4.30.0";
+    version = "4.29.0";
 
     mimalloc-src = fetchFromGitHub {
       owner = "microsoft";
@@ -32,7 +30,7 @@ let
       owner = "leanprover";
       repo = "lean4";
       tag = "v${finalAttrs.version}";
-      hash = "sha256-YTsfIppd6km7wOjAxRH5KMPsW++ztFDCJT2up72J86Q=";
+      hash = "sha256-0v4OTrCLdHBbWJUq7hIjJonqget9SvsG3izGlOwhwyU=";
     };
 
     # Vendor mimalloc. Upstream has since partially adopted FetchContent:
@@ -72,13 +70,12 @@ let
     nativeBuildInputs = [
       cmake
       pkg-config
-      leangz # Provides leantar
     ];
 
     buildInputs = [
       gmp
       libuv
-      cadical'
+      cadical
     ];
 
     nativeCheckInputs = [
@@ -106,10 +103,7 @@ let
       changelog = "https://github.com/leanprover/lean4/blob/${finalAttrs.src.tag}/RELEASES.md";
       license = lib.licenses.asl20;
       platforms = lib.platforms.all;
-      maintainers = with lib.maintainers; [
-        nadja-y
-        niklashh
-      ];
+      maintainers = with lib.maintainers; [ nadja-y ];
       mainProgram = "lean";
     };
   });
diff --git a/pkgs/development/lean-modules/mathlib/default.nix b/pkgs/development/lean-modules/mathlib/default.nix
index 60ae77331f02..70a34dd9f333 100644
--- a/pkgs/development/lean-modules/mathlib/default.nix
+++ b/pkgs/development/lean-modules/mathlib/default.nix
@@ -14,13 +14,13 @@
 
 buildLakePackage {
   pname = "lean4-mathlib";
-  version = "4.30.0";
+  version = "4.29.0";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "mathlib4";
-    tag = "v4.30.0";
-    hash = "sha256-RxOxdUiVUAxUbfVhxlkjmPX1V64EtmIIn1eW75TiJWA=";
+    tag = "v4.29.0";
+    hash = "sha256-fe+qS7gNxdLnACX3/jqToa9m7r1gbskY6kDJbm1ZefE=";
   };
 
   leanPackageName = "mathlib";
@@ -44,9 +44,6 @@ buildLakePackage {
     description = "Mathematical library for Lean 4";
     homepage = "https://github.com/leanprover-community/mathlib4";
     license = lib.licenses.asl20;
-    maintainers = with lib.maintainers; [
-      nadja-y
-      niklashh
-    ];
+    maintainers = with lib.maintainers; [ nadja-y ];
   };
 }
diff --git a/pkgs/development/lean-modules/plausible/default.nix b/pkgs/development/lean-modules/plausible/default.nix
index 6f4d08d0ee28..07b22b3ebe87 100644
--- a/pkgs/development/lean-modules/plausible/default.nix
+++ b/pkgs/development/lean-modules/plausible/default.nix
@@ -6,13 +6,13 @@
 
 buildLakePackage {
   pname = "lean4-plausible";
-  version = "4.30.0";
+  version = "4.29.0";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "plausible";
-    tag = "v4.30.0";
-    hash = "sha256-DSaS0W2cfCUh2N+7WyiM7aUv3trtRNON0PzCgCW2SKY=";
+    tag = "v4.29.0";
+    hash = "sha256-08fNB2GK5AqDJ15n5Ol+HYqaSbsznyp4cerDo32bG50=";
   };
 
   leanPackageName = "plausible";
@@ -21,9 +21,6 @@ buildLakePackage {
     description = "Property-based testing framework for Lean 4";
     homepage = "https://github.com/leanprover-community/plausible";
     license = lib.licenses.asl20;
-    maintainers = with lib.maintainers; [
-      nadja-y
-      niklashh
-    ];
+    maintainers = with lib.maintainers; [ nadja-y ];
   };
 }
diff --git a/pkgs/development/lean-modules/proofwidgets/default.nix b/pkgs/development/lean-modules/proofwidgets/default.nix
index 3a2793272012..54998125b500 100644
--- a/pkgs/development/lean-modules/proofwidgets/default.nix
+++ b/pkgs/development/lean-modules/proofwidgets/default.nix
@@ -62,9 +62,6 @@ buildLakePackage {
     description = "Interactive UI framework for Lean 4 proof assistants";
     homepage = "https://github.com/leanprover-community/ProofWidgets4";
     license = lib.licenses.asl20;
-    maintainers = with lib.maintainers; [
-      nadja-y
-      niklashh
-    ];
+    maintainers = with lib.maintainers; [ nadja-y ];
   };
 }

From 6987e3afbeeec026af04600717d57c7dc15eeb41 Mon Sep 17 00:00:00 2001
From: Nadja Yang <nadja@njy.dev>
Date: Sun, 19 Apr 2026 13:06:21 -0400
Subject: [PATCH 2/8] leanPackages.lean4: 4.29.0 -> 4.29.1

Strip ephemeral setup.json build artifacts from library outputs.
These are produced per-module during compilation and not included
in upstream cache distributions
(https://github.com/NixOS/nixpkgs/issues/510957).

Disable Hydra builds for mathlib since the output exceeds the NAR
size limit.

Pre-build static library for batteries so downstream executables
can link against it.

Refactor update.sh to pin each dependency to the rev from mathlib's
lake-manifest.json.
---
 pkgs/build-support/lake/default.nix           |   4 +
 .../lake/test/weak-minimax/package.nix        |   2 +-
 pkgs/development/lean-modules/Cli/default.nix |   7 +-
 .../lean-modules/LeanSearchClient/default.nix |   4 +-
 pkgs/development/lean-modules/Qq/default.nix  |   5 +-
 .../lean-modules/aesop/default.nix            |   5 +-
 .../lean-modules/batteries/default.nix        |  15 ++-
 .../lean-modules/importGraph/default.nix      |   5 +-
 .../lean-modules/lean4/default.nix            |   4 +-
 .../lean-modules/mathlib/default.nix          |  15 ++-
 .../lean-modules/plausible/default.nix        |   5 +-
 .../lean-modules/proofwidgets/default.nix     |  27 ++--
 pkgs/development/lean-modules/update.sh       | 127 ++++++++++--------
 13 files changed, 130 insertions(+), 95 deletions(-)

diff --git a/pkgs/build-support/lake/default.nix b/pkgs/build-support/lake/default.nix
index 114a8354fa89..48af90f70c6d 100644
--- a/pkgs/build-support/lake/default.nix
+++ b/pkgs/build-support/lake/default.nix
@@ -190,6 +190,10 @@ lib.extendMkDerivation {
                 mv "$out/.lake/config/[anonymous]" "$out/.lake/config/${leanPackageName}"
               fi
 
+              if [ -d "$out/.lake/build/ir" ]; then
+                find "$out/.lake/build/ir" -name '*.setup.json' -delete
+              fi
+
               # 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/build-support/lake/test/weak-minimax/package.nix b/pkgs/build-support/lake/test/weak-minimax/package.nix
index 19cecab89878..4d42cd7bfad4 100644
--- a/pkgs/build-support/lake/test/weak-minimax/package.nix
+++ b/pkgs/build-support/lake/test/weak-minimax/package.nix
@@ -1,4 +1,4 @@
-# Test that buildLakePackage works with nix-only deps (no lake-manifest.json).
+# Test that buildLakePackage works with nix-only deps (empty lake-manifest.json).
 # Builds a Lean proof of the weak minimax inequality using mathlib.
 {
   leanPackages,
diff --git a/pkgs/development/lean-modules/Cli/default.nix b/pkgs/development/lean-modules/Cli/default.nix
index d3bc495ee9cf..2ea9e68a71a4 100644
--- a/pkgs/development/lean-modules/Cli/default.nix
+++ b/pkgs/development/lean-modules/Cli/default.nix
@@ -4,14 +4,15 @@
   fetchFromGitHub,
 }:
 
-buildLakePackage {
+buildLakePackage (finalAttrs: {
   pname = "lean4-cli";
+  # nixpkgs-update: no auto update
   version = "4.29.0";
 
   src = fetchFromGitHub {
     owner = "leanprover";
     repo = "lean4-cli";
-    tag = "v4.29.0";
+    tag = "v${finalAttrs.version}";
     hash = "sha256-jCUl4sXVmwtYPuQecEUFH6mwFzPaQY7au4624EOiWjk=";
   };
 
@@ -33,4 +34,4 @@ buildLakePackage {
     license = lib.licenses.mit;
     maintainers = with lib.maintainers; [ nadja-y ];
   };
-}
+})
diff --git a/pkgs/development/lean-modules/LeanSearchClient/default.nix b/pkgs/development/lean-modules/LeanSearchClient/default.nix
index b7e25b5ecbd0..ad9267133806 100644
--- a/pkgs/development/lean-modules/LeanSearchClient/default.nix
+++ b/pkgs/development/lean-modules/LeanSearchClient/default.nix
@@ -6,8 +6,8 @@
 
 buildLakePackage {
   pname = "lean4-LeanSearchClient";
-  # No lockstep tags; version pinned by mathlib's lake-manifest.json.
-  version = "0-unstable-2026-02-12";
+  # nixpkgs-update: no auto update
+  version = "4.12.0-unstable-2026-02-12";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
diff --git a/pkgs/development/lean-modules/Qq/default.nix b/pkgs/development/lean-modules/Qq/default.nix
index 6feb6fa51916..9e7b712a3250 100644
--- a/pkgs/development/lean-modules/Qq/default.nix
+++ b/pkgs/development/lean-modules/Qq/default.nix
@@ -6,12 +6,13 @@
 
 buildLakePackage {
   pname = "lean4-Qq";
-  version = "4.29.0";
+  # nixpkgs-update: no auto update
+  version = "4.29.0-unstable-2026-03-28";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "quote4";
-    tag = "v4.29.0";
+    rev = "707efb56d0696634e9e965523a1bbe9ac6ce141d";
     hash = "sha256-pNY5hv1nJbreCfU4EewIHCpiryIBv1ghWibrUW8vnQ0=";
   };
 
diff --git a/pkgs/development/lean-modules/aesop/default.nix b/pkgs/development/lean-modules/aesop/default.nix
index 7d8ad308741a..04bb848b300e 100644
--- a/pkgs/development/lean-modules/aesop/default.nix
+++ b/pkgs/development/lean-modules/aesop/default.nix
@@ -7,12 +7,13 @@
 
 buildLakePackage {
   pname = "lean4-aesop";
-  version = "4.29.0";
+  # nixpkgs-update: no auto update
+  version = "4.29.0-unstable-2026-03-28";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "aesop";
-    tag = "v4.29.0";
+    rev = "7152850e7b216a0d409701617721b6e469d34bf6";
     hash = "sha256-CNwxNig8OWjtfQRYyRnM/HGBn2oaNX5qP9CVT2eWNlg=";
   };
 
diff --git a/pkgs/development/lean-modules/batteries/default.nix b/pkgs/development/lean-modules/batteries/default.nix
index 9fdb1efd8686..90d263c51b5d 100644
--- a/pkgs/development/lean-modules/batteries/default.nix
+++ b/pkgs/development/lean-modules/batteries/default.nix
@@ -6,17 +6,28 @@
 
 buildLakePackage {
   pname = "lean4-batteries";
-  version = "4.29.0";
+  # nixpkgs-update: no auto update
+  version = "4.29.0-unstable-2026-03-27";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "batteries";
-    tag = "v4.29.0";
+    rev = "756e3321fd3b02a85ffda19fef789916223e578c";
     hash = "sha256-sEIDi2i2FaLTgKYWt/kzqPrjMdf+bFURfhw6ZZWBawQ=";
   };
 
   leanPackageName = "batteries";
 
+  # Pre-build static library for downstream executables.
+  # TODO: upstream this to batteries
+  postPatch = ''
+    substituteInPlace lakefile.toml \
+      --replace-fail '[[lean_lib]]
+    name = "Batteries"' '[[lean_lib]]
+    name = "Batteries"
+    defaultFacets = ["static"]'
+  '';
+
   meta = {
     description = "The batteries-included extended library for Lean 4";
     homepage = "https://github.com/leanprover-community/batteries";
diff --git a/pkgs/development/lean-modules/importGraph/default.nix b/pkgs/development/lean-modules/importGraph/default.nix
index 4da481fd5a16..4a9307939bf1 100644
--- a/pkgs/development/lean-modules/importGraph/default.nix
+++ b/pkgs/development/lean-modules/importGraph/default.nix
@@ -7,12 +7,13 @@
 
 buildLakePackage {
   pname = "lean4-importGraph";
-  version = "4.29.0";
+  # nixpkgs-update: no auto update
+  version = "4.29.0-unstable-2026-03-28";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "import-graph";
-    tag = "v4.29.0";
+    rev = "48d5698bc464786347c1b0d859b18f938420f060";
     hash = "sha256-tqdO2qyWiJzEbK0yuu4+tiOXTEg9XJfGnI7z6Jh/abg=";
   };
 
diff --git a/pkgs/development/lean-modules/lean4/default.nix b/pkgs/development/lean-modules/lean4/default.nix
index 7ba6dd5170f4..2db3d50c4f0d 100644
--- a/pkgs/development/lean-modules/lean4/default.nix
+++ b/pkgs/development/lean-modules/lean4/default.nix
@@ -17,7 +17,7 @@
 let
   lean4 = stdenv.mkDerivation (finalAttrs: {
     pname = "lean4";
-    version = "4.29.0";
+    version = "4.29.1";
 
     mimalloc-src = fetchFromGitHub {
       owner = "microsoft";
@@ -30,7 +30,7 @@ let
       owner = "leanprover";
       repo = "lean4";
       tag = "v${finalAttrs.version}";
-      hash = "sha256-0v4OTrCLdHBbWJUq7hIjJonqget9SvsG3izGlOwhwyU=";
+      hash = "sha256-pdhRPjSic2H8zPJXLmyfN8umKDoafjmSo4OQSRxIbyE=";
     };
 
     # Vendor mimalloc. Upstream has since partially adopted FetchContent:
diff --git a/pkgs/development/lean-modules/mathlib/default.nix b/pkgs/development/lean-modules/mathlib/default.nix
index 70a34dd9f333..6c70a6048613 100644
--- a/pkgs/development/lean-modules/mathlib/default.nix
+++ b/pkgs/development/lean-modules/mathlib/default.nix
@@ -12,15 +12,16 @@
   tests,
 }:
 
-buildLakePackage {
+buildLakePackage (finalAttrs: {
   pname = "lean4-mathlib";
-  version = "4.29.0";
+  # nixpkgs-update: no auto update
+  version = "4.29.1";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "mathlib4";
-    tag = "v4.29.0";
-    hash = "sha256-fe+qS7gNxdLnACX3/jqToa9m7r1gbskY6kDJbm1ZefE=";
+    tag = "v${finalAttrs.version}";
+    hash = "sha256-K/QPTOytsV+OX25xyKlspeB9G0a28IjmJxcUAKXFP9U=";
   };
 
   leanPackageName = "mathlib";
@@ -44,6 +45,10 @@ buildLakePackage {
     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 ];
   };
-}
+})
diff --git a/pkgs/development/lean-modules/plausible/default.nix b/pkgs/development/lean-modules/plausible/default.nix
index 07b22b3ebe87..978de87e82a9 100644
--- a/pkgs/development/lean-modules/plausible/default.nix
+++ b/pkgs/development/lean-modules/plausible/default.nix
@@ -6,12 +6,13 @@
 
 buildLakePackage {
   pname = "lean4-plausible";
-  version = "4.29.0";
+  # nixpkgs-update: no auto update
+  version = "4.29.0-unstable-2026-03-28";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "plausible";
-    tag = "v4.29.0";
+    rev = "83e90935a17ca19ebe4b7893c7f7066e266f50d3";
     hash = "sha256-08fNB2GK5AqDJ15n5Ol+HYqaSbsznyp4cerDo32bG50=";
   };
 
diff --git a/pkgs/development/lean-modules/proofwidgets/default.nix b/pkgs/development/lean-modules/proofwidgets/default.nix
index 54998125b500..d7373c734283 100644
--- a/pkgs/development/lean-modules/proofwidgets/default.nix
+++ b/pkgs/development/lean-modules/proofwidgets/default.nix
@@ -7,23 +7,20 @@
   nodejs,
 }:
 
-let
-  version = "0.0.95";
+buildLakePackage (finalAttrs: {
+  pname = "lean4-proofwidgets";
+  # nixpkgs-update: no auto update
+  version = "0.0.95+lean-v4.29.1";
+
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "ProofWidgets4";
-    tag = "v${version}";
-    hash = "sha256-LETljr+QEU6CxprR3pB4hUzhgCD8PrIuiPOgTIdhHVM=";
+    tag = "v${finalAttrs.version}";
+    hash = "sha256-D1fTsV8W29S1C53ky66sFgIoA5cLx/ilKa98czScV+s=";
   };
-in
-
-buildLakePackage {
-  pname = "lean4-proofwidgets";
-  inherit version src;
 
   leanPackageName = "proofwidgets";
 
-  # ProofWidgets has no Lean dependencies (lake-manifest.json packages = []).
   lakeHash = null;
 
   nativeBuildInputs = [
@@ -31,20 +28,14 @@ buildLakePackage {
     npmHooks.npmConfigHook
   ];
 
-  # Pre-fetched npm dependencies for the TypeScript widget build
-  # (npm/rollup in widget/).  npmConfigHook installs these offline.
   npmDeps = fetchNpmDeps {
     name = "lean4-proofwidgets-npm-deps";
-    inherit src;
+    src = finalAttrs.src;
     sourceRoot = "source/widget";
     hash = "sha256-ShH6MDr76wzWQrJvhMWCnklaox/uRsfoe+aYVSo/eNA=";
   };
   npmRoot = "widget";
 
-  # Lake's widgetJsAll target runs `npm clean-install` which wipes
-  # node_modules and the patched shebangs that npmConfigHook applied.
-  # Wrap npm to skip ci/clean-install (deps already installed) while
-  # passing `npm run build` through — same pattern as llama-cpp/evcc.
   postConfigure = ''
     local realNpm
     realNpm="$(type -P npm)"
@@ -64,4 +55,4 @@ buildLakePackage {
     license = lib.licenses.asl20;
     maintainers = with lib.maintainers; [ nadja-y ];
   };
-}
+})
diff --git a/pkgs/development/lean-modules/update.sh b/pkgs/development/lean-modules/update.sh
index fc05fe41b5c5..4ba4372b0c4c 100755
--- a/pkgs/development/lean-modules/update.sh
+++ b/pkgs/development/lean-modules/update.sh
@@ -1,30 +1,18 @@
 #!/usr/bin/env nix-shell
-#!nix-shell -i bash -p nix-update common-updater-scripts curl jq
+#!nix-shell -i bash -p nix-update curl jq gh
 
-# Update the leanPackages set.
-#
-# Usage:
-#   ./pkgs/development/lean-modules/update.sh [version]
+# Usage: ./pkgs/development/lean-modules/update.sh [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//')}"
 
-# Snapshot before any updates.
-old_lockstep=$(nix eval --raw .#leanPackages.mathlib.version 2>/dev/null || echo "")
-old_pw=$(nix eval --raw .#leanPackages.proofwidgets.version 2>/dev/null || echo "")
-old_lsc=$(nix eval --raw .#leanPackages.LeanSearchClient.version 2>/dev/null || echo "")
+dir=$(dirname "$0")
+FAKE="sha256-AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA="
 
-run() { echo "  $*"; "$@"; }
+old_lean4=$(nix eval --raw .#leanPackages.lean4.version 2>/dev/null || echo "")
 
-# --- lean4 toolchain ---
-
-run nix-update leanPackages.lean4 --version="$lean4_version"
-
-# --- mathlib dependency tree ---
-# Versions are derived from mathlib's lake-manifest.json at the
-# matching lean4 tag. Most packages release in lockstep with lean4;
-# ProofWidgets and LeanSearchClient have their own versioning.
+nix-update leanPackages.lean4 --version="$lean4_version"
 
 manifest=$(curl -sL "https://raw.githubusercontent.com/leanprover-community/mathlib4/v${lean4_version}/lake-manifest.json")
 
@@ -37,47 +25,78 @@ if [ "$manifest_deps" != "$known_deps" ]; then
   exit 1
 fi
 
-pw_version=$(echo "$manifest" | jq -r '.packages[] | select(.name == "proofwidgets") | .inputRev' | sed 's/^v//')
+patch_pkg() {
+  local pkgname="$1" repo="$2"
+  local file="$dir/$pkgname/default.nix"
+  local inputRev rev version
+  inputRev=$(echo "$manifest" | jq -r ".packages[] | select(.name == \"$pkgname\") | .inputRev")
+  rev=$(echo "$manifest" | jq -r ".packages[] | select(.name == \"$pkgname\") | .rev")
 
-lsc_rev=$(echo "$manifest" | jq -r '.packages[] | select(.name == "LeanSearchClient") | .rev')
-lsc_date=$(curl -sL "https://api.github.com/repos/leanprover-community/LeanSearchClient/commits/$lsc_rev" | jq -r '.commit.committer.date[:10]')
-lsc_version="0-unstable-$lsc_date"
+  if [[ "$inputRev" =~ ^v[0-9] ]]; then
+    version="${inputRev#v}"
+    # tag = "v${...version}" auto-follows; convert rev → tag if needed.
+    if grep -q 'rev = "' "$file"; then
+      sed -i -E "s|rev = \"[^\"]*\";|tag = \"${inputRev}\";|" "$file"
+    fi
+  else
+    local tmp=$(mktemp -d)
+    git clone --bare --filter=tree:0 --depth=100 --single-branch "https://github.com/$repo" "$tmp" 2>/dev/null
+    local latest_tag=$(git -C "$tmp" describe --tags --abbrev=0 --match 'v[0-9]*' "$rev" 2>/dev/null | sed 's/^v//')
+    rm -rf "$tmp"
+    local date=$(gh api "repos/$repo/commits/$rev" --jq '.commit.committer.date[:10]')
+    version="${latest_tag:-0}-unstable-$date"
+    if grep -q 'rev = "' "$file"; then
+      sed -i -E "s|rev = \"[^\"]*\";|rev = \"${rev}\";|" "$file"
+    else
+      sed -i -E "s|tag = \"[^\"]*\";|rev = \"${rev}\";|" "$file"
+    fi
+  fi
+
+  sed -i -E "s|version = \"[^\"]*\";|version = \"${version}\";|" "$file"
+  sed -i "0,/hash = \"sha256-[^\"]*\"/{s||hash = \"$FAKE\"|}" "$file"
+}
 
 echo "--- mathlib tree ---"
 
-# Lockstep version synchronization.
-dir=pkgs/development/lean-modules
-for pkg in batteries aesop Qq plausible Cli importGraph mathlib; do
-  sed -i "s|tag = \"v${old_lockstep}\"|tag = \"v${lean4_version}\"|" "$dir/$pkg/default.nix"
-done
+patch_pkg batteries        leanprover-community/batteries
+patch_pkg Qq               leanprover-community/quote4
+patch_pkg aesop            leanprover-community/aesop
+patch_pkg Cli              leanprover/lean4-cli
+patch_pkg plausible        leanprover-community/plausible
+patch_pkg importGraph      leanprover-community/import-graph
+patch_pkg proofwidgets     leanprover-community/ProofWidgets4
+patch_pkg LeanSearchClient leanprover-community/LeanSearchClient
 
-run nix-update leanPackages.batteries    --version="$lean4_version"
-run nix-update leanPackages.Qq           --version="$lean4_version"
-run nix-update leanPackages.plausible    --version="$lean4_version"
-run nix-update leanPackages.Cli          --version="$lean4_version"
-run nix-update leanPackages.proofwidgets --version="$pw_version"
-run update-source-version leanPackages.LeanSearchClient "$lsc_version" --rev="$lsc_rev"
-run nix-update leanPackages.aesop        --version="$lean4_version"
-run nix-update leanPackages.importGraph  --version="$lean4_version"
-run nix-update leanPackages.mathlib      --version="$lean4_version"
-
-# --- summary ---
-
-changes=()
-[ "$old_lockstep" != "$lean4_version" ] && changes+=("mathlib tree: $old_lockstep -> $lean4_version")
-[ "$old_pw" != "$pw_version" ] && changes+=("proofwidgets: $old_pw -> $pw_version")
-[ "$old_lsc" != "$lsc_version" ] && changes+=("LeanSearchClient: $old_lsc -> $lsc_version")
-
-if [ ${#changes[@]} -eq 0 ]; then
-  echo "status: up-to-date"
-  exit 0
+sed -i -E "/lean4-mathlib/,/version/s|version = \"[^\"]*\";|version = \"${lean4_version}\";|" "$dir/mathlib/default.nix"
+if ! grep -q 'tag = "v\${finalAttrs.version}"' "$dir/mathlib/default.nix"; then
+  sed -i -E 's|tag = "v[^"]*";|tag = "v${finalAttrs.version}";|' "$dir/mathlib/default.nix"
 fi
+sed -i "0,/hash = \"sha256-[^\"]*\"/{s||hash = \"$FAKE\"|}" "$dir/mathlib/default.nix"
 
-echo "commit-title: leanPackages: lean4 $old_lockstep -> $lean4_version"
-echo "---"
-for c in "${changes[@]}"; do
-  echo "  - $c"
+prefetch() {
+  local out newhash
+  out=$(nix build ".#leanPackages.${1}.${2:-src}" 2>&1 || true)
+  newhash=$(echo "$out" | awk '/got:/ {print $2}' | head -1)
+  if [ -z "$newhash" ]; then
+    echo "ERROR: failed to prefetch $1.${2:-src}" >&2
+    echo "$out" >&2
+    return 1
+  fi
+  echo "$newhash"
+}
+
+for pkg in batteries Qq aesop Cli plausible importGraph proofwidgets LeanSearchClient mathlib; do
+  echo "  prefetching $pkg"
+  newhash=$(prefetch "$pkg")
+  sed -i "s|$FAKE|$newhash|" "$dir/$pkg/default.nix"
 done
-echo "---"
-echo "manifest-source: https://github.com/leanprover-community/mathlib4/blob/v${lean4_version}/lake-manifest.json"
-echo "lean4-release: https://github.com/leanprover/lean4/releases/tag/v${lean4_version}"
+
+echo "  prefetching proofwidgets npmDeps"
+# Replace the second hash (the one inside fetchNpmDeps) with fake.
+sed -i "0,/hash = \"sha256-[^\"]*\"/!{s|hash = \"sha256-[^\"]*\"|hash = \"$FAKE\"|}" "$dir/proofwidgets/default.nix"
+newhash=$(prefetch proofwidgets npmDeps)
+sed -i "s|$FAKE|$newhash|" "$dir/proofwidgets/default.nix"
+
+echo "leanPackages.lean4: $old_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}"

From cefae5621e02e39a4a1466d74b7f697b9bbb7d3c Mon Sep 17 00:00:00 2001
From: Nadja Yang <nadja@njy.dev>
Date: Fri, 24 Apr 2026 08:15:32 -0400
Subject: [PATCH 3/8] leanPackages.lean4: use nixpkgs cadical, patch all
 binaries

Lean binaries derive sysroot from IO.appPath; patch all of them
rather than just lean and lake. Add cadical to symlinkJoin paths
instead of bundling a copy via INSTALL_CADICAL.

https://github.com/NixOS/nixpkgs/pull/513024/changes/ed10debb3c8ad78e687521bb802383e21cd74472
---
 .../lean-modules/lean4/default.nix            | 20 ++++++++-----------
 1 file changed, 8 insertions(+), 12 deletions(-)

diff --git a/pkgs/development/lean-modules/lean4/default.nix b/pkgs/development/lean-modules/lean4/default.nix
index 2db3d50c4f0d..75bee7aa8c0d 100644
--- a/pkgs/development/lean-modules/lean4/default.nix
+++ b/pkgs/development/lean-modules/lean4/default.nix
@@ -113,22 +113,18 @@ in
 # Binary-patched for correct runtime discovery in wrapped environments.
 symlinkJoin {
   inherit (lean4) name pname;
-  paths = [ lean4 ];
+  paths = [
+    lean4
+    cadical
+  ];
   nativeBuildInputs = [ perl ];
   postBuild = ''
     newStorePath=$(echo "$out" | head -c 43)
 
-    # Copy (not symlink) — IO.appPath resolves through symlinks.
-    rm $out/bin/lean $out/bin/lake
-    cp ${lean4}/bin/lean $out/bin/lean
-    cp ${lean4}/bin/lake $out/bin/lake
-
-    for bin in $out/bin/lean $out/bin/lake; do
-      cat "$bin" \
-        | perl -pe "s|\Q${oldStorePath}\E|$newStorePath|g" \
-        > "$bin.tmp"
-      chmod +x "$bin.tmp"
-      mv "$bin.tmp" "$bin"
+    for bin in ${lean4}/bin/*; do
+      test -f "$bin" || continue
+      install -m755 "$bin" "$out/bin/"
+      perl -pi -e "s|\Q${oldStorePath}\E|$newStorePath|g" "$out/bin/$(basename "$bin")"
     done
   '';
 

From fb169268a384200bb133bfdcf4d556a5437dd380 Mon Sep 17 00:00:00 2001
From: Nadja Yang <nadja@njy.dev>
Date: Fri, 24 Apr 2026 12:17:00 -0400
Subject: [PATCH 4/8] 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;
 })

From 5d81234142df96c65d9baaaf8a9bc93430453e16 Mon Sep 17 00:00:00 2001
From: Nadja Yang <nadja@njy.dev>
Date: Sat, 2 May 2026 03:57:01 -0400
Subject: [PATCH 5/8] leanPackages.lean4: pin cadical to 2.1.3, add smoke test

cadical >= 2.2.0 produces LRAT proofs Lean's checker does not
yet handle, breaking bv_decide.

https://github.com/NixOS/nixpkgs/pull/514456/commits/0eced05aae1e4493a97609f3c3f7613ecf55f91f
---
 .../lean-modules/lean4/default.nix            | 67 +++++++++++++------
 1 file changed, 45 insertions(+), 22 deletions(-)

diff --git a/pkgs/development/lean-modules/lean4/default.nix b/pkgs/development/lean-modules/lean4/default.nix
index 75bee7aa8c0d..f2eae9f85a87 100644
--- a/pkgs/development/lean-modules/lean4/default.nix
+++ b/pkgs/development/lean-modules/lean4/default.nix
@@ -8,9 +8,12 @@
   git,
   gmp,
   cadical,
+  cadical' ? cadical.override { version = "2.1.3"; },
   pkg-config,
   libuv,
   perl,
+  runCommand,
+  writeText,
   testers,
 }:
 
@@ -75,7 +78,7 @@ let
     buildInputs = [
       gmp
       libuv
-      cadical
+      cadical'
     ];
 
     nativeCheckInputs = [
@@ -109,27 +112,47 @@ let
   });
 
   oldStorePath = builtins.substring 0 43 (toString lean4);
-in
-# Binary-patched for correct runtime discovery in wrapped environments.
-symlinkJoin {
-  inherit (lean4) name pname;
-  paths = [
-    lean4
-    cadical
-  ];
-  nativeBuildInputs = [ perl ];
-  postBuild = ''
-    newStorePath=$(echo "$out" | head -c 43)
 
-    for bin in ${lean4}/bin/*; do
-      test -f "$bin" || continue
-      install -m755 "$bin" "$out/bin/"
-      perl -pi -e "s|\Q${oldStorePath}\E|$newStorePath|g" "$out/bin/$(basename "$bin")"
-    done
-  '';
+  # Binary-patched for correct runtime discovery in wrapped environments.
+  wrapped = symlinkJoin {
+    inherit (lean4) name pname;
+    paths = [
+      lean4
+      cadical'
+    ];
+    nativeBuildInputs = [ perl ];
+    postBuild = ''
+      newStorePath=$(echo "$out" | head -c 43)
 
-  inherit (lean4) version src meta;
-  passthru = {
-    inherit (lean4) version src;
+      for bin in ${lean4}/bin/*; do
+        test -f "$bin" || continue
+        install -m755 "$bin" "$out/bin/"
+        perl -pi -e "s|\Q${oldStorePath}\E|$newStorePath|g" "$out/bin/$(basename "$bin")"
+      done
+    '';
+
+    inherit (lean4) version src meta;
+    passthru = {
+      inherit (lean4) version src;
+      tests =
+        let
+          src = writeText "smoke.lean" ''
+            import Std
+            example : 1 + 1 = 2 := by decide
+            example : ∀ (x y : BitVec 8), x &&& y = y &&& x := by bv_decide
+          '';
+        in
+        {
+          version = testers.testVersion {
+            package = wrapped;
+            version = "v${lean4.version}";
+          };
+          smoke = runCommand "lean4-test-smoke" { } ''
+            ${wrapped}/bin/lean ${src}
+            touch $out
+          '';
+        };
+    };
   };
-}
+in
+wrapped

From b606786817d87fbe2ff85e4ea37d84af65612479 Mon Sep 17 00:00:00 2001
From: Nadja Yang <nadja@njy.dev>
Date: Wed, 3 Jun 2026 14:24:40 -0400
Subject: [PATCH 6/8] leanPackages: 4.29.1 -> 4.30.0

Add leangz (leantar) as a new build and runtime dependency.

https://github.com/leanprover/lean4/releases/tag/v4.30.0
https://github.com/leanprover-community/mathlib4/blob/v4.30.0/lake-manifest.json
---
 pkgs/development/lean-modules/Cli/default.nix          | 4 ++--
 pkgs/development/lean-modules/Qq/default.nix           | 6 +++---
 pkgs/development/lean-modules/aesop/default.nix        | 6 +++---
 pkgs/development/lean-modules/batteries/default.nix    | 6 +++---
 pkgs/development/lean-modules/importGraph/default.nix  | 6 +++---
 pkgs/development/lean-modules/lean4/default.nix        | 8 ++++++--
 pkgs/development/lean-modules/mathlib/default.nix      | 4 ++--
 pkgs/development/lean-modules/plausible/default.nix    | 6 +++---
 pkgs/development/lean-modules/proofwidgets/default.nix | 6 +++---
 9 files changed, 28 insertions(+), 24 deletions(-)

diff --git a/pkgs/development/lean-modules/Cli/default.nix b/pkgs/development/lean-modules/Cli/default.nix
index 2ea9e68a71a4..d5bef89381c4 100644
--- a/pkgs/development/lean-modules/Cli/default.nix
+++ b/pkgs/development/lean-modules/Cli/default.nix
@@ -7,13 +7,13 @@
 buildLakePackage (finalAttrs: {
   pname = "lean4-cli";
   # nixpkgs-update: no auto update
-  version = "4.29.0";
+  version = "4.30.0";
 
   src = fetchFromGitHub {
     owner = "leanprover";
     repo = "lean4-cli";
     tag = "v${finalAttrs.version}";
-    hash = "sha256-jCUl4sXVmwtYPuQecEUFH6mwFzPaQY7au4624EOiWjk=";
+    hash = "sha256-oMaqHvWlEfk1601JfNKPvkGIWgMW6tiF7Mej7g63vh0=";
   };
 
   leanPackageName = "Cli";
diff --git a/pkgs/development/lean-modules/Qq/default.nix b/pkgs/development/lean-modules/Qq/default.nix
index 9e7b712a3250..dd89f7baa317 100644
--- a/pkgs/development/lean-modules/Qq/default.nix
+++ b/pkgs/development/lean-modules/Qq/default.nix
@@ -7,13 +7,13 @@
 buildLakePackage {
   pname = "lean4-Qq";
   # nixpkgs-update: no auto update
-  version = "4.29.0-unstable-2026-03-28";
+  version = "4.30.0";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "quote4";
-    rev = "707efb56d0696634e9e965523a1bbe9ac6ce141d";
-    hash = "sha256-pNY5hv1nJbreCfU4EewIHCpiryIBv1ghWibrUW8vnQ0=";
+    tag = "v4.30.0";
+    hash = "sha256-jVsRw/R7D7HmsE7vQvVeDXcnVerlcDBOrhf9FJJiXkY=";
   };
 
   leanPackageName = "Qq";
diff --git a/pkgs/development/lean-modules/aesop/default.nix b/pkgs/development/lean-modules/aesop/default.nix
index 04bb848b300e..f5c6393b3859 100644
--- a/pkgs/development/lean-modules/aesop/default.nix
+++ b/pkgs/development/lean-modules/aesop/default.nix
@@ -8,13 +8,13 @@
 buildLakePackage {
   pname = "lean4-aesop";
   # nixpkgs-update: no auto update
-  version = "4.29.0-unstable-2026-03-28";
+  version = "4.30.0";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "aesop";
-    rev = "7152850e7b216a0d409701617721b6e469d34bf6";
-    hash = "sha256-CNwxNig8OWjtfQRYyRnM/HGBn2oaNX5qP9CVT2eWNlg=";
+    tag = "v4.30.0";
+    hash = "sha256-7PhQVMdiYImuzRYdf0Kgw3JYS4nBLfILXxyhFH8Zag0=";
   };
 
   leanPackageName = "aesop";
diff --git a/pkgs/development/lean-modules/batteries/default.nix b/pkgs/development/lean-modules/batteries/default.nix
index 90d263c51b5d..5ac5ffadc806 100644
--- a/pkgs/development/lean-modules/batteries/default.nix
+++ b/pkgs/development/lean-modules/batteries/default.nix
@@ -7,13 +7,13 @@
 buildLakePackage {
   pname = "lean4-batteries";
   # nixpkgs-update: no auto update
-  version = "4.29.0-unstable-2026-03-27";
+  version = "4.30.0-unstable-2026-05-26";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "batteries";
-    rev = "756e3321fd3b02a85ffda19fef789916223e578c";
-    hash = "sha256-sEIDi2i2FaLTgKYWt/kzqPrjMdf+bFURfhw6ZZWBawQ=";
+    rev = "32dc18cde3684679f3c003de608743b57498c56f";
+    hash = "sha256-OOcKCQEgnn9zkkwjHOovMb/IprNomTDufLOfEXs7hFU=";
   };
 
   leanPackageName = "batteries";
diff --git a/pkgs/development/lean-modules/importGraph/default.nix b/pkgs/development/lean-modules/importGraph/default.nix
index 4a9307939bf1..bda81c7ed521 100644
--- a/pkgs/development/lean-modules/importGraph/default.nix
+++ b/pkgs/development/lean-modules/importGraph/default.nix
@@ -8,13 +8,13 @@
 buildLakePackage {
   pname = "lean4-importGraph";
   # nixpkgs-update: no auto update
-  version = "4.29.0-unstable-2026-03-28";
+  version = "4.30.0-unstable-2026-05-26";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "import-graph";
-    rev = "48d5698bc464786347c1b0d859b18f938420f060";
-    hash = "sha256-tqdO2qyWiJzEbK0yuu4+tiOXTEg9XJfGnI7z6Jh/abg=";
+    rev = "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1";
+    hash = "sha256-V3bGQxTNs2G4MqaVxRb6WED1a7VaHfEo1HgBNqPipz8=";
   };
 
   leanPackageName = "importGraph";
diff --git a/pkgs/development/lean-modules/lean4/default.nix b/pkgs/development/lean-modules/lean4/default.nix
index f2eae9f85a87..d521467d50cb 100644
--- a/pkgs/development/lean-modules/lean4/default.nix
+++ b/pkgs/development/lean-modules/lean4/default.nix
@@ -9,6 +9,7 @@
   gmp,
   cadical,
   cadical' ? cadical.override { version = "2.1.3"; },
+  leangz,
   pkg-config,
   libuv,
   perl,
@@ -20,7 +21,7 @@
 let
   lean4 = stdenv.mkDerivation (finalAttrs: {
     pname = "lean4";
-    version = "4.29.1";
+    version = "4.30.0";
 
     mimalloc-src = fetchFromGitHub {
       owner = "microsoft";
@@ -33,7 +34,7 @@ let
       owner = "leanprover";
       repo = "lean4";
       tag = "v${finalAttrs.version}";
-      hash = "sha256-pdhRPjSic2H8zPJXLmyfN8umKDoafjmSo4OQSRxIbyE=";
+      hash = "sha256-YTsfIppd6km7wOjAxRH5KMPsW++ztFDCJT2up72J86Q=";
     };
 
     # Vendor mimalloc. Upstream has since partially adopted FetchContent:
@@ -72,6 +73,7 @@ let
 
     nativeBuildInputs = [
       cmake
+      leangz
       pkg-config
     ];
 
@@ -90,6 +92,7 @@ let
       "-DUSE_GITHASH=OFF"
       "-DINSTALL_LICENSE=OFF"
       "-DINSTALL_CADICAL=OFF"
+      "-DINSTALL_LEANTAR=OFF"
       "-DUSE_MIMALLOC=ON"
     ];
 
@@ -119,6 +122,7 @@ let
     paths = [
       lean4
       cadical'
+      leangz
     ];
     nativeBuildInputs = [ perl ];
     postBuild = ''
diff --git a/pkgs/development/lean-modules/mathlib/default.nix b/pkgs/development/lean-modules/mathlib/default.nix
index adfce0b79ed6..aea15d0e06d2 100644
--- a/pkgs/development/lean-modules/mathlib/default.nix
+++ b/pkgs/development/lean-modules/mathlib/default.nix
@@ -18,13 +18,13 @@ let
   mathlib__archive = buildLakePackage (finalAttrs: {
     pname = "lean4-mathlib";
     # nixpkgs-update: no auto update
-    version = "4.29.1";
+    version = "4.30.0";
 
     src = fetchFromGitHub {
       owner = "leanprover-community";
       repo = "mathlib4";
       tag = "v${finalAttrs.version}";
-      hash = "sha256-K/QPTOytsV+OX25xyKlspeB9G0a28IjmJxcUAKXFP9U=";
+      hash = "sha256-RxOxdUiVUAxUbfVhxlkjmPX1V64EtmIIn1eW75TiJWA=";
     };
 
     leanPackageName = "mathlib";
diff --git a/pkgs/development/lean-modules/plausible/default.nix b/pkgs/development/lean-modules/plausible/default.nix
index 978de87e82a9..34cf8fe6cb29 100644
--- a/pkgs/development/lean-modules/plausible/default.nix
+++ b/pkgs/development/lean-modules/plausible/default.nix
@@ -7,13 +7,13 @@
 buildLakePackage {
   pname = "lean4-plausible";
   # nixpkgs-update: no auto update
-  version = "4.29.0-unstable-2026-03-28";
+  version = "4.30.0-unstable-2026-05-26";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "plausible";
-    rev = "83e90935a17ca19ebe4b7893c7f7066e266f50d3";
-    hash = "sha256-08fNB2GK5AqDJ15n5Ol+HYqaSbsznyp4cerDo32bG50=";
+    rev = "a456461b368b71d2accd95234832cd9c174b5437";
+    hash = "sha256-DSaS0W2cfCUh2N+7WyiM7aUv3trtRNON0PzCgCW2SKY=";
   };
 
   leanPackageName = "plausible";
diff --git a/pkgs/development/lean-modules/proofwidgets/default.nix b/pkgs/development/lean-modules/proofwidgets/default.nix
index d7373c734283..e0df936ad74c 100644
--- a/pkgs/development/lean-modules/proofwidgets/default.nix
+++ b/pkgs/development/lean-modules/proofwidgets/default.nix
@@ -10,13 +10,13 @@
 buildLakePackage (finalAttrs: {
   pname = "lean4-proofwidgets";
   # nixpkgs-update: no auto update
-  version = "0.0.95+lean-v4.29.1";
+  version = "0.0.99";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "ProofWidgets4";
     tag = "v${finalAttrs.version}";
-    hash = "sha256-D1fTsV8W29S1C53ky66sFgIoA5cLx/ilKa98czScV+s=";
+    hash = "sha256-kGoEkKGrucNUWFYkHW2LsS1gI4C0J8bAHQL2MiE4Pzc=";
   };
 
   leanPackageName = "proofwidgets";
@@ -32,7 +32,7 @@ buildLakePackage (finalAttrs: {
     name = "lean4-proofwidgets-npm-deps";
     src = finalAttrs.src;
     sourceRoot = "source/widget";
-    hash = "sha256-ShH6MDr76wzWQrJvhMWCnklaox/uRsfoe+aYVSo/eNA=";
+    hash = "sha256-ssWSr2qfsIbX25DidiVPm0tsLGjrhQhQ6YKPL0rfc1k=";
   };
   npmRoot = "widget";
 

From bdea40b4edb984318832ebbf14b9a3afac2ff6c1 Mon Sep 17 00:00:00 2001
From: Nadja Yang <nadja@njy.dev>
Date: Wed, 3 Jun 2026 17:04:11 -0400
Subject: [PATCH 7/8] 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}"

From d63d353258b2124b3757ae770e08c8eae14bebfc Mon Sep 17 00:00:00 2001
From: Nadja Yang <nadja@njy.dev>
Date: Thu, 4 Jun 2026 17:13:18 -0400
Subject: [PATCH 8/8] leanPackages.mathlib: add comment for leangz-raw

Co-authored-by: Mauricio Collares <mauricio@collares.org>
---
 pkgs/development/lean-modules/mathlib/default.nix | 1 +
 1 file changed, 1 insertion(+)

diff --git a/pkgs/development/lean-modules/mathlib/default.nix b/pkgs/development/lean-modules/mathlib/default.nix
index 36e3222f0033..8b76f66964c4 100644
--- a/pkgs/development/lean-modules/mathlib/default.nix
+++ b/pkgs/development/lean-modules/mathlib/default.nix
@@ -15,6 +15,7 @@
 }:
 
 let
+  # build leangz without zstd support, to improve Hydra's xz compression ratio
   leangz-raw = leangz.overrideAttrs { cargoBuildNoDefaultFeatures = true; };
 
   mathlib__archive = buildLakePackage (finalAttrs: {