Skip to content
This repository was archived by the owner on Oct 25, 2023. It is now read-only.

Commit 13930f2

Browse files
tydeutydeu
committed
refactor: reorg build code into smaller, focused files
1 parent f4c604b commit 13930f2

18 files changed

+930
-775
lines changed

Diff for: ‎Lake/Build.lean

+3-4
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,7 @@ Authors: Mac Malone
55
-/
66
import Lake.Build.Monad
77
import Lake.Build.Actions
8-
import Lake.Build.TargetTypes
9-
import Lake.Build.Targets
108
import Lake.Build.Module
11-
import Lake.Build.Package
12-
import Lake.Build.Binary
9+
import Lake.Build.Library
10+
import Lake.Build.Executable
11+
import Lake.Build.Imports

Diff for: ‎Lake/Build/Data.lean

+53
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
/-
2+
Copyright (c) 2022 Mac Malone. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Mac Malone
5+
-/
6+
import Lake.Build.Key
7+
import Lake.Util.DynamicType
8+
9+
open Lean
10+
namespace Lake
11+
12+
/--
13+
Type of build data associated with a module facet in the Lake build store.
14+
For example a transitive × direct import pair for `imports` or an active build
15+
target for `lean.c`.
16+
17+
It is a dynamic type, meaning additional alternatives can be add lazily
18+
as needed.
19+
-/
20+
opaque ModuleData (facet : WfName) : Type
21+
22+
/-- Type of build data associated with package facets (e.g., `extraDep`). -/
23+
opaque PackageData (facet : WfName) : Type
24+
25+
/-- Type of build data associated with Lake targets (e.g., `extern_lib`). -/
26+
opaque TargetData (key : BuildKey) : Type
27+
28+
/--
29+
Type of the build data associated with a key in the Lake build store.
30+
It is dynamic type composed of the three separate dynamic types for modules,
31+
packages, and targets.
32+
-/
33+
def BuildData (key : BuildKey) :=
34+
if key.isModuleKey then
35+
ModuleData key.facet
36+
else if key.isPackageKey then
37+
PackageData key.facet
38+
else
39+
TargetData key
40+
41+
/-- Macro for declaring new `PackageData`. -/
42+
scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment)
43+
"package_data " id:ident " : " ty:term : command => do
44+
let dty := mkCIdentFrom (← getRef) ``PackageData
45+
let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
46+
`($[$doc?]? dynamic_data $id : $dty $key := $ty)
47+
48+
/-- Macro for declaring new `ModuleData`. -/
49+
scoped macro (name := moduleDataDecl) doc?:optional(Parser.Command.docComment)
50+
"module_data " id:ident " : " ty:term : command => do
51+
let dty := mkCIdentFrom (← getRef) ``ModuleData
52+
let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
53+
`($[$doc?]? dynamic_data $id : $dty $key := $ty)

Diff for: ‎Lake/Build/Executable.lean

+32
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
/-
2+
Copyright (c) 2022 Mac Malone. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Mac Malone
5+
-/
6+
import Lake.Build.Library
7+
8+
open Std System
9+
open Lean (Name NameMap)
10+
11+
namespace Lake
12+
13+
-- # Build Package Executable
14+
15+
def Package.mkExeTarget (self : Package) (exe : LeanExeConfig) : FileTarget :=
16+
let exeFile := self.binDir / exe.fileName
17+
BuildTarget.mk' exeFile do
18+
let root : Module := ⟨self, WfName.ofName exe.root⟩
19+
let cTargetMap ← buildModuleFacetMap #[root] &`lean.c
20+
let pkgLinkTargets ← self.linkTargetsOf cTargetMap
21+
let linkTargets :=
22+
if self.isLocalModule exe.root then
23+
pkgLinkTargets
24+
else
25+
let rootTarget := cTargetMap.find? root.name |>.get!
26+
let rootLinkTarget := root.mkOTarget <| Target.active rootTarget
27+
#[rootLinkTarget] ++ pkgLinkTargets
28+
let target := leanExeTarget exeFile linkTargets exe.linkArgs
29+
target.materializeAsync
30+
31+
protected def Package.exeTarget (self : Package) : FileTarget :=
32+
self.mkExeTarget self.builtinExeConfig

Diff for: ‎Lake/Build/Imports.lean

