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.
This commit is contained in:
Archit Gupta
2026-09-14 01:11:15 -07:00
parent 88aca26684
commit 8babb02766
2 changed files with 2 additions and 0 deletions

View File

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

View File

@@ -95,6 +95,7 @@ let
"-DINSTALL_LICENSE=OFF"
"-DINSTALL_CADICAL=OFF"
"-DINSTALL_LEANTAR=OFF"
"-DSTAGE1_CMAKE_INSTALL_PREFIX=${placeholder "out"}"
"-DUSE_MIMALLOC=ON"
];