Skip to content

Commit 99c0d27

Browse files
committed
chore: fix tests
1 parent 8d734cb commit 99c0d27

File tree

4 files changed

+8
-10
lines changed

4 files changed

+8
-10
lines changed

src/lake/Lake/Build/Package.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ open Lean (Name)
2828
/-- Fetch the package's direct dependencies. -/
2929
private def Package.recFetchDeps (self : Package) : FetchM (Job (Array Package)) := ensureJob do
3030
(pure ·) <$> self.depConfigs.mapM fun cfg => do
31-
let some dep ← findPackageByKey? cfg.name
31+
let some dep ← findPackageByName? cfg.name
3232
| error s!"{self.prettyName}: package not found for dependency '{cfg.name}' \
3333
(this is likely a bug in Lake)"
3434
return dep
@@ -40,7 +40,7 @@ public def Package.depsFacetConfig : PackageFacetConfig depsFacet :=
4040
/-- Compute a topological ordering of the package's transitive dependencies. -/
4141
private def Package.recComputeTransDeps (self : Package) : FetchM (Job (Array Package)) := ensureJob do
4242
(pure ·.toArray) <$> self.depConfigs.foldlM (init := OrdPackageSet.empty) fun deps cfg => do
43-
let some dep ← findPackageByKey? cfg.name
43+
let some dep ← findPackageByName? cfg.name
4444
| error s!"{self.prettyName}: package not found for dependency '{cfg.name}' \
4545
(this is likely a bug in Lake)"
4646
let depDeps ← (← fetch <| dep.transDeps).await

src/lake/Lake/Load/Resolve.lean

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -71,8 +71,7 @@ abbrev DepStackT m := CallStackT Name m
7171

7272
@[inline] nonrec def DepStackT.run
7373
(x : DepStackT m α) (stack : DepStack := {})
74-
: m α :=
75-
x.run stack
74+
: m α := x.run stack
7675

7776
/-- Log dependency cycle and error. -/
7877
@[specialize] def depCycleError [MonadError m] (cycle : Cycle Name) : m α :=
@@ -86,8 +85,7 @@ abbrev ResolveT m := DepStackT <| StateT Workspace m
8685

8786
@[inline] nonrec def ResolveT.run
8887
(ws : Workspace) (x : ResolveT m α) (stack : DepStack := {})
89-
: m (α × Workspace) :=
90-
x.run stack |>.run ws
88+
: m (α × Workspace) := x.run stack |>.run ws
9189

9290
/-- Recursively run a `ResolveT` monad starting from the workspace's root. -/
9391
@[specialize] private def Workspace.runResolveT
@@ -102,7 +100,7 @@ abbrev ResolveT m := DepStackT <| StateT Workspace m
102100
/-
103101
Recursively visits each node in a package's dependency graph, starting from
104102
the workspace package `root`. Each dependency missing from the workspace is
105-
resolved using the `resolve` function and added into the workspace.
103+
resolved using the `load` function and added into the workspace.
106104
107105
Recursion occurs breadth-first. Each direct dependency of a package is
108106
resolved in reverse order before recursing to the dependencies' dependencies.
@@ -121,7 +119,7 @@ where
121119
-- Materialize and load the missing direct dependencies of `pkg`
122120
pkg.depConfigs.forRevM fun dep => do
123121
let ws ← getWorkspace
124-
if ws.packageMap.contains dep.name then
122+
if ws.packages.any (·.baseName == dep.name) then
125123
return -- already handled in another branch
126124
if pkg.baseName = dep.name then
127125
error s!"{pkg.prettyName}: package requires itself (or a package with the same name)"

tests/lake/examples/targets/lakefile.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ target bark_bark : Unit := do
3939
bark.fetch
4040

4141
package_facet print_name pkg : Unit := Job.async do
42-
IO.println pkg.name
42+
IO.println pkg.prettyName
4343

4444
module_facet get_src mod : System.FilePath := do
4545
inputTextFile mod.leanFile

tests/lake/tests/depRenaming/dep/lakefile.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,4 @@ open System Lake DSL
44
package dep
55

66
target name : String := Job.sync do
7-
return (__name__).toString
7+
return (__name__).getPrefix.toString

0 commit comments

Comments
 (0)