@@ -19,39 +19,20 @@ open System Lean
1919namespace Lake
2020
2121/-- Load the tagged `Dependency` definitions from a package configuration environment. -/
22- def loadDeps (env : Environment) (opts : Options) : Except String (Array Dependency) := do
22+ def loadDepsFromEnv (env : Environment) (opts : Options) : Except String (Array Dependency) := do
2323 packageDepAttr.ext.getState env |>.foldM (init := #[]) fun arr name => do
2424 return arr.push <| ← evalConstCheck env opts Dependency ``Dependency name
2525
26- /-- Add entries from `pkg`'s manifest to this one. -/
27- def Manifest.appendPackageManifest (self : Manifest) (pkg : Package) : LogIO Manifest := do
28- let mut result := self
29- let pkgManifest ← Manifest.loadOrEmpty pkg.manifestFile
30- for pkgEntry in pkgManifest do
31- if let some entry := self.find? pkgEntry.name then
32- let shouldUpdate :=
33- match entry.inputRev?, pkgEntry.inputRev? with
34- | none, none => entry.rev != pkgEntry.rev
35- | none, some _ => false
36- | some _, none => false
37- | some rev, some dep => rev = dep ∧ entry.rev ≠ pkgEntry.rev
38- let contributors := entry.contributors.insert pkg.name pkgEntry.toPersistentPackageEntry
39- result := result.insert {entry with contributors, shouldUpdate}
40- else
41- let contributors := NameMap.empty.insert pkg.name pkgEntry.toPersistentPackageEntry
42- result := result.insert {pkgEntry with contributors}
43- return result
44-
4526/--
4627Resolve a single dependency and load the resulting package.
4728Resolution is based on the `Dependency` configuration and the package manifest.
4829-/
49- def resolveDep (ws : Workspace ) (pkg : Package) (dep : Dependency)
30+ def resolveDep (packagesDir : FilePath ) (pkg : Package) (dep : Dependency)
5031(topLevel : Bool) (shouldUpdate : Bool) : StateT Manifest LogIO Package := do
5132 let entry? := (← get).find? dep.name
5233 let entry? := entry?.map fun entry =>
5334 {entry with shouldUpdate := if topLevel then shouldUpdate else entry.shouldUpdate}
54- let ⟨dir, url?, tag?, entry?⟩ ← materializeDep ws. packagesDir pkg.dir dep entry?
35+ let ⟨dir, url?, tag?, entry?⟩ ← materializeDep packagesDir pkg.dir dep entry?
5536 let configEnv ← elabConfigFile dir dep.options pkg.leanOpts (dir / defaultConfigFile)
5637 let config ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv pkg.leanOpts
5738 let depPkg : Package := {
@@ -85,20 +66,20 @@ def resolveDep (ws : Workspace) (pkg : Package) (dep : Dependency)
8566Resolves the package's dependencies,
8667downloading and/or updating them as necessary.
8768-/
88- def resolveDeps (ws : Workspace) (pkg : Package) (shouldUpdate := true ) : LogIO Package := do
89- let manifest ← Manifest.loadOrEmpty pkg .manifestFile
90- let (pkg , manifest) ← StateT.run (s := manifest) do
69+ def Package. resolveDepsroot : Package) (shouldUpdate := true ) : LogIO Package := do
70+ let manifest ← Manifest.loadOrEmpty root .manifestFile
71+ let (root , manifest) ← StateT.run (s := manifest) do
9172 let res ← EStateT.run' (mkNameMap Package) do
92- buildAcyclic (·.name) pkg fun pkg resolve => do
93- let topLevel := pkg.name = ws. root.name
94- let deps ← IO.ofExcept <| loadDeps pkg.configEnv pkg.leanOpts
73+ buildAcyclic (·.name) root fun pkg resolve => do
74+ let topLevel := pkg.name = root.name
75+ let deps ← IO.ofExcept <| loadDepsFromEnv pkg.configEnv pkg.leanOpts
9576 let depPkgs ← deps.mapM fun dep => do
9677 fetchOrCreate dep.name do
97- liftM <| resolveDep ws pkg dep topLevel shouldUpdate
78+ liftM <| resolveDep root.packagesDir pkg dep topLevel shouldUpdate
9879 return {pkg with opaqueDeps := ← depPkgs.mapM (.mk <$> resolve ·)}
9980 match res with
100- | Except.ok pkg =>
101- return pkg
81+ | Except.ok root =>
82+ return root
10283 | Except.error cycle =>
10384 let cycle := cycle.map (s! " { ·} "
10485 error s! "dependency cycle detected:\n { "\n " .intercalate cycle} "
@@ -112,8 +93,8 @@ def resolveDeps (ws : Workspace) (pkg : Package) (shouldUpdate := true) : LogIO
11293 let inputRev := entry.inputRev?.getD Git.upstreamBranch
11394 log := log ++ s! "Using `{ inputRev} ` at `{ entry.rev} `"
11495 logInfo log
115- manifest.saveToFile ws .manifestFile
116- return pkg
96+ manifest.saveToFile root .manifestFile
97+ return root
11798
11899/--
119100Finalize the workspace's root and its transitive dependencies
@@ -160,5 +141,5 @@ def loadWorkspace (config : LoadConfig) : LogIO Workspace := do
160141 packageFacetConfigs := initPackageFacetConfigs
161142 libraryFacetConfigs := initLibraryFacetConfigs
162143 }
163- let root ← resolveDeps ws root config.updateDeps
144+ let root ← root.resolveDeps config.updateDeps
164145 {ws with root}.finalize
0 commit comments