Skip to content

Commit 183463c

Browse files
tydeutydeu
authored
refactor: lake: generalize targets (#7185)
This PR refactors Lake's build internals to enable the introduction of targets and facets beyond packages, modules, and libraries. Facets, build keys, build info, and CLI commands have been generalized to arbitrary target types.
1 parent 6916075 commit 183463c

40 files changed

+1195
-716
lines changed

‎src/lake/Lake/Build/Data.lean

+202-63
Original file line numberDiff line numberDiff line change
@@ -15,59 +15,134 @@ namespace Lake
1515
--------------------------------------------------------------------------------
1616

1717
/--
18-
The open type family which maps a module facet's name to its build data
19-
in the Lake build store. For example, a transitive × direct import pair
20-
for the `lean.imports` facet or an active build target for `lean.c`.
18+
The open type family which maps a Lake data kind to its associated type.
19+
For example, `LeanLib.facetKind` maps to `LeanLib`.
2120
2221
It is an open type, meaning additional mappings can be add lazily
23-
as needed (via `module_data`).
22+
as needed (via `data_type`).
23+
-/
24+
opaque DataType (kind : Name) : Type u
25+
26+
/-- A `Name` descriptor of a data type. -/
27+
class DataKind (α : Type u) where
28+
/-- The name which describes `α`. -/
29+
name : Name
30+
/-- Proof that `α` is the data type described by `name`. -/
31+
wf : α = DataType name
32+
33+
/--
34+
Tries to synthesize a `Name` descriptor of a data type.
35+
Otherwise uses `Name.anonymous` to indicate none was found.
2436
-/
25-
opaque ModuleData (facet : Name) : Type
37+
class OptDataKind (α : Type u) where
38+
/-- The name which describes `α` (or `Name.anonymous` if none). -/
39+
name : Name
40+
/-- Proof that `α` is the data type described by `name` (if valid). -/
41+
wf (h : ¬ name.isAnonymous) : α = DataType name
42+
43+
@[instance low]
44+
def OptDataKind.anonymous : OptDataKind α where
45+
name := .anonymous
46+
wf h := by simp [Name.isAnonymous] at h
47+
48+
@[inline] def OptDataKind.isAnonymous (self : OptDataKind α) : Bool :=
49+
self.name.isAnonymous
50+
51+
theorem OptDataKind.eq_data_type
52+
{self : OptDataKind α} (h : ¬ self.isAnonymous) : α = DataType self.name
53+
:= self.wf h
54+
55+
instance [DataKind α] : OptDataKind α where
56+
name := DataKind.name α
57+
wf _ := DataKind.wf
58+
59+
instance : CoeOut (OptDataKind α) Lean.Name := ⟨(·.name)⟩
60+
instance : ToString (OptDataKind α) := ⟨(·.name.toString)⟩
61+
62+
@[deprecated DataType (since := "2025-03-26")] abbrev TargetData := DataType
2663

2764
/--
28-
The open type family which maps a package facet's name to its build data
29-
in the Lake build store. For example, a transitive dependencies of the package
30-
for the facet `deps`.
65+
The open type family which maps a Lake facet to its output type.
66+
For example, a `FilePath` for the `module.olean` facet.
3167
3268
It is an open type, meaning additional mappings can be add lazily
33-
as needed (via `package_data`).
69+
as needed (via `facet_data`).
3470
-/
35-
opaque PackageData (facet : Name) : Type
71+
opaque FacetOut (facet : Name) : Type
3672

3773
/--
38-
The open type family which maps a (builtin) Lake target's (e.g., `extern_lib`)
39-
facet to its associated build data. For example, an active build target for
40-
the `externLib.static` facet.
74+
The open type family which maps a Lake facet kind and name to its output type.
75+
For example, a `FilePath` for the `module` `olean` facet.
4176
4277
It is an open type, meaning additional mappings can be add lazily
43-
as needed (via `target_data`).
78+
as needed (via `facet_data`).
4479
-/
45-
opaque TargetData (facet : Name) : Type
80+
abbrev FacetData (kind facet : Name) := FacetOut (kind ++ facet)
4681

47-
/-
48-
The open type family which maps a library facet's name to its build data
49-
in the Lake build store. For example, an active build target for the `static`
50-
facet.
82+
instance [h : FamilyDef FacetOut (kind ++ facet) α] : FamilyDef (FacetData kind) facet α :=
83+
⟨h.fam_eq⟩
84+
85+
instance [h : FamilyDef (FacetData kind) facet α] : FamilyDef FacetOut (kind ++ facet) α :=
86+
⟨h.fam_eq⟩
87+
88+
/--
89+
The open type family which maps a module facet's name to its output type.
90+
For example, a `FilePath` for the module `olean` facet.
91+
92+
It is an open type, meaning additional mappings can be add lazily
93+
as needed (via `module_data`).
94+
-/
95+
abbrev ModuleData := FacetData Module.facetKind
96+
97+
/--
98+
The open type family which maps a package facet's name to output type.
99+
For example, an `Arrry Package` of direct dependencies for the `deps` facet.
100+
101+
It is an open type, meaning additional mappings can be add lazily
102+
as needed (via `package_data`).
103+
-/
104+
abbrev PackageData := FacetData Package.facetKind
105+
106+
/-- The kind identifier for facets of a Lean library. -/
107+
@[match_pattern] abbrev LeanLib.facetKind : Name := `lean_lib
108+
109+
/--
110+
The open type family which maps a Lean library facet's name to its output type.
111+
For example, the `FilePath` pf the generated static library for the `static` facet.
51112
52113
It is an open type, meaning additional mappings can be add lazily
53114
as needed (via `library_data`).
54115
-/
55-
abbrev LibraryData (facet : Name) := TargetData (`leanLib ++ facet)
116+
abbrev LibraryData := FacetData LeanLib.facetKind
56117

