diff --git a/Leanpkg2/Build.lean b/Leanpkg2/Build.lean
index 0a1bdaa5cc..c6a4be4d76 100644
--- a/Leanpkg2/Build.lean
+++ b/Leanpkg2/Build.lean
@@ -7,7 +7,6 @@ import Lean.Data.Name
 import Lean.Elab.Import
 import Leanpkg2.Resolve
 import Leanpkg2.Package
-import Leanpkg2.BuildConfig
 import Leanpkg2.Make
 import Leanpkg2.Proc
 
@@ -15,6 +14,22 @@ open Lean System
 
 namespace Leanpkg2
 
+structure BuildConfig where
+  module   : Name
+  leanArgs : List String
+  leanPath : String
+  -- things like `leanpkg.toml` and olean roots of dependencies that should also trigger rebuilds
+  moreDeps : List FilePath
+
+def mkBuildConfig
+(pkg : Package) (deps : List Package) (leanArgs : List String)
+: BuildConfig := {
+  leanArgs,
+  module := pkg.module
+  leanPath := SearchPath.toString <| deps.map (·.buildDir)
+  moreDeps := deps.filter (·.dir != pkg.dir) |>.map (·.oleanRoot)
+}
+
 structure BuildContext extends BuildConfig where
   parents       : List Name := []
   moreDepsMTime : IO.FS.SystemTime
@@ -84,7 +99,7 @@ partial def buildModule (mod : Name) : BuildM Result := do
   modify fun st => { st with modTasks := st.modTasks.insert mod r }
   return r
 
-def buildModules (manifest : Manifest) (cfg : BuildConfig) (mods : List Name) : IO Unit := do
+def buildModules (cfg : BuildConfig) (mods : List Name) : IO Unit := do
   let moreDepsMTime := (← cfg.moreDeps.mapM (·.metadata)).map (·.modified) |>.maximum? |>.getD ⟨0, 0⟩
   let rs ← mods.mapM buildModule |>.run { toBuildConfig := cfg, moreDepsMTime } |>.run' {}
   for r in rs do
@@ -92,44 +107,42 @@ def buildModules (manifest : Manifest) (cfg : BuildConfig) (mods : List Name) :
       -- actual error has already been printed above
       throw <| IO.userError "Build failed."
 
-def buildImports (manifest : Manifest) (cfg : BuildConfig) (imports leanArgs : List String := []) : IO Unit := do
+def buildImports (pkg : Package) (deps : List Package) (imports leanArgs : List String := []) : IO Unit := do
   let imports := imports.map (·.toName)
-  let localImports := imports.filter (·.getRoot == cfg.module)
+  let localImports := imports.filter (·.getRoot == pkg.module)
   if localImports != [] then
     if ← FilePath.pathExists "Makefile" then
       let oleans := localImports.map fun i =>
         Lean.modToFilePath buildPath i "olean" |>.toString
-      execMake manifest oleans cfg
+      execMake pkg deps oleans leanArgs
     else
-      buildModules manifest cfg localImports
+      buildModules (mkBuildConfig pkg deps leanArgs) localImports
 
-def buildDeps (manifest : Manifest) : IO (List Package) := do
-  let pkgs ← solveDeps manifest
-  for pkg in pkgs do
-    unless pkg.dir.toString == "." do
+def buildDeps (pkg : Package) : 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
       execCmd {
-        cwd := pkg.dir
+        cwd := dep.dir
         cmd := (← IO.appDir) / "lean" |>.toString
         args := #["--run", "Package.lean"]
       }
-  return pkgs
+  return deps
 
-def configure (manifest : Manifest) : IO Unit := do
-  discard <| buildDeps manifest
+def configure (pkg : Package) : IO Unit := do
+  discard <| buildDeps pkg
 
-def printPaths (manifest : Manifest) (imports leanArgs : List String := []) : IO Unit := do
-  let pkgs ← buildDeps manifest
-  let cfg := BuildConfig.fromPackages manifest.module leanArgs pkgs
-  buildImports manifest cfg imports leanArgs
-  IO.println cfg.leanPath
-  IO.println <| SearchPath.toString <| pkgs.map (·.sourceDir)
+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)
 
