diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean
index 3e1bc4efa1..167f678fa0 100644
--- a/Lake/Build/Module.lean
+++ b/Lake/Build/Module.lean
@@ -25,12 +25,12 @@ def Module.soloTarget (mod : Module) (dynlibs : Array FilePath)
       let cUpToDate ← modTrace.checkAgainstFile mod.cFile mod.cTraceFile
       unless modUpToDate && cUpToDate do
         compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
-          (← getOleanPath) mod.pkg.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
+          (← getOleanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
       modTrace.writeToFile mod.cTraceFile
     else
       unless modUpToDate do
         compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile none
-          (← getOleanPath) mod.pkg.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
+          (← getOleanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
     modTrace.writeToFile mod.traceFile
     return depTrace
 
diff --git a/Lake/Config/LeanLib.lean b/Lake/Config/LeanLib.lean
index afca1cf398..39bc3d1d54 100644
--- a/Lake/Config/LeanLib.lean
+++ b/Lake/Config/LeanLib.lean
@@ -38,6 +38,10 @@ namespace LeanLib
 @[inline] def srcDir (self : LeanLib) : FilePath :=
   self.pkg.srcDir / self.config.srcDir
 
+/-- The library's root directory for `lean` (i.e., `srcDir`). -/
+@[inline] def rootDir (self : LeanLib) : FilePath :=
+  self.srcDir
+
 /-- Whether the given module is considered local to the library. -/
 @[inline] def isLocalModule (mod : Name) (self : LeanLib) : Bool :=
   self.config.isLocalModule mod
diff --git a/Lake/Config/Module.lean b/Lake/Config/Module.lean
index fd44073981..bf4fe7c444 100644
--- a/Lake/Config/Module.lean
+++ b/Lake/Config/Module.lean
@@ -38,6 +38,9 @@ namespace Module
 abbrev pkg (self : Module) : Package :=
   self.lib.pkg
 
+@[inline] def rootDir (self : Module) : FilePath :=
+  self.lib.rootDir
+
 @[inline] def leanFile (self : Module) : FilePath :=
   Lean.modToFilePath self.lib.srcDir self.name "lean"