diff --git a/Lake/Package.lean b/Lake/Package.lean index 0f74ef1202..9a7fd46306 100644 --- a/Lake/Package.lean +++ b/Lake/Package.lean @@ -101,24 +101,24 @@ def depsDir (self : Package) : FilePath := def srcDir (self : Package) : FilePath := self.dir / self.config.srcDir -def srcRoot (self : Package) : FilePath := - self.srcDir / FilePath.withExtension self.moduleRootName "lean" - def modToSrc (mod : Name) (self : Package) : FilePath := Lean.modToFilePath self.srcDir mod "lean" +def srcRoot (self : Package) : FilePath := + self.modToSrc self.moduleRoot + def oleanDir (self : Package) : FilePath := self.dir / self.config.oleanDir +def modToOlean (mod : Name) (self : Package) : FilePath := + Lean.modToFilePath self.oleanDir mod "olean" + def oleanRoot (self : Package) : FilePath := - self.oleanDir / FilePath.withExtension self.moduleRootName "olean" + self.modToOlean self.moduleRoot def modToHashFile (mod : Name) (self : Package) : FilePath := Lean.modToFilePath self.oleanDir mod "hash" -def modToOlean (mod : Name) (self : Package) : FilePath := - Lean.modToFilePath self.oleanDir mod "olean" - def irDir (self : Package) : FilePath := self.dir / self.config.irDir