fix: lake: better library plugin heuristic (#8528)

This PR fixes the heuristic Lake uses to determine whether a `lean_lib`
can be loaded via `lean --plugin` rather than `lean --load-dynlib`.
Previously, a mismatch between the single root's name and the library's
name would not be caught and cause loading to fail.

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

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