From 8babb027668a78d7ad2bfbeec992e91e695a9a88 Mon Sep 17 00:00:00 2001 From: Archit Gupta Date: Mon, 14 Sep 2026 01:11:15 -0700 Subject: [PATCH] lean4: fix install prefix for CMake 4.4 `lean4` failed to build with CMake 4.4 since CMake started putting help strings for known variables set from the command line. Lean was using the presence of the generic help string to determine if a variable was passed from the command line. For CMAKE_* variables, it considers them as platform variables if they were not passed on the command line. Those variables are then passed only to its stage0 and not stage1. This caused CMAKE_INSTALL_PREFIX to be dropped, since previously the nixpkgs command line override resulted in the generic help string, and with CMake 4.4 it no longer does. This works around this insanity by passing STAGE1_CMAKE_INSTALL_PREFIX which Lean understands for passing CMAKE_INSTALL_PREFIX to its stage1 build. --- pkgs/by-name/le/lean4/package.nix | 1 + pkgs/development/lean-modules/lean4/default.nix | 1 + 2 files changed, 2 insertions(+) diff --git a/pkgs/by-name/le/lean4/package.nix b/pkgs/by-name/le/lean4/package.nix index 8d98ebd2c356..17913e8b1181 100644 --- a/pkgs/by-name/le/lean4/package.nix +++ b/pkgs/by-name/le/lean4/package.nix @@ -93,6 +93,7 @@ stdenv.mkDerivation (finalAttrs: { "-DUSE_GITHASH=OFF" "-DINSTALL_LICENSE=OFF" "-DINSTALL_CADICAL=OFF" + "-DSTAGE1_CMAKE_INSTALL_PREFIX=${placeholder "out"}" "-DUSE_MIMALLOC=${if enableMimalloc then "ON" else "OFF"}" ]; diff --git a/pkgs/development/lean-modules/lean4/default.nix b/pkgs/development/lean-modules/lean4/default.nix index 3f62f6151b8f..d9ce64b4f591 100644 --- a/pkgs/development/lean-modules/lean4/default.nix +++ b/pkgs/development/lean-modules/lean4/default.nix @@ -95,6 +95,7 @@ let "-DINSTALL_LICENSE=OFF" "-DINSTALL_CADICAL=OFF" "-DINSTALL_LEANTAR=OFF" + "-DSTAGE1_CMAKE_INSTALL_PREFIX=${placeholder "out"}" "-DUSE_MIMALLOC=ON" ];