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

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

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 := #[]
 

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?
 

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

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]

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