-def build (manifest : Manifest) (makeArgs leanArgs : List String := []) : IO Unit := do
-  let pkgs ← buildDeps manifest
-  let cfg := BuildConfig.fromPackages manifest.module leanArgs pkgs
+def build (pkg : Package) (makeArgs leanArgs : List String := []) : IO Unit := do
+  let deps ← buildDeps pkg
   if makeArgs != [] || (← FilePath.pathExists "Makefile") then
-    execMake manifest makeArgs cfg
+    execMake pkg deps makeArgs leanArgs
   else
-    buildModules manifest cfg [manifest.module]
+    buildModules (mkBuildConfig pkg deps leanArgs) [pkg.module]
diff --git a/Leanpkg2/BuildConfig.lean b/Leanpkg2/BuildConfig.lean
deleted file mode 100644
index 009ec6b06f..0000000000
--- a/Leanpkg2/BuildConfig.lean
+++ /dev/null
@@ -1,31 +0,0 @@
-/-
-Copyright (c) 2021 Sebastian Ullrich. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich, Mac Malone
--/
-import Lean.Data.Name
-import Lean.Elab.Import
-import Leanpkg2.Package
-import Leanpkg2.Proc
-
-open Lean System
-
-namespace Leanpkg2
-
-structure BuildConfig where
-  module   : Name
-  leanArgs : List String
-  leanPath : String
-  -- things like `leanpkg.toml` and olean roots of dependencies that should also trigger rebuilds
-  moreDeps : List FilePath
-
-namespace BuildConfig
-
-def fromPackages
-(module : Name) (leanArgs : List String) (pkgs : List Package)
-: BuildConfig := {
-  module, leanArgs,
-  leanPath := SearchPath.toString <| pkgs.map (·.buildDir)
-  moreDeps := pkgs.filter (·.dir.toString != ".") |>.map
-    (·.buildRoot.withExtension "olean")
-}
diff --git a/Leanpkg2/Cli.lean b/Leanpkg2/Cli.lean
index e94674e429..9ab76db53e 100644
--- a/Leanpkg2/Cli.lean
+++ b/Leanpkg2/Cli.lean
@@ -5,7 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Leanpkg2.Init
 import Leanpkg2.Build
-import Leanpkg2.TomlManifest
+import Leanpkg2.TomlConfig
 
 namespace Leanpkg2
 
@@ -61,11 +61,18 @@ Usage:
 This command creates a new Lean package with the given name in the current
 directory."
 
+def getRootPkg : IO Package := do
+  let cfg ← PackageConfig.fromTomlFile leanpkgToml
+  if cfg.leanVersion ≠ leanVersionString then
+    IO.eprintln $ "\nWARNING: Lean version mismatch: installed version is " ++
+      leanVersionString ++ ", but package requires " ++ cfg.leanVersion ++ "\n"
+  return ⟨".", cfg⟩
+
 def cli : (cmd : String) → (leanpkgArgs leanArgs : List String) → IO Unit
 | "init",         [name],         []        => init name
-| "configure",    [],             []        => do configure (← readManifest)
-| "print-paths",  imports,        leanArgs  => do printPaths (← readManifest) imports leanArgs
-| "build",        makeArgs,       leanArgs  => do build (← readManifest) makeArgs leanArgs
+| "configure",    [],             []        => do configure (← getRootPkg)
+| "print-paths",  imports,        leanArgs  => do printPaths (← getRootPkg) imports leanArgs
+| "build",        makeArgs,       leanArgs  => do build (← getRootPkg) makeArgs leanArgs
 | "help",         ["init"],       []        => IO.println helpInit
 | "help",         ["configure"],  []        => IO.println helpConfigure
 | "help",         ["build"],      []        => IO.println helpBuild
diff --git a/Leanpkg2/Init.lean b/Leanpkg2/Init.lean
index 97026ba820..b08495b872 100644
--- a/Leanpkg2/Init.lean
+++ b/Leanpkg2/Init.lean
@@ -5,7 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Leanpkg2.Git
 import Leanpkg2.Proc