57-
instance [h : FamilyOut LibraryData facet α] : FamilyDef TargetData (`leanLib ++ facet) α :=
58-
⟨by simp [h.family_key_eq_type]⟩
118+
@[inherit_doc LibraryData]
119+
abbrev LeanLibData := LibraryData
59120

60-
instance [h : FamilyOut TargetData (`leanLib ++ facet) α] : FamilyDef LibraryData facet α :=
61-
⟨h.family_key_eq_type⟩
121+
/-- The kind identifier for facets of a Lean executable. -/
122+
@[match_pattern] abbrev LeanExe.facetKind : Name := `lean_exe
123+
124+
/-- The kind identifier for facets of an external library. -/
125+
@[match_pattern] abbrev ExternLib.facetKind : Name := `extern_lib
126+
127+
/--
128+
The open type family which maps a custom package target
129+
(package × target name) to its output type.
130+
131+
It is an open type, meaning additional mappings can be add lazily
132+
as needed (via `custom_data`).
133+
-/
134+
opaque CustomOut (target : Name × Name) : Type
62135

63136
/--
64-
The open type family which maps a custom target (package × target name) to
65-
its build data in the Lake build store.
137+
The open type family which maps a custom package targetto its output type.
66138
67139
It is an open type, meaning additional mappings can be add lazily
68140
as needed (via `custom_data`).
69141
-/
70-
opaque CustomData (target : Name × Name) : Type
142+
abbrev CustomData (package target : Name) := CustomOut (package, target)
143+
144+
instance [h : FamilyDef CustomOut (p, t) α] : FamilyDef (CustomData p) t α :=
145+
⟨h.fam_eq⟩
71146

