Skip to content
This repository was archived by the owner on Oct 25, 2023. It is now read-only.

Commit d0896b3

Browse files
committed
fix: use library, not package, for lean root dir
1 parent d23660c commit d0896b3

File tree

3 files changed

+9
-2
lines changed

3 files changed

+9
-2
lines changed

Diff for: Lake/Build/Module.lean

+2-2
Original file line numberDiff line numberDiff line change
@@ -25,12 +25,12 @@ def Module.soloTarget (mod : Module) (dynlibs : Array FilePath)
2525
let cUpToDate ← modTrace.checkAgainstFile mod.cFile mod.cTraceFile
2626
unless modUpToDate && cUpToDate do
2727
compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
28-
(← getOleanPath) mod.pkg.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
28+
(← getOleanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
2929
modTrace.writeToFile mod.cTraceFile
3030
else
3131
unless modUpToDate do
3232
compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile none
33-
(← getOleanPath) mod.pkg.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
33+
(← getOleanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
3434
modTrace.writeToFile mod.traceFile
3535
return depTrace
3636

Diff for: Lake/Config/LeanLib.lean

+4
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,10 @@ namespace LeanLib
3838
@[inline] def srcDir (self : LeanLib) : FilePath :=
3939
self.pkg.srcDir / self.config.srcDir
4040

41+
/-- The library's root directory for `lean` (i.e., `srcDir`). -/
42+
@[inline] def rootDir (self : LeanLib) : FilePath :=
43+
self.srcDir
44+
4145
/-- Whether the given module is considered local to the library. -/
4246
@[inline] def isLocalModule (mod : Name) (self : LeanLib) : Bool :=
4347
self.config.isLocalModule mod

Diff for: Lake/Config/Module.lean

+3
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,9 @@ namespace Module
3838
abbrev pkg (self : Module) : Package :=
3939
self.lib.pkg
4040

41+
@[inline] def rootDir (self : Module) : FilePath :=
42+
self.lib.rootDir
43+
4144
@[inline] def leanFile (self : Module) : FilePath :=
4245
Lean.modToFilePath self.lib.srcDir self.name "lean"
4346

0 commit comments

Comments
 (0)