@@ -21,6 +21,9 @@ buildDir = "${CMAKE_BINARY_DIR}"
2121# will expect the previous stage's artifacts to be in the build directory.
2222restoreAllArtifacts = true
2323
24+ # Lean expects its libraries to always have a `lib` prefix
25+ libPrefixOnWindows = true
26+
2427# The directory of Lean source files (i.e., `src`)
2528srcDir = "${LEAN_SOURCE_DIR}"
2629
@@ -46,17 +49,14 @@ ${LEAN_EXTRA_LAKEFILE_TOML}
4649
4750[[lean_lib]]
4851name = "Init"
49- libName = "${LAKE_LIB_PREFIX}Init"
5052defaultFacets = ["static", "static.export"]
5153
5254[[lean_lib]]
5355name = "Std"
54- libName = "${LAKE_LIB_PREFIX}Std"
5556defaultFacets = ["static", "static.export"]
5657
5758[[lean_lib]]
5859name = "Lean"
59- libName = "${LAKE_LIB_PREFIX}Lean"
6060defaultFacets = ["static", "static.export"]
6161globs = [
6262 # Library root
@@ -72,17 +72,14 @@ name = "Lake"
7272srcDir = "lake"
7373# Build Lake and all its submodules (which may not be imported elsewhere)
7474globs = ["Lake.*"]
75- libName = "${LAKE_LIB_PREFIX}Lake"
7675defaultFacets = ["static", "static.export"]
7776
7877[[lean_lib]]
7978name = "LakeMain"
8079srcDir = "lake"
81- libName = "${LAKE_LIB_PREFIX}LakeMain"
8280defaultFacets = ["static.export"]
8381
8482[[lean_lib]]
8583name = "Leanc"
8684srcDir = "${CMAKE_BINARY_DIR}/leanc"
87- libName = "${LAKE_LIB_PREFIX}Leanc"
8885defaultFacets = ["static"]
0 commit comments