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] 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
   '';