From deef4e8e23dabf4940a3d083b569e523b05738f4 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Sat, 19 Jul 2025 00:46:42 -0400 Subject: [PATCH] feat: lake: `libPrefixOnWindows` (#9435) This PR adds the `libPrefixOnWindows` package and library configuration option. When enabled, Lake will prefix static and shared libraries with `lib` on Windows (i.e., the same way it does on Unix). --- src/lake/Lake/Config/LeanLib.lean | 8 ++++++-- src/lake/Lake/Config/LeanLibConfig.lean | 11 +++++++++++ src/lake/Lake/Config/Package.lean | 24 ++++++++++++++++++++---- src/lake/Lake/Util/NativeLib.lean | 11 +++++------ src/lake/examples/targets/lakefile.lean | 1 + src/lake/examples/targets/test.sh | 9 +++++++-- 6 files changed, 50 insertions(+), 14 deletions(-) diff --git a/src/lake/Lake/Config/LeanLib.lean b/src/lake/Lake/Config/LeanLib.lean index bf095369f2..15a60b5ab4 100644 --- a/src/lake/Lake/Config/LeanLib.lean +++ b/src/lake/Lake/Config/LeanLib.lean @@ -53,9 +53,13 @@ The names of the library's root modules @[inline] def libName (self : LeanLib) : String := self.config.libName +/-- Whether this library's native binaries should be prefixed with `lib` on Windows. -/ +@[inline] def libPrefixOnWindows (self : LeanLib) : Bool := + self.config.libPrefixOnWindows || self.pkg.libPrefixOnWindows + /-- The file name of the library's static binary (i.e., its `.a`) -/ @[inline] def staticLibFileName (self : LeanLib) : FilePath := - nameToStaticLib self.config.libName + nameToStaticLib self.config.libName self.libPrefixOnWindows /-- The path to the static library in the package's `libDir`. -/ @[inline] def staticLibFile (self : LeanLib) : FilePath := @@ -67,7 +71,7 @@ The names of the library's root modules /-- The file name of the library's shared binary (i.e., its `dll`, `dylib`, or `so`) . -/ @[inline] def sharedLibFileName (self : LeanLib) : FilePath := - nameToSharedLib self.config.libName + nameToSharedLib self.config.libName self.libPrefixOnWindows /-- The path to the shared library in the package's `libDir`. -/ @[inline] def sharedLibFile (self : LeanLib) : FilePath := diff --git a/src/lake/Lake/Config/LeanLibConfig.lean b/src/lake/Lake/Config/LeanLibConfig.lean index 2f52c49230..fd56689b2b 100644 --- a/src/lake/Lake/Config/LeanLibConfig.lean +++ b/src/lake/Lake/Config/LeanLibConfig.lean @@ -49,6 +49,17 @@ configuration LeanLibConfig (name : Name) extends LeanConfig where -/ libName : String := name.mangle "" + /-- + Whether static and shared binaries of this library should be prefixed with `lib` on Windows. + + Unlike Unix, Windows does not require native libraries to start with `lib` and, + by convention, they usually do not. However, for consistent naming across all platforms, + users may wish to enable this. + + Defaults to `false`. + -/ + libPrefixOnWindows : Bool := false + /-- An `Array` of targets to build before the executable's modules. -/ needs : Array PartialBuildKey := #[] diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index 8c79d34ba3..873ede6326 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/src/lake/Lake/Config/Package.lean @@ -284,7 +284,8 @@ configuration PackageConfig (name : Name) extends WorkspaceConfig, LeanConfig wh and will remove it if it was already there (when Reservoir is next updated). -/ reservoir : Bool := true - /- + + /-- Whether to enables Lake's local, offline artifact cache for the package. Artifacts (i.e., build products) of packages will be shared across @@ -296,11 +297,22 @@ configuration PackageConfig (name : Name) extends WorkspaceConfig, LeanConfig wh in their usual location within the build directory. Thus, projects with custom build scripts that rely on specific location of artifacts may wish to disable this feature. - If `none`, the cache will be disabled by default unless the `LAKE_ARTIFACT_CACHE` - environment variable is set to true. + If `none` (the default), the cache will be disabled by default unless + the `LAKE_ARTIFACT_CACHE` environment variable is set to true. -/ enableArtifactCache?, enableArtifactCache : Option Bool := none + /-- + Whether native libraries (of this package) should be prefixed with `lib` on Windows. + + Unlike Unix, Windows does not require native libraries to start with `lib` and, + by convention, they usually do not. However, for consistent naming across all platforms, + users may wish to enable this. + + Defaults to `false`. + -/ + libPrefixOnWindows : Bool := false + instance : EmptyCollection (PackageConfig n) := ⟨{}⟩ /-- The package's name. -/ @@ -625,7 +637,11 @@ def nativeLibDir (self : Package) : FilePath := @[inline] def irDir (self : Package) : FilePath := self.buildDir / self.config.irDir.normalize - /-- The package's `enableArtifactCache?` configuration. -/ +/-- The package's `libPrefixOnWindows` configuration. -/ +@[inline] def libPrefixOnWindows (self : Package) : Bool := + self.config.libPrefixOnWindows + +/-- The package's `enableArtifactCache?` configuration. -/ @[inline] def enableArtifactCache? (self : Package) : Option Bool := self.config.enableArtifactCache? diff --git a/src/lake/Lake/Util/NativeLib.lean b/src/lake/Lake/Util/NativeLib.lean index abdf6bd441..b585fc61c5 100644 --- a/src/lake/Lake/Util/NativeLib.lean +++ b/src/lake/Lake/Util/NativeLib.lean @@ -16,14 +16,13 @@ def sharedLibExt : String := else "so" /-- Convert a library name into its static library file name for the `Platform`. -/ -def nameToStaticLib (name : String) : String := - if Platform.isWindows then s!"{name}.a" else s!"lib{name}.a" +def nameToStaticLib (name : String) (libPrefixOnWindows := false) : String := + if libPrefixOnWindows || !System.Platform.isWindows then s!"lib{name}.a" else s!"{name}.a" /-- Convert a library name into its shared library file name for the `Platform`. -/ -def nameToSharedLib (name : String) : String := - if Platform.isWindows then s!"{name}.dll" - else if Platform.isOSX then s!"lib{name}.dylib" - else s!"lib{name}.so" +def nameToSharedLib (name : String) (libPrefixOnWindows := false) : String := + let libPrefix := if libPrefixOnWindows || !System.Platform.isWindows then "lib" else "" + s!"{libPrefix}{name}.{sharedLibExt}" /-- The environment variable that stores the search path diff --git a/src/lake/examples/targets/lakefile.lean b/src/lake/examples/targets/lakefile.lean index 821a990842..5153059068 100644 --- a/src/lake/examples/targets/lakefile.lean +++ b/src/lake/examples/targets/lakefile.lean @@ -10,6 +10,7 @@ lean_lib Foo where lean_lib Bar where defaultFacets := #[LeanLib.sharedFacet] + libPrefixOnWindows := true lean_lib Baz where extraDepTargets := #[`caw] diff --git a/src/lake/examples/targets/test.sh b/src/lake/examples/targets/test.sh index e8b6ba68b0..9bd3f5ca9d 100755 --- a/src/lake/examples/targets/test.sh +++ b/src/lake/examples/targets/test.sh @@ -76,10 +76,15 @@ cat ./.lake/build/meow.txt | grep Meow! # Test shared lib facets test ! -f ./.lake/build/lib/${LIB_PREFIX}Foo.$SHARED_LIB_EXT -test ! -f ./.lake/build/lib/${LIB_PREFIX}Bar.$SHARED_LIB_EXT +test ! -f ./.lake/build/lib/libBar.$SHARED_LIB_EXT $LAKE build Foo:shared Bar test -f ./.lake/build/lib/${LIB_PREFIX}Foo.$SHARED_LIB_EXT -test -f ./.lake/build/lib/${LIB_PREFIX}Bar.$SHARED_LIB_EXT +test -f ./.lake/build/lib/libBar.$SHARED_LIB_EXT + +# Test static lib facet +test ! -f ./.lake/build/lib/libBar.a +$LAKE build Foo:shared Bar:static +test -f ./.lake/build/lib/libBar.a # Test dynlib facet test ! -f ./.lake/build/lib/lean/Foo.$SHARED_LIB_EXT