max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: only pass known CMake build types to Lake (#10595)

Browse source 
This PR ensures that Lake only receives recognized CMake build types
from CMake. This fixes an issue with #10581 which broke the
`RelWithAssert` build.
This commit is contained in:
Mac Malone 2025-09-27 13:47:15 -04:00 • committed by GitHub
parent 69b8b0098c
commit fbfc7694a0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/CMakeLists.txt
View file

@ -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

4
src/lakefile.toml.in
View file

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