-import Leanpkg2.TomlManifest
+import Leanpkg2.TomlConfig
 
 namespace Leanpkg2
 
diff --git a/Leanpkg2/Make.lean b/Leanpkg2/Make.lean
index 8a61c24d4e..55f164fc4e 100644
--- a/Leanpkg2/Make.lean
+++ b/Leanpkg2/Make.lean
@@ -3,50 +3,58 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
+import Leanpkg2.Proc
 import Leanpkg2.Package
-import Leanpkg2.BuildConfig
 
 open System
 
 namespace Leanpkg2
 
-def lockFileName : FilePath := ".leanpkg-lock"
+def lockfile : FilePath := ".leanpkg-lock"
 
 partial def withLockFile (x : IO α) : IO α := do
   acquire
   try
     x
   finally
-    IO.removeFile lockFileName
+    IO.removeFile lockfile
   where
     acquire (firstTime := true) :=
       try
         -- TODO: lock file should ideally contain PID
         if !Platform.isWindows then
-          discard <| IO.Prim.Handle.mk lockFileName "wx"
+          discard <| IO.Prim.Handle.mk lockfile "wx"
         else
           -- `x` mode doesn't seem to work on Windows even though it's listed at
           -- https://docs.microsoft.com/en-us/cpp/c-runtime-library/reference/fopen-wfopen?view=msvc-160
           -- ...? Let's use the slightly racy approach then.
-          if ← lockFileName.pathExists then
+          if ← lockfile.pathExists then
             throw <| IO.Error.alreadyExists 0 ""
-          discard <| IO.Prim.Handle.mk lockFileName "w"
+          discard <| IO.Prim.Handle.mk lockfile "w"
       catch
         | IO.Error.alreadyExists _ _ => do
           if firstTime then
-            IO.eprintln s!"Waiting for prior leanpkg invocation to finish... (remove '{lockFileName}' if stuck)"
+            IO.eprintln s!"Waiting for prior leanpkg invocation to finish... (remove '{lockfile}' if stuck)"
           IO.sleep (ms := 300)
           acquire (firstTime := false)
         | e => throw e
 
-def execMake (manifest : Manifest) (makeArgs : List String) (cfg : BuildConfig) : IO Unit := withLockFile do
+def execMake
+(pkg : Package) (deps : List Package) (makeArgs leanArgs : List String := [])
+: IO Unit := withLockFile do
   let timeoutArgs :=
-    match manifest.timeout with
+    match pkg.timeout with
     | some t => ["-T", toString t]
     | none => []
-  let leanArgs := timeoutArgs ++ cfg.leanArgs
+  let leanmake := (← IO.appDir) / "leanmake"
+  let leanOptsStr := " ".intercalate <| timeoutArgs ++ leanArgs
+  let leanPathStr := SearchPath.toString <| deps.map (·.buildDir)
+  let makeArgsStr := " ".intercalate makeArgs
+  let moreDepsStr := " ".intercalate $
+    deps.filter (·.dir.toString != pkg.dir) |>.map (·.oleanRoot.toString)
   let mut spawnArgs := {
     cmd := "sh"
-    args := #["-c", s!"\"{← IO.appDir}/leanmake\" PKG={cfg.module} LEAN_OPTS=\"{" ".intercalate leanArgs}\" LEAN_PATH=\"{cfg.leanPath}\" {" ".intercalate makeArgs} MORE_DEPS+=\"{" ".intercalate (cfg.moreDeps.map toString)}\" >&2"]
+    cwd := pkg.dir
+    args := #["-c", s!"\"{leanmake}\" PKG={pkg.module} LEAN_OPTS=\"{leanOptsStr}\" LEAN_PATH=\"{leanPathStr}\" {makeArgsStr} MORE_DEPS+=\"{moreDepsStr}\" >&2"]
   }
   execCmd spawnArgs