72147
--------------------------------------------------------------------------------
73148
/-! ## Build Data -/
@@ -79,55 +154,119 @@ It is a simple type function composed of the separate open type families for
79154
modules facets, package facets, Lake target facets, and custom targets.
80155
-/
81156
abbrev BuildData : BuildKey → Type
82-
| .moduleFacet _ f => ModuleData f
83-
| .packageFacet _ f => PackageData f
84-
| .targetFacet _ _ f => TargetData f
85-
| .customTarget p t => CustomData (p, t)
157+
| .module _ => DataType Module.facetKind
158+
| .package _ => DataType Package.facetKind
159+
| .packageTarget p t => CustomData p t
160+
| .facet _ f => FacetOut f
161+
162+
instance (priority := low) : FamilyDef BuildData (.packageTarget p t) (CustomData p t) := ⟨rfl⟩
163+
instance (priority := low) : FamilyDef BuildData (.facet t f) (FacetOut f) := ⟨rfl⟩
164+
165+
instance [FamilyOut (CustomData p) t α]
166+
: FamilyDef BuildData (.packageTarget p t) α where
167+
fam_eq := by unfold BuildData; simp
168+
169+
instance [FamilyOut DataType Module.facetKind α]
170+
: FamilyDef BuildData (.module k) α where
171+
fam_eq := by unfold BuildData; simp
86172

87-
instance (priority := low) : FamilyDef BuildData k (BuildData k) := ⟨rfl⟩
88-
instance (priority := low) : FamilyDef BuildData (.moduleFacet m f) (ModuleData f) := ⟨rfl⟩
89-
instance (priority := low) : FamilyDef BuildData (.packageFacet p f) (PackageData f) := ⟨rfl⟩
90-
instance (priority := low) : FamilyDef BuildData (.targetFacet p t f) (TargetData f) := ⟨rfl⟩
91-
instance (priority := low) : FamilyDef BuildData (.customTarget p t) (CustomData (p,t)) := ⟨rfl⟩
173+
instance [FamilyOut DataType Package.facetKind α]
174+
: FamilyDef BuildData (.package k) α where
175+
fam_eq := by unfold BuildData; simp
92176

93177
--------------------------------------------------------------------------------
94178
/-! ## Macros for Declaring Build Data -/
95179
--------------------------------------------------------------------------------
96180

