From fbfc7694a030c3d9639557bdb7bd77d375177d08 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Sat, 27 Sep 2025 13:47:15 -0400
Subject: [PATCH] fix: only pass known CMake build types to Lake (#10595)

This PR ensures that Lake only receives recognized CMake build types
from CMake. This fixes an issue with #10581 which broke the
`RelWithAssert` build.
---
 src/CMakeLists.txt   | 6 ++++++
 src/lakefile.toml.in | 4 ++--
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 17c7bd3509..4982f39e79 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -855,6 +855,12 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   set(LAKE_LIB_PREFIX "lib")
 endif()
 
+if(${CMAKE_BUILD_TYPE} MATCHES "Debug|Release|RelWithDebInfo|MinSizeRel")
+  set(CMAKE_BUILD_TYPE_TOML "${CMAKE_BUILD_TYPE}")
+else()
+  set(CMAKE_BUILD_TYPE_TOML "Release")
+endif()
+
 if(USE_LAKE)
   configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${CMAKE_BINARY_DIR}/lakefile.toml)
   # copy for editing
diff --git a/src/lakefile.toml.in b/src/lakefile.toml.in
index 7c557d1e24..28eb6c6892 100644
--- a/src/lakefile.toml.in
+++ b/src/lakefile.toml.in
@@ -10,8 +10,8 @@ bootstrap = true
 
 defaultTargets = ["Init", "Std", "Lean", "Lake", "LakeMain", "Leanc"]
 
-# Ensure that Lake and CMake agree on the build type (e.g., `Release`, `Debug`)
-buildType = "${CMAKE_BUILD_TYPE}"
+# Have Lake use CMake's build type (e.g., `Release`, `Debug`) where possible
+buildType = "${CMAKE_BUILD_TYPE_TOML}"
 
 # The root of all the compiler output directories
 buildDir = "${CMAKE_BINARY_DIR}"