max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: lake: libPrefixOnWindows on libName (#10579)

Browse source 
This PR alters `libPrefixOnWindows` behavior to add the `lib` prefix to
the library's `libName` rather than just the file path. This means that
Lake's `-l` will now have the prefix on Windows. While this should not
matter to a MSYS2 build (which accepts both `lib`-prefixed and
unprefixed variants), it should ensure compatibility with MSVC (if that
is ever an issue).
This commit is contained in:
Mac Malone 2025-09-26 21:54:23 -04:00 • committed by GitHub
parent 5b8d4d7210
commit f80d6e7d38
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 8 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/lake/Lake/Config/LeanLib.lean
View file

@ -52,17 +52,19 @@ The names of the library's root modules
@[inline] public def isBuildableModule (mod : Name) (self : LeanLib) : Bool :=
self.config.isBuildableModule mod
/-- The name of the library artifact. -/
@[inline] public def libName (self : LeanLib) : String :=
self.config.libName
/-- Whether this library's native binaries should be prefixed with `lib` on Windows. -/
@[inline] public def libPrefixOnWindows (self : LeanLib) : Bool :=
self.config.libPrefixOnWindows || self.pkg.libPrefixOnWindows
/-- The name of the native library (e.g., what is passed to `-l`). -/
public def libName (self : LeanLib) : String :=
if self.libPrefixOnWindows && System.Platform.isWindows then
s!"lib{self.config.libName}"
else self.config.libName
/-- The file name of the library's static binary (i.e., its `.a`) -/
@[inline] public def staticLibFileName (self : LeanLib) : FilePath :=
nameToStaticLib self.config.libName self.libPrefixOnWindows
nameToStaticLib self.libName
/-- The path to the static library in the package's `libDir`. -/
@[inline] public def staticLibFile (self : LeanLib) : FilePath :=
@ -74,7 +76,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] public def sharedLibFileName (self : LeanLib) : FilePath :=
nameToSharedLib self.config.libName self.libPrefixOnWindows
nameToSharedLib self.libName
/-- The path to the shared library in the package's `libDir`. -/
@[inline] public def sharedLibFile (self : LeanLib) : FilePath :=