leanPackages.lean4: 4.29.0 -> 4.30.0 (#511524)

2026-06-05 21:03:40 +00:00 · 2026-06-04 21:20:34 +00:00
parent fbac98ae6b d63d353258
commit c93cb7ca2e
15 changed files with 254 additions and 186 deletions
--- 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"
--- 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,
--- 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";
  };
 })
--- 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 ];
  };
-}
+})
--- 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 ];
  };
 }
--- 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 ];
  };
 }
--- 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 ];
  };
 }
--- 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 ];
  };
 }
--- 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 ];
  };
 }
--- 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
--- 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
+  ''
--- 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 ];
  };
 }
--- 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 ];
  };
-}
+})
--- 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"
--- 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;
 })