diff --git a/src/lake/Lake/Build/Library.lean b/src/lake/Lake/Build/Library.lean index 6268e60b28..18d4dddb1b 100644 --- a/src/lake/Lake/Build/Library.lean +++ b/src/lake/Lake/Build/Library.lean @@ -113,7 +113,7 @@ protected def LeanLib.recBuildShared (self : LeanLib) : FetchM (Job Dynlib) := d (·.push <$> ·.dynlib.fetch) jobs return jobs buildLeanSharedLib self.libName self.sharedLibFile objJobs libJobs - self.weakLinkArgs self.linkArgs (plugin := self.roots.size == 1) + self.weakLinkArgs self.linkArgs self.isPlugin /-- The `LibraryFacetConfig` for the builtin `sharedFacet`. -/ def LeanLib.sharedFacetConfig : LibraryFacetConfig sharedFacet := diff --git a/src/lake/Lake/Config/LeanLib.lean b/src/lake/Lake/Config/LeanLib.lean index 31f24b315b..ffb9407399 100644 --- a/src/lake/Lake/Config/LeanLib.lean +++ b/src/lake/Lake/Config/LeanLib.lean @@ -73,6 +73,10 @@ The names of the library's root modules @[inline] def sharedLibFile (self : LeanLib) : FilePath := self.pkg.sharedLibDir / self.sharedLibFileName +/-- Whether the shared binary of this library is a valid plugin. -/ +def isPlugin (self : LeanLib) : Bool := + self.roots == #[self.name] && self.libName == self.name.mangle "" + /-- The library's `extraDepTargets` configuration. -/ @[inline] def extraDepTargets (self : LeanLib) := self.config.extraDepTargets