diff --git a/Leanpkg2/Build.lean b/Leanpkg2/Build.lean index 02a52b65f1..acabad4092 100644 --- a/Leanpkg2/Build.lean +++ b/Leanpkg2/Build.lean @@ -26,8 +26,8 @@ def mkBuildConfig : BuildConfig := { leanArgs, module := pkg.module - leanPath := SearchPath.toString <| deps.map (·.buildDir) - moreDeps := deps.filter (·.dir != pkg.dir) |>.map (·.oleanRoot) + leanPath := SearchPath.toString <| pkg.buildDir :: deps.map (·.buildDir) + moreDeps := deps.map (·.oleanRoot) } structure BuildContext extends BuildConfig where @@ -127,11 +127,10 @@ def buildPkg (pkg : Package) (deps : List Package) (makeArgs leanArgs : List Str def buildDeps (pkg : Package) (makeArgs leanArgs : List String := []) : IO (List Package) := do let deps ← solveDeps pkg for dep in deps do - unless dep.dir == pkg.dir do - -- build recursively - -- TODO: share build of common dependencies - let depDeps ← solveDeps dep - buildPkg dep depDeps makeArgs leanArgs + -- build recursively + -- TODO: share build of common dependencies + let depDeps ← solveDeps dep + buildPkg dep depDeps makeArgs leanArgs return deps def configure (pkg : Package) : IO Unit := @@ -140,8 +139,8 @@ def configure (pkg : Package) : IO Unit := def printPaths (pkg : Package) (imports leanArgs : List String := []) : IO Unit := do let deps ← buildDeps pkg buildImports pkg deps imports leanArgs - IO.println <| SearchPath.toString <| deps.map (·.buildDir) - IO.println <| SearchPath.toString <| deps.map (·.sourceDir) + IO.println <| SearchPath.toString <| pkg.buildDir :: deps.map (·.buildDir) + IO.println <| SearchPath.toString <| pkg.sourceDir :: deps.map (·.sourceDir) def build (pkg : Package) (makeArgs leanArgs : List String := []) : IO Unit := do let deps ← buildDeps pkg (if makeArgs.contains "bin" then ["lib"] else []) diff --git a/Leanpkg2/Make.lean b/Leanpkg2/Make.lean index 55f164fc4e..5c23dc7f44 100644 --- a/Leanpkg2/Make.lean +++ b/Leanpkg2/Make.lean @@ -48,10 +48,9 @@ def execMake | none => [] let leanmake := (← IO.appDir) / "leanmake" let leanOptsStr := " ".intercalate <| timeoutArgs ++ leanArgs - let leanPathStr := SearchPath.toString <| deps.map (·.buildDir) + let leanPathStr := SearchPath.toString <| pkg.buildDir :: deps.map (·.buildDir) let makeArgsStr := " ".intercalate makeArgs - let moreDepsStr := " ".intercalate $ - deps.filter (·.dir.toString != pkg.dir) |>.map (·.oleanRoot.toString) + let moreDepsStr := " ".intercalate <| deps.map (·.oleanRoot.toString) let mut spawnArgs := { cmd := "sh" cwd := pkg.dir diff --git a/Leanpkg2/Resolve.lean b/Leanpkg2/Resolve.lean index 9dce9f2c15..ad809679ca 100644 --- a/Leanpkg2/Resolve.lean +++ b/Leanpkg2/Resolve.lean @@ -82,10 +82,8 @@ def solveDepsCore (pkg : Package) : (maxDepth : Nat) → Solver Unit /-- Resolves the dependency tree for the given package, downloading and/or updating missing dependencies as necessary. - - Note that resulting list of dependencies *will* include the given package. -/ def solveDeps (pkg : Package) : IO (List Package) := do let solver := solveDepsCore pkg 1024 let (_, assg) ← solver.run (Assignment.empty.insert pkg.name ⟨pkg.dir, pkg.config⟩) - assg.reverse.mapM (·.2) + assg.reverse.tail!.mapM (·.2)