diff --git a/Lake/Build.lean b/Lake/Build.lean index f90283186e..69b98bfd26 100644 --- a/Lake/Build.lean +++ b/Lake/Build.lean @@ -172,7 +172,7 @@ def Package.buildTargetWithDepTargetsFor (mod : Name) (depTargets : List PackageTarget) (self : Package) : IO PackageTarget := do let depsTarget ← LeanTarget.all <| - self.moreDepsTarget.withArtifact arbitrary :: depTargets + (← self.buildMoreDepsTarget).withArtifact arbitrary :: depTargets let oLeanDirs := depTargets.map (·.package.oleanDir) let (target, targetMap) ← self.buildModuleTargetDAGFor mod oLeanDirs depsTarget return {target with artifact := ⟨self, targetMap⟩} @@ -219,7 +219,7 @@ def Package.buildModuleTargetsWithDeps : IO (List ModuleTarget) := do let oleanDirs := deps.map (·.oleanDir) let depsTarget ← LeanTarget.all <| - self.moreDepsTarget.withArtifact arbitrary :: (← deps.mapM (·.buildTarget)) + (← self.buildMoreDepsTarget).withArtifact arbitrary :: (← deps.mapM (·.buildTarget)) self.buildModuleTargets mods oleanDirs depsTarget def Package.buildModulesWithDeps diff --git a/Lake/Package.lean b/Lake/Package.lean index 8cb9345cac..e05435a9a7 100644 --- a/Lake/Package.lean +++ b/Lake/Package.lean @@ -49,7 +49,7 @@ structure PackageConfig where libName : String := moduleRoot.toString (escape := false) depsDir : FilePath := defaultDepsDir dependencies : List Dependency := [] - moreDepsTarget : BuildTarget LeanTrace PUnit := BuildTarget.nil + buildMoreDepsTarget : IO (BuildTarget LeanTrace PUnit) := BuildTarget.nil scripts : HashMap String Script := HashMap.empty deriving Inhabited @@ -83,8 +83,8 @@ def moduleRootName (self : Package) : String := def dependencies (self : Package) : List Dependency := self.config.dependencies -def moreDepsTarget (self : Package) : BuildTarget LeanTrace PUnit := - self.config.moreDepsTarget +def buildMoreDepsTarget (self : Package) : IO (BuildTarget LeanTrace PUnit) := + self.config.buildMoreDepsTarget def leanArgs (self : Package) : Array String := self.config.leanArgs