diff --git a/pkgs/build-support/lake/default.nix b/pkgs/build-support/lake/default.nix
index 114a8354fa89..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
@@ -190,6 +191,12 @@ 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
+
+              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/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/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/Cli/default.nix b/pkgs/development/lean-modules/Cli/default.nix
index 07476219fea2..d5bef89381c4 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.30.0";
 
   src = fetchFromGitHub {
     owner = "leanprover";
     repo = "lean4-cli";
-    tag = "v4.30.0";
+    tag = "v${finalAttrs.version}";
     hash = "sha256-oMaqHvWlEfk1601JfNKPvkGIWgMW6tiF7Mej7g63vh0=";
   };
 
@@ -31,9 +32,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..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";
@@ -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..dd89f7baa317 100644
--- a/pkgs/development/lean-modules/Qq/default.nix
+++ b/pkgs/development/lean-modules/Qq/default.nix
@@ -6,6 +6,7 @@
 
 buildLakePackage {
   pname = "lean4-Qq";
+  # nixpkgs-update: no auto update
   version = "4.30.0";
 
   src = fetchFromGitHub {
@@ -21,9 +22,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..f5c6393b3859 100644
--- a/pkgs/development/lean-modules/aesop/default.nix
+++ b/pkgs/development/lean-modules/aesop/default.nix
@@ -7,6 +7,7 @@
 
 buildLakePackage {
   pname = "lean4-aesop";
+  # nixpkgs-update: no auto update
   version = "4.30.0";
 
   src = fetchFromGitHub {
@@ -23,9 +24,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..5ac5ffadc806 100644
--- a/pkgs/development/lean-modules/batteries/default.nix
+++ b/pkgs/development/lean-modules/batteries/default.nix
@@ -6,12 +6,13 @@
 
 buildLakePackage {
   pname = "lean4-batteries";
-  version = "4.30.0";
+  # nixpkgs-update: no auto update
+  version = "4.30.0-unstable-2026-05-26";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "batteries";
-    tag = "v4.30.0";
+    rev = "32dc18cde3684679f3c003de608743b57498c56f";
     hash = "sha256-OOcKCQEgnn9zkkwjHOovMb/IprNomTDufLOfEXs7hFU=";
   };
 
@@ -31,9 +32,6 @@ buildLakePackage {
     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..bda81c7ed521 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.30.0";
+  # nixpkgs-update: no auto update
+  version = "4.30.0-unstable-2026-05-26";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "import-graph";
-    tag = "v4.30.0";
+    rev = "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1";
     hash = "sha256-V3bGQxTNs2G4MqaVxRb6WED1a7VaHfEo1HgBNqPipz8=";
   };
 
@@ -23,9 +24,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..d521467d50cb 100644
--- a/pkgs/development/lean-modules/lean4/default.nix
+++ b/pkgs/development/lean-modules/lean4/default.nix
@@ -8,15 +8,17 @@
   git,
   gmp,
   cadical,
+  cadical' ? cadical.override { version = "2.1.3"; },
   leangz,
   pkg-config,
   libuv,
   perl,
+  runCommand,
+  writeText,
   testers,
 }:
-let
-  cadical' = cadical.override { version = "2.1.3"; };
 
+let
   lean4 = stdenv.mkDerivation (finalAttrs: {
     pname = "lean4";
     version = "4.30.0";
@@ -71,8 +73,8 @@ let
 
     nativeBuildInputs = [
       cmake
+      leangz
       pkg-config
-      leangz # Provides leantar
     ];
 
     buildInputs = [
@@ -90,6 +92,7 @@ let
       "-DUSE_GITHASH=OFF"
       "-DINSTALL_LICENSE=OFF"
       "-DINSTALL_CADICAL=OFF"
+      "-DINSTALL_LEANTAR=OFF"
       "-DUSE_MIMALLOC=ON"
     ];
 
@@ -106,40 +109,54 @@ 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";
     };
   });
 
   oldStorePath = builtins.substring 0 43 (toString lean4);
-in
-# Binary-patched for correct runtime discovery in wrapped environments.
-symlinkJoin {
-  inherit (lean4) name pname;
-  paths = [ lean4 ];
-  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
+  # Binary-patched for correct runtime discovery in wrapped environments.
+  wrapped = symlinkJoin {
+    inherit (lean4) name pname;
+    paths = [
+      lean4
+      cadical'
+      leangz
+    ];
+    nativeBuildInputs = [ perl ];
+    postBuild = ''
+      newStorePath=$(echo "$out" | head -c 43)
 
-    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"
-    done
-  '';
+      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;
+    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
diff --git a/pkgs/development/lean-modules/mathlib/default.nix b/pkgs/development/lean-modules/mathlib/default.nix
index 60ae77331f02..8b76f66964c4 100644
--- a/pkgs/development/lean-modules/mathlib/default.nix
+++ b/pkgs/development/lean-modules/mathlib/default.nix
@@ -1,6 +1,8 @@
 {
   lib,
   buildLakePackage,
+  runCommand,
+  leangz,
   fetchFromGitHub,
   batteries,
   aesop,
@@ -12,41 +14,88 @@
   tests,
 }:
 
-buildLakePackage {
-  pname = "lean4-mathlib";
-  version = "4.30.0";
+let
+  # build leangz without zstd support, to improve Hydra's xz compression ratio
+  leangz-raw = leangz.overrideAttrs { cargoBuildNoDefaultFeatures = true; };
 
-  src = fetchFromGitHub {
-    owner = "leanprover-community";
-    repo = "mathlib4";
-    tag = "v4.30.0";
-    hash = "sha256-RxOxdUiVUAxUbfVhxlkjmPX1V64EtmIIn1eW75TiJWA=";
-  };
+  mathlib__archive = buildLakePackage (finalAttrs: {
+    pname = "lean4-mathlib";
+    # nixpkgs-update: no auto update
+    version = "4.30.0";
 
-  leanPackageName = "mathlib";
-  leanDeps = [
-    batteries
-    aesop
-    Qq
-    proofwidgets
-    plausible
-    LeanSearchClient
-    importGraph
-  ];
+    src = fetchFromGitHub {
+      owner = "leanprover-community";
+      repo = "mathlib4";
+      tag = "v${finalAttrs.version}";
+      hash = "sha256-RxOxdUiVUAxUbfVhxlkjmPX1V64EtmIIn1eW75TiJWA=";
+    };
 
-  requiredSystemFeatures = [ "big-parallel" ];
-
-  passthru.tests = {
-    inherit (tests.lake) weak-minimax;
-  };
-
-  meta = {
-    description = "Mathematical library for Lean 4";
-    homepage = "https://github.com/leanprover-community/mathlib4";
-    license = lib.licenses.asl20;
-    maintainers = with lib.maintainers; [
-      nadja-y
-      niklashh
+    leanPackageName = "mathlib";
+    leanDeps = [
+      batteries
+      aesop
+      Qq
+      proofwidgets
+      plausible
+      LeanSearchClient
+      importGraph
     ];
-  };
-}
+
+    nativeBuildInputs = [ leangz-raw ];
+
+    # 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 = ''
+      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 = {
+      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 = [ leangz-raw ];
+    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
+    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/plausible/default.nix b/pkgs/development/lean-modules/plausible/default.nix
index 6f4d08d0ee28..34cf8fe6cb29 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.30.0";
+  # nixpkgs-update: no auto update
+  version = "4.30.0-unstable-2026-05-26";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "plausible";
-    tag = "v4.30.0";
+    rev = "a456461b368b71d2accd95234832cd9c174b5437";
     hash = "sha256-DSaS0W2cfCUh2N+7WyiM7aUv3trtRNON0PzCgCW2SKY=";
   };
 
@@ -21,9 +22,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..e0df936ad74c 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.99";
+
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "ProofWidgets4";
-    tag = "v${version}";
-    hash = "sha256-LETljr+QEU6CxprR3pB4hUzhgCD8PrIuiPOgTIdhHVM=";
+    tag = "v${finalAttrs.version}";
+    hash = "sha256-kGoEkKGrucNUWFYkHW2LsS1gI4C0J8bAHQL2MiE4Pzc=";
   };
-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=";
+    hash = "sha256-ssWSr2qfsIbX25DidiVPm0tsLGjrhQhQ6YKPL0rfc1k=";
   };
   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)"
@@ -62,9 +53,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 ];
   };
-}
+})
diff --git a/pkgs/development/lean-modules/update.sh b/pkgs/development/lean-modules/update.sh
index fc05fe41b5c5..76691bb6b475 100755
--- a/pkgs/development/lean-modules/update.sh
+++ b/pkgs/development/lean-modules/update.sh
@@ -1,30 +1,15 @@
 #!/usr/bin/env nix-shell
-#!nix-shell -i bash -p nix-update common-updater-scripts curl jq
+#!nix-shell -i bash -p curl jq gh
 
-# Update the leanPackages set.
-#
-# 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)
 
-# 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 "")
-
-run() { 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.
+dir=$(dirname "$0")
+FAKE="sha256-AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA="
 
 manifest=$(curl -sL "https://raw.githubusercontent.com/leanprover-community/mathlib4/v${lean4_version}/lake-manifest.json")
 
@@ -37,47 +22,77 @@ 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: updated dependency tree for lean4 $lean4_version"
+echo "https://github.com/leanprover-community/mathlib4/blob/v${lean4_version}/lake-manifest.json"
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;
 })