From 3b72c7d1930197c07f35ea770ea13ff2ae4ddceb Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Thu, 29 May 2025 13:48:05 -0400 Subject: [PATCH] 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 | 2 +- src/lake/Lake/Config/LeanLib.lean | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) 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