Skip to content

Commit 3200264

Browse files
committed
fix: Target.Fetch & alias Package.name as baseName
1 parent 7f7915f commit 3200264

File tree

2 files changed

+16
-11
lines changed

2 files changed

+16
-11
lines changed

src/lake/Lake/Build/Target/Fetch.lean

Lines changed: 14 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -27,15 +27,15 @@ private def PartialBuildKey.fetchInCoreAux
2727
return ⟨.module modName, cast (by simp) <| Job.pure mod⟩
2828
| .package pkgName =>
2929
let pkg ← resolveTargetPackageD pkgName
30-
return ⟨.package pkg.name, cast (by simp) <| Job.pure pkg⟩
30+
return ⟨.package pkg.keyName, cast (by simp) <| Job.pure pkg⟩
3131
| .packageModule pkgName modName =>
3232
let pkg ← resolveTargetPackageD pkgName
3333
let some mod := pkg.findTargetModule? modName
34-
| error s!"invalid target '{root}': module target '{modName}' not found in package '{pkg.name}'"
35-
return ⟨.packageModule pkg.name modName, cast (by simp) <| Job.pure mod⟩
34+
| error s!"invalid target '{root}': module target '{modName}' not found in package '{pkg.prettyName}'"
35+
return ⟨.packageModule pkg.keyName modName, cast (by simp) <| Job.pure mod⟩
3636
| .packageTarget pkgName target =>
3737
let pkg ← resolveTargetPackageD pkgName
38-
let key := BuildKey.packageTarget pkg.name target
38+
let key := BuildKey.packageTarget pkg.keyName target
3939
if facetless then
4040
if let some decl := pkg.findTargetDecl? target then
4141
if h : decl.kind.isAnonymous then
@@ -48,7 +48,7 @@ private def PartialBuildKey.fetchInCoreAux
4848
let info := BuildInfo.facet key decl.kind tgt facet
4949
return ⟨key.facet facet, ← info.fetch⟩
5050
else
51-
error s!"invalid target '{root}': target not found in package '{pkg.name}'"
51+
error s!"invalid target '{root}': target not found in package '{pkg.prettyName}'"
5252
else
5353
let job ← (pkg.target target).fetch
5454
return ⟨key, cast (by simp) job⟩
@@ -67,10 +67,15 @@ private def PartialBuildKey.fetchInCoreAux
6767
return ⟨.facet target facet, cast (by simp) job⟩
6868
where
6969
@[inline] resolveTargetPackageD (name : Name) : FetchM Package := do
70-
if name.isAnonymous then
71-
pure defaultPkg
72-
else
73-
let some pkg ← findPackage? name
70+
match name with
71+
| .anonymous =>
72+
return defaultPkg
73+
| p@(.num ..) =>
74+
let some pkg ← findPackageByKey? p
75+
| error s!"invalid target '{root}': package '{name}' not found in workspace"
76+
return pkg
77+
| p =>
78+
let some pkg ← findPackageByName? p
7479
| error s!"invalid target '{root}': package '{name}' not found in workspace"
7580
return pkg
7681

src/lake/Lake/Config/Package.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -101,8 +101,8 @@ public instance : BEq Package where beq p1 p2 := p1.wsIdx == p2.wsIdx
101101
public instance : QueryJson Package := ⟨(toJson ·.keyName)⟩
102102
public instance : QueryText Package := ⟨(·.prettyName)⟩
103103

104-
@[deprecated "Use `keyName` or `prettyName` instead" (since := "2025-12-03")]
105-
public abbrev name := @keyName
104+
@[deprecated "Use `baseName`, `keyName`, or `prettyName` instead" (since := "2025-12-03")]
105+
public abbrev name := @baseName
106106

107107
/-- The (unscoped) name of the package as it appears in Reservoir URLs (before URI-encoding). -/
108108
@[inline] public def reservoirName (self : Package) : String :=

0 commit comments

Comments
 (0)