diff --git a/Lake/BuildModule.lean b/Lake/BuildModule.lean index 98bde859e4..90ba69da24 100644 --- a/Lake/BuildModule.lean +++ b/Lake/BuildModule.lean @@ -16,18 +16,29 @@ open Lean hiding SearchPath namespace Lake --- # Build Target +-- # Targets + +abbrev OleanTarget := ActiveFileTarget structure ModuleArtifact where oleanFile : FilePath cFile : FilePath deriving Inhabited -protected def ModuleArtifact.getMTime (self : ModuleArtifact) : IO MTime := do - return max (← getMTime self.oleanFile) (← getMTime self.cFile) +namespace ModuleArtifact + +protected def getMTime (self : ModuleArtifact) : IO MTime := do + return mixTrace (← getMTime self.oleanFile) (← getMTime self.cFile) instance : GetMTime ModuleArtifact := ⟨ModuleArtifact.getMTime⟩ +protected def computeHash (self : ModuleArtifact) : IO Hash := do + return mixTrace (← computeHash self.oleanFile) (← computeHash self.cFile) + +instance : ComputeHash ModuleArtifact := ⟨ModuleArtifact.computeHash⟩ + +end ModuleArtifact + abbrev ModuleTarget := ActiveBuildTarget ModuleArtifact namespace ModuleTarget @@ -58,65 +69,96 @@ def checkIfSameHash (hash : Hash) (file : FilePath) : IO Bool := def skipIf [Pure m] [Pure n] (cond : Bool) (build : m (n PUnit)) : m (n PUnit) := do if cond then pure (pure ()) else build --- # Build Modules +def checkModuleTrace [GetMTime a] (artifact : a) +(leanFile hashFile : FilePath) (contents : String) (depTrace : LakeTrace) +: IO (Bool × LakeTrace) := do + let leanMTime ← getMTime leanFile + let leanHash := Hash.compute contents + let maxMTime := max leanMTime depTrace.mtime + let fullHash := Hash.mix leanHash depTrace.hash + let sameHash ← checkIfSameHash fullHash hashFile + try + discard <| getMTime artifact -- ensure the artifact actually exists + let mtime := ite sameHash 0 maxMTime + (sameHash, ⟨fullHash, mtime⟩) + catch _ => + (false, ⟨fullHash, maxMTime⟩) + +-- # Module Builders + +def fetchModuleTarget (pkg : Package) (moreOleanDirs : List FilePath) +(mod : Name) (leanFile : FilePath) (contents : String) (depTarget : ActiveOpaqueTarget) +: BuildM ModuleTarget := do + let cFile := pkg.modToC mod + let oleanFile := pkg.modToOlean mod + let artifact := ModuleArtifact.mk oleanFile cFile + let hashFile := pkg.modToHashFile mod + let oleanDirs := pkg.oleanDir :: moreOleanDirs + let (upToDate, trace) ← checkModuleTrace artifact leanFile hashFile contents depTarget.trace + ActiveTarget.mk artifact trace <| ← skipIf upToDate <| depTarget.andThen do + compileOleanAndC leanFile oleanFile cFile oleanDirs pkg.rootDir pkg.leanArgs + IO.FS.writeFile hashFile trace.hash.toString + +def fetchModuleOleanTarget (pkg : Package) (moreOleanDirs : List FilePath) +(mod : Name) (leanFile : FilePath) (contents : String) (depTarget : ActiveOpaqueTarget) +: BuildM OleanTarget := do + let oleanFile := pkg.modToOlean mod + let hashFile := pkg.modToHashFile mod + let oleanDirs := pkg.oleanDir :: moreOleanDirs + let (upToDate, trace) ← checkModuleTrace oleanFile leanFile hashFile contents depTarget.trace + ActiveTarget.mk oleanFile trace <| ← skipIf upToDate <| depTarget.andThen do + compileOlean leanFile oleanFile oleanDirs pkg.rootDir pkg.leanArgs + IO.FS.writeFile hashFile trace.hash.toString + +-- # Recursive Fetching /- Produces a recursive module target fetcher that - builds the target module after waiting for `depTargets` to materialize - and recursively fetching its local imports (relative to `pkg`). - - The module is built with the configuration from `pkg` and - a `LEAN_PATH` that includes `oleanDirs`. + builds the target module after recursively fetching its local imports + (relative to `pkg`). -/ -def fetchModuleWithLocalImports -(pkg : Package) (oleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) -{m} [Monad m] [MonadLiftT BuildM m] [MonadExceptOf IO.Error m] : RecFetch Name ModuleTarget m := +def recFetchModuleWithLocalImports (pkg : Package) +[Monad m] [MonadLiftT BuildM m] (build : Name → FilePath → String → List α → m α) +: RecFetch Name α m := fun mod fetch => do have : MonadLift BuildM m := ⟨liftM⟩ - let leanPath := SearchPath.toString <| pkg.oleanDir :: oleanDirs - fun mod fetch => do - let leanFile := pkg.modToSrc mod - let contents ← liftM (m := BuildM) <| IO.FS.readFile leanFile - -- parse direct local imports - let (imports, _, _) ← Elab.parseImports contents leanFile.toString - let imports := imports.map (·.module) |>.filter (·.getRoot == pkg.moduleRoot) - -- we fetch the import targets even if a rebuild is not required - -- because other build processes (ex. `.o`) rely on the map being complete - let importTargets ← imports.mapM fetch - -- calculate trace - let leanMTime ← getMTime leanFile - let leanHash := Hash.compute contents - let depTrace := mixTrace depTarget.trace - (mixTraceList <| importTargets.map (·.trace)) - let maxMTime := max leanMTime depTrace.mtime - let fullHash := Hash.mix leanHash depTrace.hash - let hashFile := pkg.modToHashFile mod - let sameHash ← checkIfSameHash fullHash hashFile - let mtime := ite sameHash 0 maxMTime - -- construct target - let cFile := pkg.modToC mod - let oleanFile := pkg.modToOlean mod - let depTasks := depTarget.task :: importTargets.map (·.task) - ActiveTarget.mk ⟨oleanFile, cFile⟩ ⟨fullHash, mtime⟩ <| ← - skipIf sameHash <| afterTaskList (m := BuildM) depTasks do - compileOleanAndC leanFile oleanFile cFile leanPath pkg.rootDir pkg.leanArgs - IO.FS.writeFile hashFile fullHash.toString + let leanFile := pkg.modToSrc mod + let contents ← IO.FS.readFile leanFile + -- parse direct local imports + let (imports, _, _) ← Elab.parseImports contents leanFile.toString + let imports := imports.map (·.module) |>.filter (·.getRoot == pkg.moduleRoot) + -- we fetch the import targets even if a rebuild is not required + -- because other build processes (ex. `.o`) rely on the map being complete + let importTargets ← imports.mapM fetch + build mod leanFile contents importTargets +def recFetchModuleTargetWithLocalImports [Monad m] [MonadLiftT BuildM m] +(pkg : Package) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) +: RecFetch Name ModuleTarget m := + recFetchModuleWithLocalImports pkg fun mod leanFile contents importTargets => do + let importTarget ← ActiveOpaqueTarget.collectList importTargets + let allDepTarget ← depTarget.andThenTargetAsync importTarget + fetchModuleTarget pkg moreOleanDirs mod leanFile contents allDepTarget + +def recFetchModuleOleanTargetWithLocalImports [Monad m] [MonadLiftT BuildM m] +(pkg : Package) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) +: RecFetch Name OleanTarget m := + recFetchModuleWithLocalImports pkg fun mod leanFile contents importTargets => do + let importTarget ← ActiveOpaqueTarget.collectList importTargets + let allDepTarget ← depTarget.andThenTargetAsync importTarget + fetchModuleOleanTarget pkg moreOleanDirs mod leanFile contents allDepTarget + +-- ## Definitions + +abbrev ModuleM (α) := + -- equivalent to `RBTopT (cmp := Name.quickCmp) Name ModuleTarget BuildM`. + -- phrased this way to use `NameMap` + EStateT (List Name) (NameMap α) BuildM + +abbrev ModuleFetch (α) := + RecFetch Name α (ModuleM α) + +abbrev OleanTargetFetch := ModuleFetch OleanTarget +abbrev ModuleTargetFetch := ModuleFetch ModuleTarget + +abbrev OleanTargetMap := NameMap OleanTarget abbrev ModuleTargetMap := NameMap ModuleTarget - -/- - Equivalent to `RBTopT (cmp := Name.quickCmp) Name ModuleTarget BuildM`. - Phrased this way to use `ModuleTargetMap`. --/ -abbrev ModuleTargetM := - EStateT (List Name) ModuleTargetMap BuildM - -abbrev ModuleTargetFetch := - RecFetch Name ModuleTarget ModuleTargetM - -def failOnCycle : Except (List Name) α → BuildM α -| Except.ok a => a -| Except.error cycle => do - let cycle := cycle.map (s!" {·}") - let msg := s!"import cycle detected:\n{"\n".intercalate cycle}" - BuildM.logError msg - throw <| IO.userError msg diff --git a/Lake/BuildPackage.lean b/Lake/BuildPackage.lean index cb970211da..026cd82332 100644 --- a/Lake/BuildPackage.lean +++ b/Lake/BuildPackage.lean @@ -35,32 +35,63 @@ end PackageTarget -- # Build Modules def Package.buildModuleTargetDAGFor -(mod : Name) (oleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) +(mod : Name) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) : BuildM (ModuleTarget × ModuleTargetMap) := do - let fetch := fetchModuleWithLocalImports self oleanDirs depTarget - failOnCycle <| ← buildRBTop fetch mod |>.run {} + let fetch := recFetchModuleTargetWithLocalImports self moreOleanDirs depTarget + failOnImportCycle <| ← buildRBTop fetch mod |>.run {} + +def Package.buildOleanTargetDAGFor +(mod : Name) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) +(self : Package) : BuildM (OleanTarget × OleanTargetMap) := do + let fetch := recFetchModuleOleanTargetWithLocalImports self moreOleanDirs depTarget + failOnImportCycle <| ← buildRBTop fetch mod |>.run {} def Package.buildModuleTargetDAG -(oleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) := - self.buildModuleTargetDAGFor self.moduleRoot oleanDirs depTarget +(moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) := + self.buildModuleTargetDAGFor self.moduleRoot moreOleanDirs depTarget + +def Package.buildOleanTargetDAG +(moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) := + self.buildOleanTargetDAGFor self.moduleRoot moreOleanDirs depTarget def Package.buildModuleTargets -(mods : List Name) (oleanDirs : List FilePath) +(mods : List Name) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) : BuildM (List ModuleTarget) := do - let fetch : ModuleTargetFetch := fetchModuleWithLocalImports self oleanDirs depTarget - failOnCycle <| ← mods.mapM (buildRBTop fetch) |>.run' {} + let fetch : ModuleTargetFetch := + recFetchModuleTargetWithLocalImports self moreOleanDirs depTarget + failOnImportCycle <| ← mods.mapM (buildRBTop fetch) |>.run' {} + +def Package.buildOleanTargets +(mods : List Name) (moreOleanDirs : List FilePath) +(depTarget : ActiveOpaqueTarget) (self : Package) +: BuildM (List OleanTarget) := do + let fetch : OleanTargetFetch := + recFetchModuleOleanTargetWithLocalImports self moreOleanDirs depTarget + failOnImportCycle <| ← mods.mapM (buildRBTop fetch) |>.run' {} + +def Package.buildRootModuleTarget +(moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) := + self.buildModuleTargets [self.moduleRoot] moreOleanDirs depTarget |>.map (·.get! 0) + +def Package.buildRootOleanTarget +(moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) := + self.buildOleanTargets [self.moduleRoot] moreOleanDirs depTarget |>.map (·.get! 0) -- # Configure/Build Packages +def Package.buildDepTargetWith +(depTargets : List PackageTarget) (self : Package) : BuildM ActiveOpaqueTarget := do + let extraDepTarget ← self.buildExtraDepTarget + let depTarget ← ActiveOpaqueTarget.collectList depTargets + depTarget.andThenTargetAsync extraDepTarget + def Package.buildTargetWithDepTargetsFor (mod : Name) (depTargets : List PackageTarget) (self : Package) : BuildM PackageTarget := do - let extraDepTarget ← self.buildExtraDepTarget - let depTarget ← ActiveOpaqueTarget.collectList depTargets - let allDepsTarget ← extraDepTarget.andThenTargetAsync depTarget - let oleanDirs := depTargets.map (·.package.oleanDir) - let (target, targetMap) ← self.buildModuleTargetDAGFor mod oleanDirs allDepsTarget + let depTarget ← self.buildDepTargetWith depTargets + let moreOleanDirs := depTargets.map (·.package.oleanDir) + let (target, targetMap) ← self.buildModuleTargetDAGFor mod moreOleanDirs depTarget return {target with artifact := ⟨self, targetMap⟩} def Package.buildTargetWithDepTargets @@ -88,32 +119,33 @@ def configure (pkg : Package) : IO Unit := runBuild pkg.buildDeps def Package.build (self : Package) : BuildM PUnit := do - (← self.buildTarget).materialize + let depTargets ← self.buildDepTargets + let depTarget ← self.buildDepTargetWith depTargets + let moreOleanDirs := depTargets.map (·.package.oleanDir) + let target ← self.buildRootOleanTarget moreOleanDirs depTarget + target.materialize def build (pkg : Package) : IO PUnit := runBuild pkg.build -- # Print Paths -def Package.buildModuleTargetsWithDeps -(deps : List Package) (mods : List Name) (self : Package) -: BuildM (List ModuleTarget) := do - let oleanDirs := deps.map (·.oleanDir) - let extraDepTarget ← self.buildExtraDepTarget - let depTarget ← ActiveOpaqueTarget.collectList <| ← deps.mapM (·.buildTarget) - let allDepsTarget ← extraDepTarget.andThenTargetAsync depTarget - self.buildModuleTargets mods oleanDirs allDepsTarget +def Package.buildOleanTargetsWithDeps +(deps : List Package) (mods : List Name) (self : Package) +: BuildM (List OleanTarget) := do + let moreOleanDirs := deps.map (·.oleanDir) + let depTarget ← self.buildDepTargetWith <| ← deps.mapM (·.buildTarget) + self.buildOleanTargets mods moreOleanDirs depTarget -def Package.buildModulesWithDeps -(deps : List Package) (mods : List Name) (self : Package) -: BuildM PUnit := do - (← self.buildModuleTargetsWithDeps deps mods).forM (·.materialize) +def Package.buildOleansWithDeps +(deps : List Package) (mods : List Name) (self : Package) := + self.buildOleanTargetsWithDeps deps mods >>= (·.forM (·.materialize)) def printPaths (pkg : Package) (imports : List String := []) : IO Unit := do let deps ← solveDeps pkg unless imports.isEmpty do let imports := imports.map (·.toName) let localImports := imports.filter (·.getRoot == pkg.moduleRoot) - runBuild <| pkg.buildModulesWithDeps deps localImports + runBuild <| pkg.buildOleansWithDeps deps localImports IO.println <| SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir) IO.println <| SearchPath.toString <| pkg.srcDir :: deps.map (·.srcDir) diff --git a/Lake/Compile.lean b/Lake/Compile.lean index 85ba6b91d8..f9e1a0115d 100644 --- a/Lake/Compile.lean +++ b/Lake/Compile.lean @@ -26,8 +26,20 @@ def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do BuildM.logError msg -- log errors early throw <| IO.userError msg +def compileOlean (leanFile oleanFile : FilePath) +(oleanDirs : List FilePath := []) (rootDir : FilePath := ".") (leanArgs : Array String := #[]) +: BuildM PUnit := do + createParentDirs oleanFile + proc { + cmd := "lean" + args := leanArgs ++ #[ + "-R", rootDir.toString, "-o", oleanFile.toString, leanFile.toString + ] + env := #[("LEAN_PATH", SearchPath.toString oleanDirs)] + } + def compileOleanAndC (leanFile oleanFile cFile : FilePath) -(leanPath : String := "") (rootDir : FilePath := ".") (leanArgs : Array String := #[]) +(oleanDirs : List FilePath := []) (rootDir : FilePath := ".") (leanArgs : Array String := #[]) : BuildM PUnit := do createParentDirs cFile createParentDirs oleanFile @@ -37,7 +49,7 @@ def compileOleanAndC (leanFile oleanFile cFile : FilePath) "-R", rootDir.toString, "-o", oleanFile.toString, "-c", cFile.toString, leanFile.toString ] - env := #[("LEAN_PATH", leanPath)] + env := #[("LEAN_PATH", SearchPath.toString oleanDirs)] } def compileO (oFile cFile : FilePath)