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