+46
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
/-
2+
Copyright (c) 2022 Mac Malone. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Mac Malone
5+
-/
6+
import Lake.Build.Module
7+
import Lake.Config.Workspace
8+
9+
/-!
10+
Definitions to support `lake print-paths` builds.
11+
-/
12+
13+
namespace Lake
14+
15+
/--
16+
Construct an `Array` of `Module`s for the workspace-local modules of
17+
a `List` of import strings.
18+
-/
19+
def Workspace.processImportList
20+
(imports : List String) (self : Workspace) : Array Module := Id.run do
21+
let mut localImports := #[]
22+
for imp in imports do
23+
if let some mod := self.findModule? imp.toName then
24+
localImports := localImports.push mod
25+
return localImports
26+
27+
/--
28+
Build the workspace-local modules of list of imports.
29+
30+
Build only module `.olean` and `.ilean` files if
31+
the default package build does not include any binary targets
32+
Otherwise, also build `.c` files.
33+
-/
34+
def Package.buildImportsAndDeps (imports : List String) (self : Package) : BuildM PUnit := do
35+
if imports.isEmpty then
36+
-- build the package's (and its dependencies') `extraDepTarget`
37+
buildPackageFacet self &`extraDep >>= (·.buildOpaque)
38+
else
39+
-- build local imports from list
40+
let mods := (← getWorkspace).processImportList imports
41+
if self.leanExes.isEmpty && self.defaultFacet matches .none | .leanLib | .oleans then
42+
let targets ← buildModuleFacetArray mods &`lean
43+
targets.forM (·.buildOpaque)
44+
else
45+
let targets ← buildModuleFacetArray mods &`lean.c
46+
targets.forM (·.buildOpaque)

Diff for: ‎Lake/Build/Index.lean

+178
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,178 @@
1+
/-
2+
Copyright (c) 2022 Mac Malone. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Mac Malone
5+
-/
6+
import Lake.Build.Module1
7+
import Lake.Build.Topological
8+
import Lake.Util.EStateT
9+
10+
/-!
11+
# The Lake Build Index
12+
13+
The Lake build index is the complete map of Lake build keys to
14+
Lake build functions, which is used by Lake to build any Lake build info.
15+
16+
This module contains the definitions used to formalize this concept,
17+
and it leverages the index to perform topological-based recursive builds.
18+
-/
19+
20+
open Std Lean
21+
namespace Lake
22+
23+
/-!
24+
## Facet Build Maps
25+
-/
26+
27+
/-- A map from module facet names to build functions. -/
28+
abbrev ModuleBuildMap (m : Type → Type v) :=
29+
DRBMap WfName (cmp := WfName.quickCmp) fun k =>
30+
Module → IndexBuildFn m → m (ModuleData k)
31+
32+
@[inline] def ModuleBuildMap.empty : ModuleBuildMap m := DRBMap.empty
33+
34+
/-- A map from package facet names to build functions. -/
35+
abbrev PackageBuildMap (m : Type → Type v) :=
36+
DRBMap WfName (cmp := WfName.quickCmp) fun k =>
37+
Package → IndexBuildFn m → m (PackageData k)
38+
39+
@[inline] def PackageBuildMap.empty : PackageBuildMap m := DRBMap.empty
40+
41+
/-!
42+
## Build Function Constructor Helpers
43+
-/
44+
45+
/--
46+
Converts a conveniently typed module facet build function into its
47+
dynamically typed equivalent.
48+
-/
49+
@[inline] def mkModuleFacetBuild {facet : WfName}
50+
(build : Module → IndexBuildFn m → m α) [h : DynamicType ModuleData facet α]
51+
: Module → IndexBuildFn m → m (ModuleData facet) :=
52+
cast (by rw [← h.eq_dynamic_type]) build
53+
54+
/--
55+
Converts a conveniently typed package facet build function into its
56+
dynamically typed equivalent.
57+
-/
58+
@[inline] def mkPackageFacetBuild {facet : WfName}
59+
(build : Package → IndexBuildFn m → m α) [h : DynamicType PackageData facet α]
60+
: Package → IndexBuildFn m → m (PackageData facet) :=
61+
cast (by rw [← h.eq_dynamic_type]) build
62+
63+
section
64+
variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
65+
66+
/-!
67+
## Initial Facet Maps
68+
-/
69+
70+
/--
71+
A module facet name to build function map that contains builders for
72+
the initial set of Lake module facets (e.g., `lean.{imports, c, o, dynlib]`).
73+
-/
74+
@[specialize] def moduleBuildMap : ModuleBuildMap m :=
75+
have : MonadLift BuildM m := ⟨liftM⟩
76+
ModuleBuildMap.empty.insert
77+
-- Compute unique imports (direct × transitive)
78+
&`lean.imports (mkModuleFacetBuild <| fun mod recurse => do
79+
mod.recParseImports recurse
80+
) |>.insert
81+
-- Build module (`.olean` and `.ilean`)
82+
&`lean (mkModuleFacetBuild <| fun mod recurse => do
83+
mod.recBuildLean false recurse
84+
) |>.insert
85+
&`olean (mkModuleFacetBuild <| fun mod recurse => do
86+
mod.recBuildFacet &`lean recurse
87+
) |>.insert
88+
&`ilean (mkModuleFacetBuild <| fun mod recurse => do
89+
mod.recBuildFacet &`lean recurse
90+
) |>.insert
91+
-- Build module `.c` (and `.olean` and `.ilean`)
92+
&`lean.c (mkModuleFacetBuild <| fun mod recurse => do
93+
mod.recBuildLean true recurse <&> (·.withInfo mod.cFile)
94+
) |>.insert
95+
-- Build module `.o`
96+
&`lean.o (mkModuleFacetBuild <| fun mod recurse => do
97+
let cTarget ← mod.recBuildFacet &`lean.c recurse
98+
mod.mkOTarget (Target.active cTarget) |>.activate
99+
) |>.insert
100+
-- Build shared library for `--load-dynlb`
101+
&`lean.dynlib (mkModuleFacetBuild <| fun mod recurse => do
102+
mod.recBuildDynLib recurse
103+
)
104+
105+
/--
106+
A package facet name to build function map that contains builders for
107+
the initial set of Lake package facets (e.g., `extraDep`).
108+
-/
109+
@[specialize] def packageBuildMap : PackageBuildMap m :=
110+
have : MonadLift BuildM m := ⟨liftM⟩
111+
PackageBuildMap.empty.insert
112+
-- Build the `extraDepTarget` for the package and its transitive dependencies
113+
&`extraDep (mkPackageFacetBuild <| fun pkg recurse => do
114+
let mut target := ActiveTarget.nil
115+
for dep in pkg.dependencies do
116+
if let some depPkg ← findPackage? dep.name then
117+
let extraDepTarget ← depPkg.recBuildFacet &`extraDep recurse
118+
target ← target.mixOpaqueAsync extraDepTarget
119+
target.mixOpaqueAsync <| ← pkg.extraDepTarget.activate
120+
)
121+
122+
/-!
123+
## Topologically-based Recursive Build Using the Index
124+
-/
125+
126+
/-- The type of a recursive build function for the Lake build index. -/
127+
abbrev RecIndexBuildFn (m) :=
128+
DRecBuildFn BuildInfo (BuildData ·.key) m
129+
130+
/-- Recursive build function for anything in the Lake build index. -/
131+
@[specialize] def recBuildIndex : RecIndexBuildFn m := fun info recurse => do
132+
have : MonadLift BuildM m := ⟨liftM⟩
133+
match info with
134+
| .module mod facet =>
135+
if let some build := moduleBuildMap.find? facet then
136+
build mod recurse
137+
else
138+
error s!"do not know how to build module facet `{facet}`"
139+
| .package pkg facet =>
140+
if let some build := packageBuildMap.find? facet then
141+
build pkg recurse
142+
else
143+
error s!"do not know how to build package facet `{facet}`"
144+
| _ =>
145+
error s!"do not know how to build `{info.key}`"
146+
147+
/--
148+
Recursively build the given info using the Lake build index
149+
and a topological / suspending scheduler.
150+
-/
151+
@[specialize] def buildIndexTop (info : BuildInfo) : CycleT BuildKey m (BuildData info.key) :=
152+
buildDTop BuildData BuildInfo.key recBuildIndex info
153+
154+
/--
155+
Build the package's specified facet recursively using a topological-based
156+
scheduler, storing the results in the monad's store and returning the result
157+
of the top-level build.
158+
-/
159+
@[inline] def buildPackageTop (pkg : Package) (facet : WfName)
160+
[h : DynamicType PackageData facet α] : CycleT BuildKey m α :=
161+
have of_data := by unfold BuildData, BuildInfo.key; simp [h.eq_dynamic_type]
162+
cast of_data <| buildIndexTop (m := m) <| BuildInfo.package pkg facet
163+
164+
end
165+
166+
/-!
167+
## Package Facet Builders
168+
-/
169+
170+
/--
171+
Recursively build the specified facet of the given package,
172+
returning the result.
173+
-/
174+
def buildPackageFacet
175+
(pkg : Package) (facet : WfName)
176+
[DynamicType PackageData facet α] : BuildM α := do
177+
failOnBuildCycle <| ← EStateT.run' BuildStore.empty do
178+
buildPackageTop pkg facet

Diff for: ‎Lake/Build/Info.lean

+73
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
/-
2+
Copyright (c) 2022 Mac Malone. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Mac Malone
5+
-/
6+
import Lake.Build.Data
7+
import Lake.Config.Module
8+
9+
namespace Lake
10+
11+
-- # Build Key Constructor Helpers
12+
13+
@[inline] def Module.mkBuildKey (facet : WfName) (self : Module) : ModuleBuildKey facet :=
14+
⟨⟨none, self.name, facet⟩, rfl, rfl⟩
15+
16+
@[inline] def Package.mkBuildKey (facet : WfName) (self : Package) : PackageBuildKey facet :=
17+
⟨⟨self.name, none, facet⟩, rfl, rfl⟩
18+
19+
-- # Build Info
20+
21+
/-- The type of Lake's build info. -/
22+
inductive BuildInfo
23+
| module (module : Module) (facet : WfName)
24+
| package (package : Package) (facet : WfName)
25+
| target (package : Package) (target : WfName) (facet : WfName)
26+
27+
def BuildInfo.key : (self : BuildInfo) → BuildKey
28+
| module m f => ⟨none, m.name, f⟩
29+
| package p f => ⟨p.name, none, f⟩
30+
| target p t f => ⟨p.name, t, f⟩
31+
32+
/-- A build function for a single element of the Lake build index. -/
33+
abbrev IndexBuildFn (m : Type → Type v) :=
34+
-- `DBuildFn BuildInfo (BuildData ·.key) m` with less imports
35+
(info : BuildInfo) → m (BuildData info.key)
36+
37+
@[inline] def Module.recBuildFacet {m : Type → Type v}
38+
(mod : Module) (facet : WfName) [DynamicType ModuleData facet α]
39+
(build : (info : BuildInfo) → m (BuildData info.key)) : m α :=
40+
let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
41+
cast to_data <| build <| BuildInfo.module mod facet
42+
43+
@[inline] def Package.recBuildFacet {m : Type → Type v}
44+
(pkg : Package) (facet : WfName) [DynamicType PackageData facet α]
45+
(build : (info : BuildInfo) → m (BuildData info.key)) : m α :=
46+
let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
47+
cast to_data <| build <| BuildInfo.package pkg facet
48+
49+
-- # Data Types of Build Results
50+
51+
/-- Lean binary build (`olean`, `ilean` files) -/
52+
module_data lean : ActiveOpaqueTarget
53+
54+
/-- The `olean` file produced by `lean` -/
55+
module_data olean : ActiveOpaqueTarget
56+
57+
/-- The `ilean` file produced by `lean` -/
58+
module_data ilean : ActiveOpaqueTarget
59+
60+
/-- The C file built from the Lean file via `lean` -/
61+
module_data lean.c : ActiveFileTarget
62+
63+
/-- The object file built from `lean.c` -/
64+
module_data lean.o : ActiveFileTarget
65+
66+
/-- Shared library for `--load-dynlib` -/
67+
module_data lean.dynlib : ActiveFileTarget
68+
69+
/-- The direct × transitive imports of the Lean module. -/
70+
module_data lean.imports : Array Module × Array Module
71+
72+
/-- The package's `extraDepTarget`. -/
73+
package_data extraDep : ActiveOpaqueTarget

0 commit comments

Comments
 (0)