diff --git a/Leanpkg2/Package.lean b/Leanpkg2/Package.lean
index e5ffc41bc5..27c4111cd1 100644
--- a/Leanpkg2/Package.lean
+++ b/Leanpkg2/Package.lean
@@ -22,38 +22,47 @@ structure Dependency where
   name : String
   src : Source
 
-structure Manifest where
+structure PackageConfig where
   name : String
   version : String
   leanVersion : String := leanVersionString
   timeout : Option Nat := none
-  module : String := name.capitalize
+  module : Name := name.capitalize
   dependencies : List Dependency := []
   deriving Inhabited
 
 structure Package where
   dir : FilePath
-  manifest : Manifest
+  config : PackageConfig
   deriving Inhabited
 
 namespace Package
 
-def name (self : Package) : String :=
-  self.manifest.name
+def name (self : Package) :=
+  self.config.name
 
-def dependencies (self : Package) : List Dependency :=
-  self.manifest.dependencies
+def module (self : Package) :=
+  self.config.module
 
-def sourceDir (self : Package) : FilePath :=
+def dependencies (self : Package) :=
+  self.config.dependencies
+
+def timeout (self : Package) :=
+  self.config.timeout
+
+def sourceDir (self : Package) :=
   self.dir
 
-def sourceRoot (self : Package)  : FilePath :=
-  self.sourceDir / self.manifest.module
+def sourceRoot (self : Package) :=
+  self.sourceDir / self.config.module.toString
 
-def buildDir (self : Package) : FilePath :=
+def buildDir (self : Package) :=
   self.dir / Leanpkg2.buildPath
 
-def buildRoot (self : Package)  : FilePath :=
-  self.buildDir / self.manifest.module
+def buildRoot (self : Package) :=
+  self.buildDir / self.config.module.toString
+
+def oleanRoot (self : Package) :=
+  self.buildRoot.withExtension "olean"
 
 end Package
diff --git a/Leanpkg2/Resolve.lean b/Leanpkg2/Resolve.lean
index cd20d1d4aa..732def2140 100644
--- a/Leanpkg2/Resolve.lean
+++ b/Leanpkg2/Resolve.lean
@@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Leanpkg2.Git
-import Leanpkg2.Proc
-import Leanpkg2.TomlManifest
-import Leanpkg2.BuildConfig
+import Leanpkg2.TomlConfig
 
 open System
 
@@ -28,14 +26,14 @@ def materializeGit
     let hash ← parseOriginRevision rev dir
     checkoutDetach hash dir
 
-def materialize (relPath : FilePath) (dep : Dependency) : IO FilePath :=
+def materialize (pkgDir : FilePath) (dep : Dependency) : IO FilePath :=
   match dep.src with
   | Source.path dir => do
-    let depdir := relPath / dir
+    let depdir := pkgDir / dir
     IO.eprintln s!"{dep.name}: using local path {depdir}"
     depdir
   | Source.git url rev branch => do
-    let depdir := depsPath / dep.name
+    let depdir := pkgDir / depsPath / dep.name
     materializeGit dep.name depdir url rev branch
     depdir
 
@@ -65,23 +63,29 @@ def resolvedPackage (d : String) : Solver Package := do
   let some pkg ← pure ((← get).lookup d) | unreachable!
   pkg
 
-def solveDepsCore
-(pkgName : String) (relPath : FilePath) (deps : List Dependency)
-: (maxDepth : Nat) → Solver Unit
+def solveDepsCore (pkg : Package) : (maxDepth : Nat) → Solver Unit
   | 0 => throw <| IO.userError "maximum dependency resolution depth reached"
   | maxDepth + 1 => do
-    let newDeps ← deps.filterM (notYetAssigned ·.name)
+    let newDeps ← pkg.dependencies.filterM (notYetAssigned ·.name)
     for dep in newDeps do
-      let dir ← materialize relPath dep
-      let m ← Manifest.fromTomlFile <| dir / leanpkgToml
-      modify (·.insert dep.name ⟨dir, m⟩)
+      let dir ← materialize pkg.dir dep
+      let cfg ← PackageConfig.fromTomlFile <| dir / leanpkgToml
+      modify (·.insert dep.name ⟨dir, cfg⟩)
     for dep in newDeps do
       let depPkg ← resolvedPackage dep.name
       unless depPkg.name = dep.name do
