NixOS · nadja-y · Apr 19, 2026
diff --git 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
@@ -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
@@ -1,3 +1,4 @@
+# nixpkgs-update: no auto update
 {
   lib,
   buildLakePackage,

diff --git a/pkgs/development/lean-modules/LeanSearchClient/default.nix b/pkgs/development/lean-modules/LeanSearchClient/default.nix
@@ -1,3 +1,4 @@
+# nixpkgs-update: no auto update
 {
   lib,
   buildLakePackage,
@@ -6,7 +7,6 @@
 
 buildLakePackage {
   pname = "lean4-LeanSearchClient";
-  # No lockstep tags; version pinned by mathlib's lake-manifest.json.
   version = "0-unstable-2026-02-12";
 
   src = fetchFromGitHub {

diff --git a/pkgs/development/lean-modules/Qq/default.nix b/pkgs/development/lean-modules/Qq/default.nix
@@ -1,3 +1,4 @@
+# nixpkgs-update: no auto update
 {
   lib,
   buildLakePackage,
@@ -6,12 +7,12 @@
 
 buildLakePackage {
   pname = "lean4-Qq";
-  version = "4.29.0";
+  version = "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
@@ -1,3 +1,4 @@
+# nixpkgs-update: no auto update
 {
   lib,
   buildLakePackage,
@@ -7,12 +8,12 @@
 
 buildLakePackage {
   pname = "lean4-aesop";
-  version = "4.29.0";
+  version = "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
@@ -1,3 +1,4 @@
+# nixpkgs-update: no auto update
 {
   lib,
   buildLakePackage,
@@ -6,17 +7,27 @@
 
 buildLakePackage {
   pname = "lean4-batteries";
-  version = "4.29.0";
+  version = "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
@@ -1,3 +1,4 @@
+# nixpkgs-update: no auto update
 {
   lib,
   buildLakePackage,
@@ -7,12 +8,12 @@
 
 buildLakePackage {
   pname = "lean4-importGraph";
-  version = "4.29.0";
+  version = "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
@@ -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
@@ -1,3 +1,4 @@
+# nixpkgs-update: no auto update
 {
   lib,
   buildLakePackage,
@@ -12,15 +13,15 @@
   tests,
 }:
 
-buildLakePackage {
+buildLakePackage (finalAttrs: {
   pname = "lean4-mathlib";
-  version = "4.29.0";
+  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
@@ -1,3 +1,4 @@
+# nixpkgs-update: no auto update
 {
   lib,
   buildLakePackage,
@@ -6,12 +7,12 @@
 
 buildLakePackage {
   pname = "lean4-plausible";
-  version = "4.29.0";
+  version = "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
@@ -1,3 +1,4 @@
+# nixpkgs-update: no auto update
 {
   lib,
   buildLakePackage,
@@ -8,12 +9,12 @@
 }:
 
 let
-  version = "0.0.95";
+  version = "0.0.95+lean-v4.29.1";
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "ProofWidgets4";
-    tag = "v${version}";
-    hash = "sha256-LETljr+QEU6CxprR3pB4hUzhgCD8PrIuiPOgTIdhHVM=";
+    tag = "v0.0.95+lean-v4.29.1";
+    hash = "sha256-D1fTsV8W29S1C53ky66sFgIoA5cLx/ilKa98czScV+s=";
   };
 in
 

diff --git 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 nix
 
-# 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,75 @@ if [ "$manifest_deps" != "$known_deps" ]; then
   exit 1
 fi
 
-pw_version=$(echo "$manifest" | jq -r '.packages[] | select(.name == "proofwidgets") | .inputRev' | sed 's/^v//')
-
-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"
+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")
+  if [[ "$inputRev" =~ ^v[0-9] ]]; then
+    version="${inputRev#v}"
+    sed -i -E "s|version = \"[^\"]*\";|version = \"${version}\";|" "$file"
+    if grep -q 'tag = "' "$file"; then
+      sed -i -E "s|tag = \"[^\"]*\";|tag = \"${inputRev}\";|" "$file"
+    else
+      sed -i -E "s|rev = \"[^\"]*\";|tag = \"${inputRev}\";|" "$file"
+    fi
+  else
+    local date
+    date=$(gh api "repos/$repo/commits/$rev" --jq '.commit.committer.date[:10]')
+    version="0-unstable-$date"
+    sed -i -E "s|version = \"[^\"]*\";|version = \"${version}\";|" "$file"
+    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 "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"
+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
+
+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"
+
+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
 
-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
-fi
+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 "commit-title: leanPackages: lean4 $old_lockstep -> $lean4_version"
-echo "---"
-for c in "${changes[@]}"; do
-  echo "  - $c"
-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 "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}"