181+
open Parser Command
182+
183+
/-- Macro for declaring new `DatayType`. -/
184+
scoped macro (name := dataTypeDecl)
185+
doc?:optional(docComment) "data_type " kind:ident " : " ty:term
186+
: command => do
187+
let fam := mkCIdentFrom (← getRef) ``DataType
188+
let kindName := Name.quoteFrom kind kind.getId
189+
let id := mkIdentFrom kind (canonical := true) <|
190+
kind.getId.modifyBase (kind.getId ++ ·)
191+
`($[$doc?]? family_def $id : $fam $kindName := $ty
192+
instance : DataKind $ty := ⟨$kindName, by simp⟩)
193+
194+
/-- Internal macro for declaring new facet within Lake. -/
195+
scoped macro (name := builtinFacetCommand)
196+
doc?:optional(docComment) tk:"builtin_facet "
197+
id?:optional(atomic(group(ident " @ "))) name:ident " : " ns:ident " => " ty:term
198+
: command => withRef tk do
199+
let fam := mkCIdentFrom tk ``FacetOut
200+
let kindName ← match ns.getId with
201+
| `Package => pure Package.facetKind
202+
| `Module => pure Module.facetKind
203+
| `LeanLib => pure LeanLib.facetKind
204+
| `LeanExe => pure LeanExe.facetKind
205+
| `ExternLib => pure ExternLib.facetKind
206+
| _ => Macro.throwErrorAt ns "unknown facet kind"
207+
let nameLit := Name.quoteFrom name name.getId (canonical := id?.isSome)
208+
let kindLit := Name.quoteFrom ns kindName (canonical := true)
209+
let facet := kindName ++ name.getId
210+
let facetId := mkIdentFrom tk facet (canonical := true)
211+
let facetLit := Name.quoteFrom tk facet
212+
let id ←
213+
if let some id := id? then
214+
let id := id.raw[0]
215+
pure <| mkIdentFrom id (ns.getId ++ id.getId) (canonical := true)
216+
else
217+
match name.getId with
218+
| .str .anonymous n => pure <| mkIdentFrom name (ns.getId.str s!"{n}Facet") (canonical := true)
219+
| _ => Macro.throwErrorAt name "cannot generate facet declaration name from facet name"
220+
`(
221+
$[$doc?]? abbrev $id := $facetLit
222+
family_def $facetId : $fam $facetLit := $ty
223+
instance : FamilyDef FacetOut ($kindLit ++ $nameLit) $ty :=
224+
inferInstanceAs (FamilyDef FacetOut $facetLit $ty)
225+
)
226+
227+
/-- Macro for declaring new `FacetData`. -/
228+
scoped macro (name := facetDataDecl)
229+
doc?:optional(docComment) tk:"facet_data " kind:ident name:ident " : " ty:term
230+
: command => withRef tk do
231+
let fam := mkCIdentFrom tk ``FacetOut
232+
let kindLit := Name.quoteFrom kind kind.getId
233+
let nameLit := Name.quoteFrom name name.getId
234+
let facet := kind.getId ++ name.getId
235+
let facetLit := Name.quoteFrom tk facet
236+
let id := mkIdentFrom tk facet (canonical := true)
237+
`($[$doc?]? family_def $id : $fam $facetLit := $ty
238+
instance : FamilyDef FacetOut ($kindLit ++ $nameLit) $ty :=
239+
inferInstanceAs (FamilyDef FacetOut $facetLit $ty))
240+
97241
/-- Macro for declaring new `PackageData`. -/
98-
scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment)
99-
"package_data " id:ident " : " ty:term : command => do
100-
let dty := mkCIdentFrom (← getRef) ``PackageData
101-
let key := Name.quoteFrom id id.getId
102-
`($[$doc?]? family_def $id : $dty $key := $ty)
242+
scoped macro (name := packageDataDecl)
243+
doc?:optional(docComment) tk:"package_data " facet:ident " : " ty:term
244+
: command => `($[$doc?]? facet_data%$tk $(mkIdentFrom tk Package.facetKind) $facet : $ty)
103245

104246
/-- Macro for declaring new `ModuleData`. -/
105-
scoped macro (name := moduleDataDecl) doc?:optional(Parser.Command.docComment)
106-
"module_data " id:ident " : " ty:term : command => do
107-
let dty := mkCIdentFrom (← getRef) ``ModuleData
108-
let key := Name.quoteFrom id id.getId
109-
`($[$doc?]? family_def $id : $dty $key := $ty)
110-
111-
/-- Macro for declaring new `TargetData` for libraries. -/
112-
scoped macro (name := libraryDataDecl) doc?:optional(Parser.Command.docComment)
113-
"library_data " id:ident " : " ty:term : command => do
114-
let dty := mkCIdentFrom (← getRef) ``TargetData
115-
let key := Name.quoteFrom id id.getId
116-
let id := mkIdentFrom id (canonical := true) <| id.getId.modifyBase (`leanLib ++ ·)
117-
`($[$doc?]? family_def $id : $dty (`leanLib ++ $key) := $ty)
247+
scoped macro (name := moduleDataDecl)
248+
doc?:optional(docComment) tk:"module_data " facet:ident " : " ty:term
249+
: command => `($[$doc?]? facet_data%$tk $(mkIdentFrom tk Module.facetKind) $facet : $ty)
250+
251+
/-- Macro for declaring new `LibraryData`. -/
252+
scoped macro (name := libraryDataDecl)
253+
doc?:optional(docComment) tk:"library_data " facet:ident " : " ty:term
254+
: command => `($[$doc?]? facet_data%$tk $(mkIdentFrom tk LeanLib.facetKind) $facet : $ty)
118255