-        throw <| IO.userError s!"{pkgName} (in {relPath}) depends on {depPkg.name}, but resolved dependency has name {dep.name} (in {depPkg.dir})"
-      solveDepsCore depPkg.name depPkg.dir depPkg.dependencies maxDepth
+        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
 
-def solveDeps (m : Manifest) : IO (List Package) := do
-  let solver := solveDepsCore m.name ⟨"."⟩ m.dependencies 1024
-  let (_, assg) ← solver.run (Assignment.empty.insert m.name ⟨".", m⟩)
+/--
+  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)
diff --git a/Leanpkg2/TomlManifest.lean b/Leanpkg2/TomlConfig.lean
similarity index 74%
rename from Leanpkg2/TomlManifest.lean
rename to Leanpkg2/TomlConfig.lean
index b37d893c25..fc82ff24e5 100644
--- a/Leanpkg2/TomlManifest.lean
+++ b/Leanpkg2/TomlConfig.lean
@@ -11,6 +11,8 @@ open System
 
 namespace Leanpkg2
 
+def leanpkgToml : FilePath := "leanpkg.toml"
+
 namespace Source
 
 def fromToml? (v : Toml.Value) : Option Source :=
@@ -32,9 +34,9 @@ def toToml : Source → Toml.Value
 
 end Source
 
-namespace Manifest
+namespace PackageConfig
 
-def fromToml? (t : Toml.Value) : Option Manifest := OptionM.run do
+def fromToml? (t : Toml.Value) : Option PackageConfig := OptionM.run do
   let pkg ← t.lookup "package"
   let Toml.Value.str name ← pkg.lookup "name" | none
   let Toml.Value.str version ← pkg.lookup "version" | none
@@ -54,24 +56,15 @@ def fromToml? (t : Toml.Value) : Option Manifest := OptionM.run do
   let dependencies ← deps.mapM fun ⟨n, src⟩ => do Dependency.mk n (← Source.fromToml? src)
   return { name, module, version, leanVersion, dependencies, timeout }
 
-def fromTomlString? (str : String) : IO (Option Manifest) := do
+def fromTomlString? (str : String) : IO (Option PackageConfig) := do
   fromToml? (← Toml.parse str)
 
-def fromTomlFile? (path : FilePath) : IO (Option Manifest) := do
+def fromTomlFile? (path : FilePath) : IO (Option PackageConfig) := do
   fromTomlString? (← IO.FS.readFile path)
 
-def fromTomlFile (path : FilePath) : IO Manifest := do
-  let some manifest ← fromTomlFile? path
-    | throw <| IO.userError s!"manifest (at {path}) is ill-formed"
-  manifest
+def fromTomlFile (path : FilePath) : IO PackageConfig := do
+  let some config ← fromTomlFile? path
+    | throw <| IO.userError s!"configuration (at {path}) is ill-formed"
+  config
 
-end Manifest
-
-def leanpkgToml : FilePath := "leanpkg.toml"
-
-def readManifest : IO Manifest := do
-  let m ← Manifest.fromTomlFile leanpkgToml
-  if m.leanVersion ≠ leanVersionString then
-    IO.eprintln $ "\nWARNING: Lean version mismatch: installed version is " ++ leanVersionString
-       ++ ", but package requires " ++ m.leanVersion ++ "\n"
-  return m
+end PackageConfig
diff --git a/examples/hello/Package.lean b/examples/hello/Package.lean
index 5de8e84f0b..382b9f89cc 100644
--- a/examples/hello/Package.lean
+++ b/examples/hello/Package.lean
@@ -2,16 +2,16 @@ import Leanpkg2.Build
 
 open Leanpkg2
 
