chore: use libPrefixOnWindows in core build (#10617)

This PR switches the core build Lake configuration file to use
`libPrefixOnWindows` rather than a CMake hack.

It also removes some dead TOML variables from the CMake configuration.

Author: tydeu

src/CMakeLists.txt

@@ -844,16 +844,8 @@ endfunction()
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_CC "${LEANC_CC}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_FLAGS "${LEANC_INTERNAL_FLAGS}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_LINKER_FLAGS "${LEANC_INTERNAL_LINKER_FLAGS}")
-set(LEANC_OPTS_TOML "${LEANC_OPTS} ${LEANC_EXTRA_CC_FLAGS} ${LEANC_INTERNAL_FLAGS}")
-set(LINK_OPTS_TOML "${LEANC_INTERNAL_LINKER_FLAGS} -L${CMAKE_BINARY_DIR}/lib/lean ${LEAN_EXTRA_LINKER_FLAGS}")
 
 toml_escape("${LEAN_EXTRA_MAKE_OPTS}" LEAN_EXTRA_OPTS_TOML)
-toml_escape("${LEANC_OPTS_TOML}" LEANC_OPTS_TOML)
-toml_escape("${LINK_OPTS_TOML}" LINK_OPTS_TOML)
-
-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}")

src/lakefile.toml.in

@@ -21,6 +21,9 @@ buildDir = "${CMAKE_BINARY_DIR}"
 # will expect the previous stage's artifacts to be in the build directory.
 restoreAllArtifacts = true
 
+# Lean expects its libraries to always have a `lib` prefix
+libPrefixOnWindows = true
+
 # The directory of Lean source files (i.e., `src`)
 srcDir = "${LEAN_SOURCE_DIR}"
 
@@ -46,17 +49,14 @@ ${LEAN_EXTRA_LAKEFILE_TOML}
 
 [[lean_lib]]
 name = "Init"
-libName = "${LAKE_LIB_PREFIX}Init"
 defaultFacets = ["static", "static.export"]
 
 [[lean_lib]]
 name = "Std"
-libName = "${LAKE_LIB_PREFIX}Std"
 defaultFacets = ["static", "static.export"]
 
 [[lean_lib]]
 name = "Lean"
-libName = "${LAKE_LIB_PREFIX}Lean"
 defaultFacets = ["static", "static.export"]
 globs = [
   # Library root
@@ -72,17 +72,14 @@ name = "Lake"
 srcDir = "lake"
 # Build Lake and all its submodules (which may not be imported elsewhere)
 globs = ["Lake.*"]
-libName = "${LAKE_LIB_PREFIX}Lake"
 defaultFacets = ["static", "static.export"]
 
 [[lean_lib]]
 name = "LakeMain"
 srcDir = "lake"
-libName = "${LAKE_LIB_PREFIX}LakeMain"
 defaultFacets = ["static.export"]
 
 [[lean_lib]]
 name = "Leanc"
 srcDir = "${CMAKE_BINARY_DIR}/leanc"
-libName = "${LAKE_LIB_PREFIX}Leanc"
 defaultFacets = ["static"]