119256
/-- Macro for declaring new `TargetData`. -/
120-
scoped macro (name := targetDataDecl) doc?:optional(Parser.Command.docComment)
121-
"target_data " id:ident " : " ty:term : command => do
122-
let dty := mkCIdentFrom (← getRef) ``TargetData
123-
let key := Name.quoteFrom id id.getId
124-
`($[$doc?]? family_def $id : $dty $key := $ty)
257+
scoped macro (name := targetDataDecl)
258+
doc?:optional(docComment) tk:"target_data " id:ident " : " ty:term
259+
: command => withRef tk do
260+
let fam := mkCIdentFrom (← getRef) ``TargetData
261+
let idx := Name.quoteFrom id id.getId
262+
`($[$doc?]? family_def $id : $fam $idx := $ty)
125263

126264
/-- Macro for declaring new `CustomData`. -/
127-
scoped macro (name := customDataDecl) doc?:optional(Parser.Command.docComment)
128-
"custom_data " pkg:ident tgt:ident " : " ty:term : command => do
129-
let dty := mkCIdentFrom (← getRef) ``CustomData
265+
scoped macro (name := customDataDecl)
266+
doc?:optional(docComment) tk:"custom_data " pkg:ident tgt:ident " : " ty:term
267+
: command => withRef tk do
268+
let fam := mkCIdentFrom (← getRef) ``CustomOut
130269
let id := mkIdentFrom tgt (pkg.getId ++ tgt.getId)
131270
let pkg := Name.quoteFrom pkg pkg.getId
132271
let tgt := Name.quoteFrom pkg tgt.getId
133-
`($[$doc?]? family_def $id : $dty ($pkg, $tgt) := $ty)
272+
`($[$doc?]? family_def $id : $fam ($pkg, $tgt) := $ty)

‎src/lake/Lake/Build/Executable.lean

+22-2
Original file line numberDiff line numberDiff line change
@@ -22,12 +22,32 @@ def LeanExe.recBuildExe (self : LeanExe) : FetchM (Job FilePath) :=
2222
-/
2323
let mut linkJobs := #[]
2424
for facet in self.root.nativeFacets self.supportInterpreter do
25-
linkJobs := linkJobs.push <| ← fetch <| self.root.facet facet.name
25+
linkJobs := linkJobs.push <| ← facet.fetch self.root
2626
let imports ← (← self.root.transImports.fetch).await
2727
for mod in imports do
2828
for facet in mod.nativeFacets self.supportInterpreter do
29-
linkJobs := linkJobs.push <| ← fetch <| mod.facet facet.name
29+
linkJobs := linkJobs.push <| ← facet.fetch mod
3030
let deps := (← (← self.pkg.transDeps.fetch).await).push self.pkg
3131
for dep in deps do for lib in dep.externLibs do
3232
linkJobs := linkJobs.push <| ← lib.static.fetch
3333
buildLeanExe self.file linkJobs self.weakLinkArgs self.linkArgs self.sharedLean
34+
35+
/-- The facet configuration for the builtin `LeanExe.exeFacet`. -/
36+
def LeanExe.exeFacetConfig : LeanExeFacetConfig exeFacet :=
37+
mkFacetJobConfig recBuildExe
38+
39+
def LeanExe.recBuildDefault (lib : LeanExe) : FetchM (Job FilePath) :=
40+
lib.exe.fetch
41+
42+
/-- The facet configuration for the builtin `ExternLib.dynlibFacet`. -/
43+
def LeanExe.defaultFacetConfig : LeanExeFacetConfig defaultFacet :=
44+
mkFacetJobConfig recBuildDefault
45+
46+
/--
47+
A name-configuration map for the initial set of
48+
Lean executable facets (e.g., `exe`).
49+
-/
50+
def LeanExe.initFacetConfigs : DNameMap LeanExeFacetConfig :=
51+
DNameMap.empty
52+
|>.insert defaultFacet defaultFacetConfig
53+
|>.insert exeFacet exeFacetConfig

0 commit comments

Comments
 (0)