diff --git a/Lake/BuildBin.lean b/Lake/BuildBin.lean index 7428519905..1033d22646 100644 --- a/Lake/BuildBin.lean +++ b/Lake/BuildBin.lean @@ -37,12 +37,11 @@ def buildLib (pkg : Package) : IO PUnit := -- # Build Package Bin def ActivePackageTarget.linkTargets -(depTargets : List ActivePackageTarget) (self : ActivePackageTarget) : Array FileTarget := - depTargets.foldl (fun ts dep => ts ++ dep.staticLibTargets) <| - self.oFileTargets ++ self.package.moreLibTargets +(depTargets : Array ActivePackageTarget) (self : ActivePackageTarget) : Array FileTarget := + self.oFileTargets ++ self.package.moreLibTargets ++ depTargets.concatMap (·.staticLibTargets) protected def ActivePackageTarget.binTarget -(depTargets : List ActivePackageTarget) (self : ActivePackageTarget) : FileTarget := +(depTargets : Array ActivePackageTarget) (self : ActivePackageTarget) : FileTarget := let linkTargets := self.linkTargets depTargets binTarget self.package.binFile linkTargets self.package.linkArgs "leanc" diff --git a/Lake/BuildMonad.lean b/Lake/BuildMonad.lean index 7c4226226a..064d2ef0fd 100644 --- a/Lake/BuildMonad.lean +++ b/Lake/BuildMonad.lean @@ -81,8 +81,8 @@ def logError (msg : String) : BuildM PUnit := do def runIn (ctx : BuildContext) (self : BuildM α) : IO α := self ctx -def run (self : BuildM α) : IO PUnit := - runIn BuildContext.io do try discard self catch e => +def run' (self : BuildM α) : IO α := + runIn BuildContext.io do try self catch e => /- Remark: Actual error should have already been logged earlier. However, if the error was thrown by something that did not know it was @@ -93,6 +93,9 @@ def run (self : BuildM α) : IO PUnit := BuildM.logError s!"build error: {toString e}" throw <| IO.userError "build failed" +def run (self : BuildM α) : IO PUnit := + discard self.run' + end BuildM def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α diff --git a/Lake/BuildPackage.lean b/Lake/BuildPackage.lean index b351adbc67..fc0d043d0f 100644 --- a/Lake/BuildPackage.lean +++ b/Lake/BuildPackage.lean @@ -32,6 +32,10 @@ def moduleTargets (self : ActivePackageTarget) : Array (Name × ActiveOleanAndCT end ActivePackageTarget +/-- Returns the `oleanDir`s of the given package targets in reverse order. -/ +def packageTargetsToOleanDirs (targets : Array ActivePackageTarget) : List FilePath := + targets.map (·.package.oleanDir) |>.foldl (flip List.cons) [] + -- # Build Modules def Package.buildModuleOleanAndCTargetDAG @@ -87,22 +91,22 @@ def Package.buildOleanTargets -- # Configure/Build Packages def Package.buildDepTargetWith -(depTargets : List ActivePackageTarget) (self : Package) : BuildM ActiveOpaqueTarget := do +(depTargets : Array ActivePackageTarget) (self : Package) : BuildM ActiveOpaqueTarget := do let extraDepTarget ← self.extraDepTarget.run - let depTarget ← ActiveTarget.collectOpaqueList depTargets + let depTarget ← ActiveTarget.collectOpaqueArray depTargets extraDepTarget.mixOpaqueAsync depTarget def Package.buildModuleOleanAndCTargetsWithDepTargets -(mods : Array Name) (depTargets : List ActivePackageTarget) (self : Package) +(mods : Array Name) (depTargets : Array ActivePackageTarget) (self : Package) : BuildM ActivePackageTarget := do let depTarget ← self.buildDepTargetWith depTargets - let moreOleanDirs := depTargets.map (·.package.oleanDir) + let moreOleanDirs := packageTargetsToOleanDirs depTargets let (targets, targetMap) ← self.buildModuleOleanAndCTargetDAG mods moreOleanDirs depTarget let target ← ActiveTarget.collectOpaqueArray targets return target.withInfo ⟨self, targetMap⟩ def Package.buildOleanAndCTargetsWithDepTargets -(depTargets : List ActivePackageTarget) (self : Package) : BuildM ActivePackageTarget := do +(depTargets : Array ActivePackageTarget) (self : Package) : BuildM ActivePackageTarget := do self.buildModuleOleanAndCTargetsWithDepTargets (← self.getModuleArray) depTargets /-- @@ -111,28 +115,35 @@ def Package.buildOleanAndCTargetsWithDepTargets It resolves the package's dependencies and recursively builds them. For each package, it compiles its modules into `.olean` and `.c` files. -/ -def recBuildPkgWithDeps [Monad m] [MonadLiftT BuildM m] -: RecBuild Package ActivePackageTarget m := fun pkg buildPkg => do - -- TODO: merge dependency resolution into build - let deps ← liftM (m := BuildM) <| solveDeps pkg - pkg.buildOleanAndCTargetsWithDepTargets (← deps.mapM buildPkg) +def recBuildPackageWithDeps +[Monad m] [MonadLiftT BuildM m] [MonadStore Name (Array ActivePackageTarget) m] +: RecBuild Package (Array ActivePackageTarget) m := fun pkg buildPkg => do + let mut depTargets := #[] + for dep in pkg.dependencies do + let targets? ← fetch? dep.name.toName + let targets ← do + if let some targets := targets? then + pure targets + else + let depPkg ← liftM (m := BuildM) <| resolveDep pkg dep + buildPkg depPkg + depTargets := depTargets ++ targets + let pkgTarget ← pkg.buildOleanAndCTargetsWithDepTargets depTargets + depTargets.push pkgTarget -def buildPackageTargetList (pkgs : List Package) : BuildM (List ActivePackageTarget) := do - failOnBuildCycle <| ← RBTopT.run' <| pkgs.mapM fun pkg => - buildRBTop (cmp := Name.quickCmp) recBuildPkgWithDeps (·.name.toName) pkg +def buildPackageTargetsWithDeps (pkgs : Array Package) : BuildM (Array ActivePackageTarget) := do + failOnBuildCycle <| ← RBTopT.run' <| pkgs.concatMapM fun pkg => + buildRBTop (cmp := Name.quickCmp) recBuildPackageWithDeps (·.name.toName) pkg def Package.buildTarget (self : Package) : BuildM ActivePackageTarget := do - failOnBuildCycle <| ← RBTopT.run' <| - buildRBTop (cmp := Name.quickCmp) recBuildPkgWithDeps (·.name.toName) self + (← buildPackageTargetsWithDeps #[self]).back -def Package.buildDepTargets (self : Package) : BuildM (List ActivePackageTarget) := do - buildPackageTargetList (← solveDeps self) +def Package.buildDepTargets (self : Package) : BuildM (Array ActivePackageTarget) := do + buildPackageTargetsWithDeps (← self.resolveDirectDeps).toArray -def Package.buildDeps (self : Package) : BuildM (List Package) := do - let deps ← solveDeps self - let targets ← buildPackageTargetList deps - targets.forM (discard ·.materialize) - return deps +def Package.buildDeps (self : Package) : BuildM (Array Package) := do + let targets ← self.buildDepTargets + targets.mapM fun target => Functor.mapConst target.info.1 target.materialize def configure (pkg : Package) : IO Unit := pkg.buildDeps.run @@ -140,7 +151,7 @@ def configure (pkg : Package) : IO Unit := def Package.build (self : Package) : BuildM PUnit := do let depTargets ← self.buildDepTargets let depTarget ← self.buildDepTargetWith depTargets - let moreOleanDirs := depTargets.map (·.package.oleanDir) + let moreOleanDirs := packageTargetsToOleanDirs depTargets let targets ← self.buildOleanTargets moreOleanDirs depTarget discard <| ActiveTarget.materializeArray targets @@ -149,22 +160,27 @@ def build (pkg : Package) : IO PUnit := -- # Print Paths -def Package.buildModuleOleanTargetsWithDeps -(deps : List Package) (mods : Array Name) (self : Package) -: BuildM (Array ActiveFileTarget) := do - let moreOleanDirs := deps.map (·.oleanDir) - let depTarget ← self.buildDepTargetWith <| ← buildPackageTargetList deps - self.buildModuleOleanTargets mods moreOleanDirs depTarget - -def Package.buildModuleOleansWithDeps -(deps : List Package) (mods : Array Name) (self : Package) := - self.buildModuleOleanTargetsWithDeps deps mods >>= (·.forM (discard ·.materialize)) +/-- Pick the local imports of the package from a list of import strings. -/ +def Package.filterLocalImports (imports : List String) (self : Package) : Array Name := do + let mut localImports := #[] + for imp in imports do + let impName := imp.toName + if self.isLocalModule impName then + localImports := localImports.push impName + return localImports 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 pkg.isLocalModule |>.toArray - pkg.buildModuleOleansWithDeps deps localImports |>.run + let deps ← BuildM.run' do + -- resolve and build deps + let depTargets ← pkg.buildDepTargets + let depPkgs := depTargets.map (·.package) |>.foldl (flip List.cons) [] + -- build any additional imports + unless imports.isEmpty do + let moreOleanDirs := depPkgs.map (·.oleanDir) + let depTarget ← pkg.buildDepTargetWith depTargets + let localImports := pkg.filterLocalImports imports + let oleanTargets ← pkg.buildModuleOleanTargets localImports moreOleanDirs depTarget + oleanTargets.forM (discard ·.materialize) + pure depPkgs IO.println <| SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir) IO.println <| SearchPath.toString <| pkg.srcDir :: deps.map (·.srcDir) diff --git a/Lake/BuildTop.lean b/Lake/BuildTop.lean index 0520e0c25e..5d5e02c5e8 100644 --- a/Lake/BuildTop.lean +++ b/Lake/BuildTop.lean @@ -19,7 +19,7 @@ def RecBuild.{u,v,w} (i : Type u) (o : Type v) (m : Type v → Type w) := i → (i → m o) → m o /-- A monad equipped with a key-object store. -/ -class MonadStore (k : Type u) (o : Type v) (m : Type v → Type w) where +class MonadStore (k : Type u) (o : outParam $ Type v) (m : Type v → Type w) where fetch? : k → m (Option o) store : k → o → m PUnit diff --git a/Lake/Resolve.lean b/Lake/Resolve.lean index 6e6bc5169c..50378b245e 100644 --- a/Lake/Resolve.lean +++ b/Lake/Resolve.lean @@ -11,8 +11,12 @@ open System namespace Lake open Git in -def materializeGit - (name : String) (dir : FilePath) (url rev : String) (branch : Option String) +/-- + Materializes a Git dependency in the given `dir`, + cloning and/or updating it as necessary. +-/ +def materializeGitDep +(name : String) (dir : FilePath) (url rev : String) (branch : Option String) : IO Unit := do if ← dir.isDir then IO.eprint s!"{name}: trying to update {dir} to revision {rev}" @@ -26,63 +30,36 @@ def materializeGit let hash ← parseOriginRevision rev dir checkoutDetach hash dir -def materialize (pkg : Package) (dep : Dependency) : IO FilePath := +/-- + Materializes a dependency relative to the given package, + downloading and/or updating it as necessary. +-/ +def materializeDep (pkg : Package) (dep : Dependency) : IO FilePath := match dep.src with | Source.path dir => do let depDir := pkg.dir / dir depDir | Source.git url rev branch => do let depDir := pkg.depsDir / dep.name - materializeGit dep.name depDir url rev branch + materializeGitDep dep.name depDir url rev branch depDir -def Assignment := List (String × Package) - -namespace Assignment - -def empty : Assignment := [] - -def contains (a : Assignment) (s : String) : Bool := - (a.lookup s).isSome - -def insert (a : Assignment) (k : String) (v : Package) : Assignment := - if a.contains k then a else (k, v) :: a - -def fold {α} (i : α) (f : α → String → Package → α) : Assignment → α := - List.foldl (fun a ⟨k, v⟩ => f a k v) i - -end Assignment - -abbrev Solver := StateT Assignment IO - -def notYetAssigned (d : String) : Solver Bool := do - ¬ (← get).contains d - -def resolvedPackage (d : String) : Solver Package := do - let some pkg ← pure ((← get).lookup d) | unreachable! - pkg - -def solveDepsCore (pkg : Package) : (maxDepth : Nat) → Solver Unit - | 0 => throw <| IO.userError "maximum dependency resolution depth reached" - | maxDepth + 1 => do - let newDeps ← pkg.dependencies.filterM (notYetAssigned ·.name) - for dep in newDeps do - let dir ← materialize pkg dep - let pkg ← Package.fromDir (dir / dep.dir) dep.args - modify (·.insert dep.name pkg) - for dep in newDeps do - let depPkg ← resolvedPackage dep.name - unless depPkg.name = dep.name do - throw <| IO.userError <| - s!"{pkg.name} (in {pkg.dir}) depends on {dep.name}, " ++ - s!"but resolved dependency has name {depPkg.name} (in {depPkg.dir})" - solveDepsCore depPkg maxDepth +/-- + Resolves a dependency relative to the given package, + downloading and/or updating it as necessary. +-/ +def resolveDep (pkg : Package) (dep : Dependency) : IO Package := do + let dir ← materializeDep pkg dep + let depPkg ← Package.fromDir (dir / dep.dir) dep.args + unless depPkg.name = dep.name do + throw <| IO.userError <| + s!"{pkg.name} (in {pkg.dir}) depends on {dep.name}, " ++ + s!"but resolved dependency has name {depPkg.name} (in {depPkg.dir})" + return depPkg /-- - Resolves the dependency tree for the given package, - downloading and/or updating missing dependencies as necessary. + Resolves the package's direct dependencies, + downloading and/or updating them as necessary. -/ -def solveDeps (pkg : Package) : IO (List Package) := do - let solver := solveDepsCore pkg 1024 - let (_, assg) ← solver.run <| Assignment.empty.insert pkg.name pkg - assg.reverse.tail!.mapM (·.2) +def Package.resolveDirectDeps (self : Package) : IO (List Package) := + self.dependencies.mapM (resolveDep self ·)