fix: only pass known CMake build types to Lake

Author: tydeu

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

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}"