From 7ee3079afbdb893b124068078f654269be09a95b Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Fri, 26 Sep 2025 17:06:12 -0400 Subject: [PATCH] feat: lake: CMake build types (#10578) This PR adds support for the CMake spelling of a build type (i.e., capitalized) to Lake's `buildType` configuration option. --- src/lake/Lake/Config/LeanConfig.lean | 2 +- src/lake/tests/translateConfig/source.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lake/Lake/Config/LeanConfig.lean b/src/lake/Lake/Config/LeanConfig.lean index f0dbc5c798..c4d67363e6 100644 --- a/src/lake/Lake/Config/LeanConfig.lean +++ b/src/lake/Lake/Config/LeanConfig.lean @@ -118,7 +118,7 @@ public def leancArgs : BuildType → Array String | release => #["-O3", "-DNDEBUG"] public def ofString? (s : String) : Option BuildType := - match s with + match s.decapitalize with | "debug" => some .debug | "relWithDebInfo" => some .relWithDebInfo | "minSizeRel" => some .minSizeRel diff --git a/src/lake/tests/translateConfig/source.toml b/src/lake/tests/translateConfig/source.toml index b85095a0a3..f6f5cbeffc 100644 --- a/src/lake/tests/translateConfig/source.toml +++ b/src/lake/tests/translateConfig/source.toml @@ -16,7 +16,7 @@ releaseRepo = "" buildArchive = "" preferReleaseBuild = false packagesDir = ".lake/packages" -buildType = "release" +buildType = "Release" leanOptions = [] moreServerOptions = [] moreLeanArgs = []