-def manifest : Manifest := {
+def package : PackageConfig := {
   name := "hello",
   version := "1.0",
 }
 
 def configure : IO Unit :=
-  Leanpkg2.configure manifest
+  Leanpkg2.configure ⟨".", package⟩
 
 def build : IO Unit :=
-  Leanpkg2.build manifest ["bin"]
+  Leanpkg2.build ⟨".", package⟩ ["bin"]
 
 def main : IO Unit :=
   build
diff --git a/examples/hello/package.lean b/examples/hello/package.lean
index 5de8e84f0b..382b9f89cc 100644
--- a/examples/hello/package.lean
+++ b/examples/hello/package.lean
@@ -2,16 +2,16 @@ import Leanpkg2.Build
 
 open Leanpkg2
 
-def manifest : Manifest := {
+def package : PackageConfig := {
   name := "hello",
   version := "1.0",
 }
 
 def configure : IO Unit :=
-  Leanpkg2.configure manifest
+  Leanpkg2.configure ⟨".", package⟩
 
 def build : IO Unit :=
-  Leanpkg2.build manifest ["bin"]
+  Leanpkg2.build ⟨".", package⟩ ["bin"]
 
 def main : IO Unit :=
   build
diff --git a/examples/helloDeps/a/Package.lean b/examples/helloDeps/a/Package.lean
index 11d316b818..bc4a057c30 100644
--- a/examples/helloDeps/a/Package.lean
+++ b/examples/helloDeps/a/Package.lean
@@ -2,13 +2,13 @@ import Leanpkg2.Build
 
 open Leanpkg2
 
-def manifest : Manifest := {
+def package : PackageConfig := {
   name := "a",
   version := "1.0",
 }
 
 def build : IO Unit :=
-  Leanpkg2.build manifest ["lib"]
+  Leanpkg2.build ⟨".", package⟩ ["lib"]
 
 def main : IO Unit :=
   build
diff --git a/examples/helloDeps/a/package.lean b/examples/helloDeps/a/package.lean
index 11d316b818..bc4a057c30 100644
--- a/examples/helloDeps/a/package.lean
+++ b/examples/helloDeps/a/package.lean
@@ -2,13 +2,13 @@ import Leanpkg2.Build
 
 open Leanpkg2
 
-def manifest : Manifest := {
+def package : PackageConfig := {
   name := "a",
   version := "1.0",
 }
 
 def build : IO Unit :=
-  Leanpkg2.build manifest ["lib"]
+  Leanpkg2.build ⟨".", package⟩ ["lib"]
 
 def main : IO Unit :=
   build
diff --git a/examples/helloDeps/b/Package.lean b/examples/helloDeps/b/Package.lean
index b5e24b0fc5..8bc0d71a06 100644
--- a/examples/helloDeps/b/Package.lean
+++ b/examples/helloDeps/b/Package.lean
@@ -2,7 +2,7 @@ import Leanpkg2.Build
 
 open Leanpkg2 System
 
-def manifest : Manifest := {
+def package : PackageConfig := {
   name := "b",
   version := "1.0",
   dependencies := [
@@ -11,7 +11,7 @@ def manifest : Manifest := {
 }
 
 def build : IO Unit := do
-  Leanpkg2.build manifest ["bin", "LINK_OPTS=../a/build/lib/libA.a"]
+  Leanpkg2.build ⟨".", package⟩ ["bin", "LINK_OPTS=../a/build/lib/libA.a"]
 
 def main : IO Unit :=
   build
diff --git a/examples/helloDeps/b/package.lean b/examples/helloDeps/b/package.lean
index b5e24b0fc5..8bc0d71a06 100644
--- a/examples/helloDeps/b/package.lean
+++ b/examples/helloDeps/b/package.lean
@@ -2,7 +2,7 @@ import Leanpkg2.Build
 
 open Leanpkg2 System
 
-def manifest : Manifest := {
+def package : PackageConfig := {
   name := "b",
   version := "1.0",
   dependencies := [
@@ -11,7 +11,7 @@ def manifest : Manifest := {
 }
 
 def build : IO Unit := do
-  Leanpkg2.build manifest ["bin", "LINK_OPTS=../a/build/lib/libA.a"]
+  Leanpkg2.build ⟨".", package⟩ ["bin", "LINK_OPTS=../a/build/lib/libA.a"]
 
 def main : IO Unit :=
   build