refactor: reorg build code into smaller, focused files
This commit is contained in:
tydeu
parent
d3c373478e
commit
d842158172
18 changed files with 930 additions and 775 deletions
|
|
@ -5,8 +5,7 @@ Authors: Mac Malone
|
|||
-/
|
||||
import Lake.Build.Monad
|
||||
import Lake.Build.Actions
|
||||
import Lake.Build.TargetTypes
|
||||
import Lake.Build.Targets
|
||||
import Lake.Build.Module
|
||||
import Lake.Build.Package
|
||||
import Lake.Build.Binary
|
||||
import Lake.Build.Library
|
||||
import Lake.Build.Executable
|
||||
import Lake.Build.Imports
|
||||
|
|
|
|||
53
Lake/Build/Data.lean
Normal file
53
Lake/Build/Data.lean
Normal file
|
|
@ -0,0 +1,53 @@
|
|||
/-
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lake.Build.Key
|
||||
import Lake.Util.DynamicType
|
||||
|
||||
open Lean
|
||||
namespace Lake
|
||||
|
||||
/--
|
||||
Type of build data associated with a module facet in the Lake build store.
|
||||
For example a transitive × direct import pair for `imports` or an active build
|
||||
target for `lean.c`.
|
||||
|
||||
It is a dynamic type, meaning additional alternatives can be add lazily
|
||||
as needed.
|
||||
-/
|
||||
opaque ModuleData (facet : WfName) : Type
|
||||
|
||||
/-- Type of build data associated with package facets (e.g., `extraDep`). -/
|
||||
opaque PackageData (facet : WfName) : Type
|
||||
|
||||
/-- Type of build data associated with Lake targets (e.g., `extern_lib`). -/
|
||||
opaque TargetData (key : BuildKey) : Type
|
||||
|
||||
/--
|
||||
Type of the build data associated with a key in the Lake build store.
|
||||
It is dynamic type composed of the three separate dynamic types for modules,
|
||||
packages, and targets.
|
||||
-/
|
||||
def BuildData (key : BuildKey) :=
|
||||
if key.isModuleKey then
|
||||
ModuleData key.facet
|
||||
else if key.isPackageKey then
|
||||
PackageData key.facet
|
||||
else
|
||||
TargetData key
|
||||
|
||||
/-- Macro for declaring new `PackageData`. -/
|
||||
scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment)
|
||||
"package_data " id:ident " : " ty:term : command => do
|
||||
let dty := mkCIdentFrom (← getRef) ``PackageData
|
||||
let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
|
||||
`($[$doc?]? dynamic_data $id : $dty $key := $ty)
|
||||
|
||||
/-- Macro for declaring new `ModuleData`. -/
|
||||
scoped macro (name := moduleDataDecl) doc?:optional(Parser.Command.docComment)
|
||||
"module_data " id:ident " : " ty:term : command => do
|
||||
let dty := mkCIdentFrom (← getRef) ``ModuleData
|
||||
let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
|
||||
`($[$doc?]? dynamic_data $id : $dty $key := $ty)
|
||||
32
Lake/Build/Executable.lean
Normal file
32
Lake/Build/Executable.lean
Normal file
|
|
@ -0,0 +1,32 @@
|
|||
/-
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lake.Build.Library
|
||||
|
||||
open Std System
|
||||
open Lean (Name NameMap)
|
||||
|
||||
namespace Lake
|
||||
|
||||
-- # Build Package Executable
|
||||
|
||||
def Package.mkExeTarget (self : Package) (exe : LeanExeConfig) : FileTarget :=
|
||||
let exeFile := self.binDir / exe.fileName
|
||||
BuildTarget.mk' exeFile do
|
||||
let root : Module := ⟨self, WfName.ofName exe.root⟩
|
||||
let cTargetMap ← buildModuleFacetMap #[root] &`lean.c
|
||||
let pkgLinkTargets ← self.linkTargetsOf cTargetMap
|
||||
let linkTargets :=
|
||||
if self.isLocalModule exe.root then
|
||||
pkgLinkTargets
|
||||
else
|
||||
let rootTarget := cTargetMap.find? root.name |>.get!
|
||||
let rootLinkTarget := root.mkOTarget <| Target.active rootTarget
|
||||
#[rootLinkTarget] ++ pkgLinkTargets
|
||||
let target := leanExeTarget exeFile linkTargets exe.linkArgs
|
||||
target.materializeAsync
|
||||
|
||||
protected def Package.exeTarget (self : Package) : FileTarget :=
|
||||
self.mkExeTarget self.builtinExeConfig
|
||||
46
Lake/Build/Imports.lean
Normal file
46
Lake/Build/Imports.lean
Normal file
|
|
@ -0,0 +1,46 @@
|
|||
/-
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lake.Build.Module
|
||||
import Lake.Config.Workspace
|
||||
|
||||
/-!
|
||||
Definitions to support `lake print-paths` builds.
|
||||
-/
|
||||
|
||||
namespace Lake
|
||||
|
||||
/--
|
||||
Construct an `Array` of `Module`s for the workspace-local modules of
|
||||
a `List` of import strings.
|
||||
-/
|
||||
def Workspace.processImportList
|
||||
(imports : List String) (self : Workspace) : Array Module := Id.run do
|
||||
let mut localImports := #[]
|
||||
for imp in imports do
|
||||
if let some mod := self.findModule? imp.toName then
|
||||
localImports := localImports.push mod
|
||||
return localImports
|
||||
|
||||
/--
|
||||
Build the workspace-local modules of list of imports.
|
||||
|
||||
Build only module `.olean` and `.ilean` files if
|
||||
the default package build does not include any binary targets
|
||||
Otherwise, also build `.c` files.
|
||||
-/
|
||||
def Package.buildImportsAndDeps (imports : List String) (self : Package) : BuildM PUnit := do
|
||||
if imports.isEmpty then
|
||||
-- build the package's (and its dependencies') `extraDepTarget`
|
||||
buildPackageFacet self &`extraDep >>= (·.buildOpaque)
|
||||
else
|
||||
-- build local imports from list
|
||||
let mods := (← getWorkspace).processImportList imports
|
||||
if self.leanExes.isEmpty && self.defaultFacet matches .none | .leanLib | .oleans then
|
||||
let targets ← buildModuleFacetArray mods &`lean
|
||||
targets.forM (·.buildOpaque)
|
||||
else
|
||||
let targets ← buildModuleFacetArray mods &`lean.c
|
||||
targets.forM (·.buildOpaque)
|
||||
178
Lake/Build/Index.lean
Normal file
178
Lake/Build/Index.lean
Normal file
|
|
@ -0,0 +1,178 @@
|
|||
/-
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lake.Build.Module1
|
||||
import Lake.Build.Topological
|
||||
import Lake.Util.EStateT
|
||||
|
||||
/-!
|
||||
# The Lake Build Index
|
||||
|
||||
The Lake build index is the complete map of Lake build keys to
|
||||
Lake build functions, which is used by Lake to build any Lake build info.
|
||||
|
||||
This module contains the definitions used to formalize this concept,
|
||||
and it leverages the index to perform topological-based recursive builds.
|
||||
-/
|
||||
|
||||
open Std Lean
|
||||
namespace Lake
|
||||
|
||||
/-!
|
||||
## Facet Build Maps
|
||||
-/
|
||||
|
||||
/-- A map from module facet names to build functions. -/
|
||||
abbrev ModuleBuildMap (m : Type → Type v) :=
|
||||
DRBMap WfName (cmp := WfName.quickCmp) fun k =>
|
||||
Module → IndexBuildFn m → m (ModuleData k)
|
||||
|
||||
@[inline] def ModuleBuildMap.empty : ModuleBuildMap m := DRBMap.empty
|
||||
|
||||
/-- A map from package facet names to build functions. -/
|
||||
abbrev PackageBuildMap (m : Type → Type v) :=
|
||||
DRBMap WfName (cmp := WfName.quickCmp) fun k =>
|
||||
Package → IndexBuildFn m → m (PackageData k)
|
||||
|
||||
@[inline] def PackageBuildMap.empty : PackageBuildMap m := DRBMap.empty
|
||||
|
||||
/-!
|
||||
## Build Function Constructor Helpers
|
||||
-/
|
||||
|
||||
/--
|
||||
Converts a conveniently typed module facet build function into its
|
||||
dynamically typed equivalent.
|
||||
-/
|
||||
@[inline] def mkModuleFacetBuild {facet : WfName}
|
||||
(build : Module → IndexBuildFn m → m α) [h : DynamicType ModuleData facet α]
|
||||
: Module → IndexBuildFn m → m (ModuleData facet) :=
|
||||
cast (by rw [← h.eq_dynamic_type]) build
|
||||
|
||||
/--
|
||||
Converts a conveniently typed package facet build function into its
|
||||
dynamically typed equivalent.
|
||||
-/
|
||||
@[inline] def mkPackageFacetBuild {facet : WfName}
|
||||
(build : Package → IndexBuildFn m → m α) [h : DynamicType PackageData facet α]
|
||||
: Package → IndexBuildFn m → m (PackageData facet) :=
|
||||
cast (by rw [← h.eq_dynamic_type]) build
|
||||
|
||||
section
|
||||
variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
|
||||
|
||||
/-!
|
||||
## Initial Facet Maps
|
||||
-/
|
||||
|
||||
/--
|
||||
A module facet name to build function map that contains builders for
|
||||
the initial set of Lake module facets (e.g., `lean.{imports, c, o, dynlib]`).
|
||||
-/
|
||||
@[specialize] def moduleBuildMap : ModuleBuildMap m :=
|
||||
have : MonadLift BuildM m := ⟨liftM⟩
|
||||
ModuleBuildMap.empty.insert
|
||||
-- Compute unique imports (direct × transitive)
|
||||
&`lean.imports (mkModuleFacetBuild <| fun mod recurse => do
|
||||
mod.recParseImports recurse
|
||||
) |>.insert
|
||||
-- Build module (`.olean` and `.ilean`)
|
||||
&`lean (mkModuleFacetBuild <| fun mod recurse => do
|
||||
mod.recBuildLean false recurse
|
||||
) |>.insert
|
||||
&`olean (mkModuleFacetBuild <| fun mod recurse => do
|
||||
mod.recBuildFacet &`lean recurse
|
||||
) |>.insert
|
||||
&`ilean (mkModuleFacetBuild <| fun mod recurse => do
|
||||
mod.recBuildFacet &`lean recurse
|
||||
) |>.insert
|
||||
-- Build module `.c` (and `.olean` and `.ilean`)
|
||||
&`lean.c (mkModuleFacetBuild <| fun mod recurse => do
|
||||
mod.recBuildLean true recurse <&> (·.withInfo mod.cFile)
|
||||
) |>.insert
|
||||
-- Build module `.o`
|
||||
&`lean.o (mkModuleFacetBuild <| fun mod recurse => do
|
||||
let cTarget ← mod.recBuildFacet &`lean.c recurse
|
||||
mod.mkOTarget (Target.active cTarget) |>.activate
|
||||
) |>.insert
|
||||
-- Build shared library for `--load-dynlb`
|
||||
&`lean.dynlib (mkModuleFacetBuild <| fun mod recurse => do
|
||||
mod.recBuildDynLib recurse
|
||||
)
|
||||
|
||||
/--
|
||||
A package facet name to build function map that contains builders for
|
||||
the initial set of Lake package facets (e.g., `extraDep`).
|
||||
-/
|
||||
@[specialize] def packageBuildMap : PackageBuildMap m :=
|
||||
have : MonadLift BuildM m := ⟨liftM⟩
|
||||
PackageBuildMap.empty.insert
|
||||
-- Build the `extraDepTarget` for the package and its transitive dependencies
|
||||
&`extraDep (mkPackageFacetBuild <| fun pkg recurse => do
|
||||
let mut target := ActiveTarget.nil
|
||||
for dep in pkg.dependencies do
|
||||
if let some depPkg ← findPackage? dep.name then
|
||||
let extraDepTarget ← depPkg.recBuildFacet &`extraDep recurse
|
||||
target ← target.mixOpaqueAsync extraDepTarget
|
||||
target.mixOpaqueAsync <| ← pkg.extraDepTarget.activate
|
||||
)
|
||||
|
||||
/-!
|
||||
## Topologically-based Recursive Build Using the Index
|
||||
-/
|
||||
|
||||
/-- The type of a recursive build function for the Lake build index. -/
|
||||
abbrev RecIndexBuildFn (m) :=
|
||||
DRecBuildFn BuildInfo (BuildData ·.key) m
|
||||
|
||||
/-- Recursive build function for anything in the Lake build index. -/
|
||||
@[specialize] def recBuildIndex : RecIndexBuildFn m := fun info recurse => do
|
||||
have : MonadLift BuildM m := ⟨liftM⟩
|
||||
match info with
|
||||
| .module mod facet =>
|
||||
if let some build := moduleBuildMap.find? facet then
|
||||
build mod recurse
|
||||
else
|
||||
error s!"do not know how to build module facet `{facet}`"
|
||||
| .package pkg facet =>
|
||||
if let some build := packageBuildMap.find? facet then
|
||||
build pkg recurse
|
||||
else
|
||||
error s!"do not know how to build package facet `{facet}`"
|
||||
| _ =>
|
||||
error s!"do not know how to build `{info.key}`"
|
||||
|
||||
/--
|
||||
Recursively build the given info using the Lake build index
|
||||
and a topological / suspending scheduler.
|
||||
-/
|
||||
@[specialize] def buildIndexTop (info : BuildInfo) : CycleT BuildKey m (BuildData info.key) :=
|
||||
buildDTop BuildData BuildInfo.key recBuildIndex info
|
||||
|
||||
/--
|
||||
Build the package's specified facet recursively using a topological-based
|
||||
scheduler, storing the results in the monad's store and returning the result
|
||||
of the top-level build.
|
||||
-/
|
||||
@[inline] def buildPackageTop (pkg : Package) (facet : WfName)
|
||||
[h : DynamicType PackageData facet α] : CycleT BuildKey m α :=
|
||||
have of_data := by unfold BuildData, BuildInfo.key; simp [h.eq_dynamic_type]
|
||||
cast of_data <| buildIndexTop (m := m) <| BuildInfo.package pkg facet
|
||||
|
||||
end
|
||||
|
||||
/-!
|
||||
## Package Facet Builders
|
||||
-/
|
||||
|
||||
/--
|
||||
Recursively build the specified facet of the given package,
|
||||
returning the result.
|
||||
-/
|
||||
def buildPackageFacet
|
||||
(pkg : Package) (facet : WfName)
|
||||
[DynamicType PackageData facet α] : BuildM α := do
|
||||
failOnBuildCycle <| ← EStateT.run' BuildStore.empty do
|
||||
buildPackageTop pkg facet
|
||||
73
Lake/Build/Info.lean
Normal file
73
Lake/Build/Info.lean
Normal file
|
|
@ -0,0 +1,73 @@
|
|||
/-
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lake.Build.Data
|
||||
import Lake.Config.Module
|
||||
|
||||
namespace Lake
|
||||
|
||||
-- # Build Key Constructor Helpers
|
||||
|
||||
@[inline] def Module.mkBuildKey (facet : WfName) (self : Module) : ModuleBuildKey facet :=
|
||||
⟨⟨none, self.name, facet⟩, rfl, rfl⟩
|
||||
|
||||
@[inline] def Package.mkBuildKey (facet : WfName) (self : Package) : PackageBuildKey facet :=
|
||||
⟨⟨self.name, none, facet⟩, rfl, rfl⟩
|
||||
|
||||
-- # Build Info
|
||||
|
||||
/-- The type of Lake's build info. -/
|
||||
inductive BuildInfo
|
||||
| module (module : Module) (facet : WfName)
|
||||
| package (package : Package) (facet : WfName)
|
||||
| target (package : Package) (target : WfName) (facet : WfName)
|
||||
|
||||
def BuildInfo.key : (self : BuildInfo) → BuildKey
|
||||
| module m f => ⟨none, m.name, f⟩
|
||||
| package p f => ⟨p.name, none, f⟩
|
||||
| target p t f => ⟨p.name, t, f⟩
|
||||
|
||||
/-- A build function for a single element of the Lake build index. -/
|
||||
abbrev IndexBuildFn (m : Type → Type v) :=
|
||||
-- `DBuildFn BuildInfo (BuildData ·.key) m` with less imports
|
||||
(info : BuildInfo) → m (BuildData info.key)
|
||||
|
||||
@[inline] def Module.recBuildFacet {m : Type → Type v}
|
||||
(mod : Module) (facet : WfName) [DynamicType ModuleData facet α]
|
||||
(build : (info : BuildInfo) → m (BuildData info.key)) : m α :=
|
||||
let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
|
||||
cast to_data <| build <| BuildInfo.module mod facet
|
||||
|
||||
@[inline] def Package.recBuildFacet {m : Type → Type v}
|
||||
(pkg : Package) (facet : WfName) [DynamicType PackageData facet α]
|
||||
(build : (info : BuildInfo) → m (BuildData info.key)) : m α :=
|
||||
let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
|
||||
cast to_data <| build <| BuildInfo.package pkg facet
|
||||
|
||||
-- # Data Types of Build Results
|
||||
|
||||
/-- Lean binary build (`olean`, `ilean` files) -/
|
||||
module_data lean : ActiveOpaqueTarget
|
||||
|
||||
/-- The `olean` file produced by `lean` -/
|
||||
module_data olean : ActiveOpaqueTarget
|
||||
|
||||
/-- The `ilean` file produced by `lean` -/
|
||||
module_data ilean : ActiveOpaqueTarget
|
||||
|
||||
/-- The C file built from the Lean file via `lean` -/
|
||||
module_data lean.c : ActiveFileTarget
|
||||
|
||||
/-- The object file built from `lean.c` -/
|
||||
module_data lean.o : ActiveFileTarget
|
||||
|
||||
/-- Shared library for `--load-dynlib` -/
|
||||
module_data lean.dynlib : ActiveFileTarget
|
||||
|
||||
/-- The direct × transitive imports of the Lean module. -/
|
||||
module_data lean.imports : Array Module × Array Module
|
||||
|
||||
/-- The package's `extraDepTarget`. -/
|
||||
package_data extraDep : ActiveOpaqueTarget
|
||||
142
Lake/Build/Key.lean
Normal file
142
Lake/Build/Key.lean
Normal file
|
|
@ -0,0 +1,142 @@
|
|||
/-
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lake.Util.Name
|
||||
|
||||
namespace Lake
|
||||
|
||||
/-- The type of keys in the Lake build store. -/
|
||||
structure BuildKey where
|
||||
package? : Option WfName
|
||||
target? : Option WfName
|
||||
facet : WfName
|
||||
deriving Inhabited, Repr, DecidableEq, Hashable
|
||||
|
||||
namespace BuildKey
|
||||
|
||||
@[inline] def hasPackage (self : BuildKey) : Bool :=
|
||||
self.package? ≠ none
|
||||
|
||||
@[simp] theorem hasPackage_mk : BuildKey.hasPackage ⟨some p, x, f⟩ := by
|
||||
simp [BuildKey.hasPackage]
|
||||
|
||||
@[inline] def package (self : BuildKey) (h : self.hasPackage) : WfName :=
|
||||
match mh:self.package? with
|
||||
| some n => n
|
||||
| none => absurd mh <| by
|
||||
unfold hasPackage at h
|
||||
exact of_decide_eq_true h
|
||||
|
||||
@[inline] def hasTarget (self : BuildKey) : Bool :=
|
||||
self.target? ≠ none
|
||||
|
||||
@[simp] theorem hasTarget_mk : BuildKey.hasTarget ⟨x, some t, f⟩ := by
|
||||
simp [BuildKey.hasTarget]
|
||||
|
||||
@[inline] def target (self : BuildKey) (h : self.hasTarget) : WfName :=
|
||||
match mh:self.target? with
|
||||
| some n => n
|
||||
| none => absurd mh <| by
|
||||
unfold hasTarget at h
|
||||
exact of_decide_eq_true h
|
||||
|
||||
@[inline] def isModuleKey (self : BuildKey) : Bool :=
|
||||
self.package? = none ∧ self.hasTarget
|
||||
|
||||
@[simp] theorem isModuleKey_mk : BuildKey.isModuleKey ⟨none, some m, f⟩ := by
|
||||
simp [BuildKey.isModuleKey]
|
||||
|
||||
@[simp] theorem not_isModuleKey_pkg : ¬BuildKey.isModuleKey ⟨some pkg, x, f⟩ := by
|
||||
simp [BuildKey.isModuleKey]
|
||||
|
||||
@[inline] def module (self : BuildKey) (h : self.isModuleKey) : WfName :=
|
||||
self.target <| by
|
||||
unfold isModuleKey at h
|
||||
exact of_decide_eq_true h |>.2
|
||||
|
||||
@[inline] def isPackageKey (self : BuildKey) : Bool :=
|
||||
self.hasPackage ∧ self.target? = none
|
||||
|
||||
@[simp] theorem isPackageKey_mk : BuildKey.isPackageKey ⟨some p, none, f⟩ := by
|
||||
simp [BuildKey.isPackageKey]
|
||||
|
||||
@[inline] def isTargetKey (self : BuildKey) : Bool :=
|
||||
self.hasPackage ∧ self.hasTarget
|
||||
|
||||
@[simp] theorem isTargetKey_mk : BuildKey.isTargetKey ⟨some p, some t, f⟩ := by
|
||||
simp [BuildKey.isTargetKey]
|
||||
|
||||
protected def toString : (self : BuildKey) → String
|
||||
| ⟨some p, none, f⟩ => s!"@{p}:{f}"
|
||||
| ⟨none, some m, f⟩ => s!"+{m}:{f}"
|
||||
| ⟨some p, some t, f⟩ => s!"{p}/{t}:{f}"
|
||||
| ⟨none, none, f⟩ => s!":{f}"
|
||||
|
||||
instance : ToString BuildKey := ⟨(·.toString)⟩
|
||||
|
||||
def quickCmp (k k' : BuildKey) :=
|
||||
match Option.compareWith WfName.quickCmp k.package? k'.package? with
|
||||
| .eq =>
|
||||
match Option.compareWith WfName.quickCmp k.target? k'.target? with
|
||||
| .eq => k.facet.quickCmp k'.facet
|
||||
| ord => ord
|
||||
| ord => ord
|
||||
|
||||
theorem eq_of_quickCmp :
|
||||
{k k' : _} → quickCmp k k' = Ordering.eq → k = k' := by
|
||||
intro ⟨p, t, f⟩ ⟨p', t', f'⟩
|
||||
unfold quickCmp
|
||||
simp only []
|
||||
split
|
||||
next p_eq =>
|
||||
split
|
||||
next t_eq =>
|
||||
intro f_eq
|
||||
have p_eq := eq_of_cmp p_eq
|
||||
have t_eq := eq_of_cmp t_eq
|
||||
have f_eq := eq_of_cmp f_eq
|
||||
simp only [p_eq, t_eq, f_eq]
|
||||
next =>
|
||||
intros; contradiction
|
||||
next =>
|
||||
intros; contradiction
|
||||
|
||||
instance : EqOfCmp BuildKey quickCmp where
|
||||
eq_of_cmp := eq_of_quickCmp
|
||||
|
||||
end BuildKey
|
||||
|
||||
-- ## Subtypes
|
||||
|
||||
/-- The type of build keys for modules. -/
|
||||
structure ModuleBuildKey (fixedFacet : WfName) extends BuildKey where
|
||||
is_module_key : toBuildKey.isModuleKey = true
|
||||
facet_eq_fixed : toBuildKey.facet = fixedFacet
|
||||
|
||||
instance : Coe (ModuleBuildKey f) BuildKey := ⟨(·.toBuildKey)⟩
|
||||
|
||||
@[inline] def BuildKey.toModuleKey
|
||||
(self : BuildKey) (h : self.isModuleKey) : ModuleBuildKey self.facet :=
|
||||
⟨self, h, rfl⟩
|
||||
|
||||
@[inline] def ModuleBuildKey.module (self : ModuleBuildKey f) : WfName :=
|
||||
self.toBuildKey.module self.is_module_key
|
||||
|
||||
/-- The type of build keys for packages. -/
|
||||
structure PackageBuildKey (fixedFacet : WfName) extends BuildKey where
|
||||
is_package_key : toBuildKey.isPackageKey = true
|
||||
facet_eq_fixed : toBuildKey.facet = fixedFacet
|
||||
|
||||
instance : Coe (PackageBuildKey f) BuildKey := ⟨(·.toBuildKey)⟩
|
||||
|
||||
@[inline] def BuildKey.toPackageKey
|
||||
(self : BuildKey) (h : self.isPackageKey) : PackageBuildKey self.facet :=
|
||||
⟨self, h, rfl⟩
|
||||
|
||||
@[inline] def PackageBuildKey.package (self : PackageBuildKey f) : WfName :=
|
||||
self.toBuildKey.package <| by
|
||||
have h := self.is_package_key
|
||||
unfold BuildKey.isPackageKey at h
|
||||
exact (of_decide_eq_true h).1
|
||||
|
|
@ -1,16 +1,40 @@
|
|||
/-
|
||||
Copyright (c) 2021 Mac Malone. All rights reserved.
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lake.Build.Package
|
||||
import Lake.Build.Targets
|
||||
import Lake.Build.Module
|
||||
|
||||
open Std System
|
||||
open Lean (Name NameMap)
|
||||
open Lean hiding SearchPath
|
||||
|
||||
namespace Lake
|
||||
|
||||
-- # Build Package Lean Lib
|
||||
|
||||
def Package.getLibModuleArray (lib : LeanLibConfig) (self : Package) : IO (Array Module) := do
|
||||
return (← lib.getModuleArray self.srcDir).map (⟨self, WfName.ofName ·⟩)
|
||||
|
||||
/--
|
||||
Build the `extraDepTarget` of a package and its (transitive) dependencies
|
||||
and then build the target `facet` of library's modules recursively, constructing
|
||||
a single opaque target for the whole build.
|
||||
-/
|
||||
def Package.buildLibModules
|
||||
(self : Package) (lib : LeanLibConfig) (facet : WfName)
|
||||
[DynamicType ModuleData facet (ActiveBuildTarget α)] : SchedulerM Job := do
|
||||
let buildMods : BuildM _ := do
|
||||
let mods ← self.getLibModuleArray lib
|
||||
let modTargets ← buildModuleFacetArray mods facet
|
||||
(·.task) <$> ActiveTarget.collectOpaqueArray modTargets
|
||||
buildMods.catchFailure fun _ => pure <| failure
|
||||
|
||||
def Package.mkLibTarget (self : Package) (lib : LeanLibConfig) : OpaqueTarget :=
|
||||
Target.opaque <| self.buildLibModules lib &`lean
|
||||
|
||||
def Package.libTarget (self : Package) : OpaqueTarget :=
|
||||
self.mkLibTarget self.builtinLibConfig
|
||||
|
||||
-- # Build Package Static Lib
|
||||
|
||||
def Package.localTargetsOf (map : NameMap (ActiveBuildTarget α)) (self : Package) : Array (BuildTarget α) :=
|
||||
|
|
@ -52,24 +76,3 @@ def Package.mkSharedLibTarget (self : Package) (lib : LeanLibConfig) : FileTarge
|
|||
|
||||
protected def Package.sharedLibTarget (self : Package) : FileTarget :=
|
||||
self.mkSharedLibTarget self.builtinLibConfig
|
||||
|
||||
-- # Build Package Bin
|
||||
|
||||
def Package.mkExeTarget (self : Package) (exe : LeanExeConfig) : FileTarget :=
|
||||
let exeFile := self.binDir / exe.fileName
|
||||
BuildTarget.mk' exeFile do
|
||||
let root : Module := ⟨self, WfName.ofName exe.root⟩
|
||||
let cTargetMap ← buildModuleFacetMap #[root] &`lean.c
|
||||
let pkgLinkTargets ← self.linkTargetsOf cTargetMap
|
||||
let linkTargets :=
|
||||
if self.isLocalModule exe.root then
|
||||
pkgLinkTargets
|
||||
else
|
||||
let rootTarget := cTargetMap.find? root.name |>.get!
|
||||
let rootLinkTarget := root.mkOTarget <| Target.active rootTarget
|
||||
#[rootLinkTarget] ++ pkgLinkTargets
|
||||
let target := leanExeTarget exeFile linkTargets exe.linkArgs
|
||||
target.materializeAsync
|
||||
|
||||
protected def Package.exeTarget (self : Package) : FileTarget :=
|
||||
self.mkExeTarget self.builtinExeConfig
|
||||
|
|
@ -1,536 +1,19 @@
|
|||
|
||||
/-
|
||||
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Ullrich, Mac Malone
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lake.Util.EStateT
|
||||
import Lean.Elab.Import
|
||||
import Lake.Build.Target
|
||||
import Lake.Build.Actions
|
||||
import Lake.Build.Recursive
|
||||
import Lake.Build.Targets
|
||||
import Lake.Config.Module
|
||||
|
||||
open Std System
|
||||
open Lean hiding SearchPath
|
||||
import Lake.Build.Index
|
||||
|
||||
open Std Lean
|
||||
namespace Lake
|
||||
|
||||
abbrev ModuleSet := RBTree Module (·.name.quickCmp ·.name)
|
||||
@[inline] def ModuleSet.empty : ModuleSet := RBTree.empty
|
||||
|
||||
abbrev ModuleMap (α) := RBMap Module α (·.name.quickCmp ·.name)
|
||||
@[inline] def ModuleMap.empty : ModuleMap α := RBMap.empty
|
||||
|
||||
-- # Dynamic Data
|
||||
|
||||
class DynamicType {α : Type u} (Δ : α → Type v) (a : α) (β : outParam $ Type v) : Prop where
|
||||
eq_dynamic_type : Δ a = β
|
||||
|
||||
export DynamicType (eq_dynamic_type)
|
||||
|
||||
@[inline] def toDynamic (a : α) [DynamicType Δ a β] (b : β) : Δ a :=
|
||||
cast eq_dynamic_type.symm b
|
||||
|
||||
@[inline] def ofDynamic (a : α) [DynamicType Δ a β] (b : Δ a) : β :=
|
||||
cast eq_dynamic_type b
|
||||
|
||||
/--
|
||||
The syntax:
|
||||
|
||||
```lean
|
||||
dynamic_data foo : Data 0 := Nat
|
||||
```
|
||||
|
||||
Declares a new alternative for the dynamic `Data` type via the
|
||||
production of an axiom `foo : Data 0 = Nat` and an instance of `DynamicType`
|
||||
that uses this axiom for key `0`.
|
||||
-/
|
||||
scoped macro (name := dynamicDataDecl) doc?:optional(Parser.Command.docComment)
|
||||
"dynamic_data " id:ident " : " dty:ident key:term " := " ty:term : command => do
|
||||
let tid := extractMacroScopes dty.getId |>.name
|
||||
if let (tid, _) :: _ ← Macro.resolveGlobalName tid then
|
||||
let app := Syntax.mkApp dty #[key]
|
||||
let axm := mkIdentFrom dty <| `_root_ ++ tid ++ id.getId
|
||||
`($[$doc?]? @[simp] axiom $axm : $app = $ty
|
||||
instance : DynamicType $dty $key $ty := ⟨$axm⟩)
|
||||
else
|
||||
Macro.throwErrorAt dty s!"unknown identifier '{tid}'"
|
||||
|
||||
@[inline] instance [MonadDStore κ β m] [t : DynamicType β k α] : MonadStore1 k α m where
|
||||
fetch? := cast (by rw [t.eq_dynamic_type]) <| fetch? (m := m) k
|
||||
store a := store k <| cast t.eq_dynamic_type.symm a
|
||||
|
||||
-- # Build Key
|
||||
|
||||
/-- The type of keys in the Lake build store. -/
|
||||
structure BuildKey where
|
||||
package? : Option WfName
|
||||
target? : Option WfName
|
||||
facet : WfName
|
||||
deriving Inhabited, Repr, DecidableEq, Hashable
|
||||
|
||||
namespace BuildKey
|
||||
|
||||
@[inline] def hasPackage (self : BuildKey) : Bool :=
|
||||
self.package? ≠ none
|
||||
|
||||
@[simp] theorem hasPackage_mk : BuildKey.hasPackage ⟨some p, x, f⟩ := by
|
||||
simp [BuildKey.hasPackage]
|
||||
|
||||
@[inline] def package (self : BuildKey) (h : self.hasPackage) : WfName :=
|
||||
match mh:self.package? with
|
||||
| some n => n
|
||||
| none => absurd mh <| by
|
||||
unfold hasPackage at h
|
||||
exact of_decide_eq_true h
|
||||
|
||||
@[inline] def hasTarget (self : BuildKey) : Bool :=
|
||||
self.target? ≠ none
|
||||
|
||||
@[simp] theorem hasTarget_mk : BuildKey.hasTarget ⟨x, some t, f⟩ := by
|
||||
simp [BuildKey.hasTarget]
|
||||
|
||||
@[inline] def target (self : BuildKey) (h : self.hasTarget) : WfName :=
|
||||
match mh:self.target? with
|
||||
| some n => n
|
||||
| none => absurd mh <| by
|
||||
unfold hasTarget at h
|
||||
exact of_decide_eq_true h
|
||||
|
||||
@[inline] def isModuleKey (self : BuildKey) : Bool :=
|
||||
self.package? = none ∧ self.hasTarget
|
||||
|
||||
@[simp] theorem isModuleKey_mk : BuildKey.isModuleKey ⟨none, some m, f⟩ := by
|
||||
simp [BuildKey.isModuleKey]
|
||||
|
||||
@[simp] theorem not_isModuleKey_pkg : ¬BuildKey.isModuleKey ⟨some pkg, x, f⟩ := by
|
||||
simp [BuildKey.isModuleKey]
|
||||
|
||||
@[inline] def module (self : BuildKey) (h : self.isModuleKey) : WfName :=
|
||||
self.target <| by
|
||||
unfold isModuleKey at h
|
||||
exact of_decide_eq_true h |>.2
|
||||
|
||||
@[inline] def isPackageKey (self : BuildKey) : Bool :=
|
||||
self.hasPackage ∧ self.target? = none
|
||||
|
||||
@[simp] theorem isPackageKey_mk : BuildKey.isPackageKey ⟨some p, none, f⟩ := by
|
||||
simp [BuildKey.isPackageKey]
|
||||
|
||||
@[inline] def isTargetKey (self : BuildKey) : Bool :=
|
||||
self.hasPackage ∧ self.hasTarget
|
||||
|
||||
@[simp] theorem isTargetKey_mk : BuildKey.isTargetKey ⟨some p, some t, f⟩ := by
|
||||
simp [BuildKey.isTargetKey]
|
||||
|
||||
protected def toString : (self : BuildKey) → String
|
||||
| ⟨some p, none, f⟩ => s!"@{p}:{f}"
|
||||
| ⟨none, some m, f⟩ => s!"+{m}:{f}"
|
||||
| ⟨some p, some t, f⟩ => s!"{p}/{t}:{f}"
|
||||
| ⟨none, none, f⟩ => s!":{f}"
|
||||
|
||||
instance : ToString BuildKey := ⟨(·.toString)⟩
|
||||
|
||||
def quickCmp (k k' : BuildKey) :=
|
||||
match Option.compareWith WfName.quickCmp k.package? k'.package? with
|
||||
| .eq =>
|
||||
match Option.compareWith WfName.quickCmp k.target? k'.target? with
|
||||
| .eq => k.facet.quickCmp k'.facet
|
||||
| ord => ord
|
||||
| ord => ord
|
||||
|
||||
theorem eq_of_quickCmp :
|
||||
{k k' : _} → quickCmp k k' = Ordering.eq → k = k' := by
|
||||
intro ⟨p, t, f⟩ ⟨p', t', f'⟩
|
||||
unfold quickCmp
|
||||
simp only []
|
||||
split
|
||||
next p_eq =>
|
||||
split
|
||||
next t_eq =>
|
||||
intro f_eq
|
||||
have p_eq := eq_of_cmp p_eq
|
||||
have t_eq := eq_of_cmp t_eq
|
||||
have f_eq := eq_of_cmp f_eq
|
||||
simp only [p_eq, t_eq, f_eq]
|
||||
next =>
|
||||
intros; contradiction
|
||||
next =>
|
||||
intros; contradiction
|
||||
|
||||
instance : EqOfCmp BuildKey quickCmp where
|
||||
eq_of_cmp := eq_of_quickCmp
|
||||
|
||||
end BuildKey
|
||||
|
||||
-- ## Subtypes
|
||||
|
||||
/-- The type of build keys for modules. -/
|
||||
structure ModuleBuildKey (fixedFacet : WfName) extends BuildKey where
|
||||
is_module_key : toBuildKey.isModuleKey = true
|
||||
facet_eq_fixed : toBuildKey.facet = fixedFacet
|
||||
|
||||
instance : Coe (ModuleBuildKey f) BuildKey := ⟨(·.toBuildKey)⟩
|
||||
|
||||
@[inline] def BuildKey.toModuleKey
|
||||
(self : BuildKey) (h : self.isModuleKey) : ModuleBuildKey self.facet :=
|
||||
⟨self, h, rfl⟩
|
||||
|
||||
@[inline] def ModuleBuildKey.module (self : ModuleBuildKey f) : WfName :=
|
||||
self.toBuildKey.module self.is_module_key
|
||||
|
||||
/-- The type of build keys for packages. -/
|
||||
structure PackageBuildKey (fixedFacet : WfName) extends BuildKey where
|
||||
is_package_key : toBuildKey.isPackageKey = true
|
||||
facet_eq_fixed : toBuildKey.facet = fixedFacet
|
||||
|
||||
instance : Coe (PackageBuildKey f) BuildKey := ⟨(·.toBuildKey)⟩
|
||||
|
||||
@[inline] def BuildKey.toPackageKey
|
||||
(self : BuildKey) (h : self.isPackageKey) : PackageBuildKey self.facet :=
|
||||
⟨self, h, rfl⟩
|
||||
|
||||
@[inline] def PackageBuildKey.package (self : PackageBuildKey f) : WfName :=
|
||||
self.toBuildKey.package <| by
|
||||
have h := self.is_package_key
|
||||
unfold BuildKey.isPackageKey at h
|
||||
exact (of_decide_eq_true h).1
|
||||
|
||||
-- ## Constructor Helpers
|
||||
|
||||
@[inline] def Module.mkBuildKey (facet : WfName) (self : Module) : ModuleBuildKey facet :=
|
||||
⟨⟨none, self.name, facet⟩, rfl, rfl⟩
|
||||
|
||||
@[inline] def Package.mkBuildKey (facet : WfName) (self : Package) : PackageBuildKey facet :=
|
||||
⟨⟨self.name, none, facet⟩, rfl, rfl⟩
|
||||
|
||||
-- # Build Data
|
||||
|
||||
/--
|
||||
Build data associated with module facets in the Lake build store.
|
||||
For example a transitive × direct import pair for `imports` or an
|
||||
active build target for `lean.c`.
|
||||
|
||||
It is a dynamic type, meaning additional alternatives can be add lazily
|
||||
as needed.
|
||||
-/
|
||||
opaque ModuleData (facet : WfName) : Type
|
||||
|
||||
/-- Build data associated with package facets (e.g., `extraDep`). -/
|
||||
opaque PackageData (facet : WfName) : Type
|
||||
|
||||
/-- Build data associated with Lake targets (e.g., `extern_lib`). -/
|
||||
opaque TargetData (key : BuildKey) : Type
|
||||
|
||||
/--
|
||||
The build data associated with the given key in the Lake build store.
|
||||
It is dynamic type composed of the three separate dynamic types for modules,
|
||||
packages, and targets.
|
||||
-/
|
||||
def BuildData (key : BuildKey) :=
|
||||
if key.isModuleKey then
|
||||
ModuleData key.facet
|
||||
else if key.isPackageKey then
|
||||
PackageData key.facet
|
||||
else
|
||||
TargetData key
|
||||
|
||||
/-- Macro for declaring new `PackageData`. -/
|
||||
scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment)
|
||||
"package_data " id:ident " : " ty:term : command => do
|
||||
let dty := mkCIdentFrom (← getRef) ``PackageData
|
||||
let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
|
||||
`($[$doc?]? dynamic_data $id : $dty $key := $ty)
|
||||
|
||||
/-- Macro for declaring new `ModuleData`. -/
|
||||
scoped macro (name := moduleDataDecl) doc?:optional(Parser.Command.docComment)
|
||||
"module_data " id:ident " : " ty:term : command => do
|
||||
let dty := mkCIdentFrom (← getRef) ``ModuleData
|
||||
let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
|
||||
`($[$doc?]? dynamic_data $id : $dty $key := $ty)
|
||||
|
||||
/-- Lean binary build (`olean`, `ilean` files) -/
|
||||
module_data lean : ActiveOpaqueTarget
|
||||
|
||||
/-- The `olean` file produced by `lean` -/
|
||||
module_data olean : ActiveOpaqueTarget
|
||||
|
||||
/-- The `ilean` file produced by `lean` -/
|
||||
module_data ilean : ActiveOpaqueTarget
|
||||
|
||||
/-- The C file built from the Lean file via `lean` -/
|
||||
module_data lean.c : ActiveFileTarget
|
||||
|
||||
/-- The object file built from `lean.c` -/
|
||||
module_data lean.o : ActiveFileTarget
|
||||
|
||||
/-- Shared library for `--load-dynlib` -/
|
||||
module_data lean.dynlib : ActiveFileTarget
|
||||
|
||||
/-- The direct × transitive imports of the Lean module. -/
|
||||
module_data lean.imports : Array Module × Array Module
|
||||
|
||||
/-- The package's `extraDepTarget`. -/
|
||||
package_data extraDep : ActiveOpaqueTarget
|
||||
|
||||
-- # Build Store
|
||||
|
||||
/-- A monad equipped with a Lake build store. -/
|
||||
abbrev MonadBuildStore (m) := MonadDStore BuildKey BuildData m
|
||||
|
||||
instance (k : ModuleBuildKey f)
|
||||
[t : DynamicType ModuleData f α] : DynamicType BuildData k α where
|
||||
eq_dynamic_type := by
|
||||
unfold BuildData
|
||||
simp [k.is_module_key, k.facet_eq_fixed, t.eq_dynamic_type]
|
||||
|
||||
@[inline] instance [MonadBuildStore m]
|
||||
[DynamicType ModuleData f α] : MonadStore (ModuleBuildKey f) α m where
|
||||
fetch? k := fetch? k.toBuildKey
|
||||
store k a := store k.toBuildKey a
|
||||
|
||||
instance (k : PackageBuildKey f)
|
||||
[t : DynamicType PackageData f α] : DynamicType BuildData k α where
|
||||
eq_dynamic_type := by
|
||||
unfold BuildData, BuildKey.isModuleKey
|
||||
have has_pkg := of_decide_eq_true (of_decide_eq_true k.is_package_key |>.1)
|
||||
simp [has_pkg, k.is_package_key, k.facet_eq_fixed, t.eq_dynamic_type]
|
||||
|
||||
@[inline] instance [MonadBuildStore m]
|
||||
[DynamicType PackageData f α] : MonadStore (PackageBuildKey f) α m where
|
||||
fetch? k := fetch? k.toBuildKey
|
||||
store k a := store k.toBuildKey a
|
||||
|
||||
-- # Build Info
|
||||
|
||||
inductive BuildInfo
|
||||
| module (module : Module) (facet : WfName)
|
||||
| package (package : Package) (facet : WfName)
|
||||
| externLib (package : Package) (externLib : ExternLibConfig)
|
||||
| target (package : Package) (target : WfName) (facet : WfName)
|
||||
|
||||
def BuildInfo.key : (self : BuildInfo) → BuildKey
|
||||
| module m f => ⟨none, m.name, f⟩
|
||||
| package p f => ⟨p.name, none, f⟩
|
||||
| externLib p e => ⟨p.name, WfName.ofName e.name, &`externLib⟩
|
||||
| target p t f => ⟨p.name, t, f⟩
|
||||
|
||||
-- # Build Index
|
||||
|
||||
/-- A build function for a single element of the Lake build index. -/
|
||||
abbrev IndexBuild (m) :=
|
||||
DBuild BuildInfo (BuildData ·.key) m
|
||||
|
||||
/-- A recursive build function for the Lake build index. -/
|
||||
abbrev RecIndexBuild (m) :=
|
||||
DRecBuild BuildInfo (BuildData ·.key) m
|
||||
|
||||
@[inline] def mkModuleBuild {facet : WfName} (build : Module → IndexBuild m → m α)
|
||||
[h : DynamicType ModuleData facet α] : Module → IndexBuild m → m (ModuleData facet) :=
|
||||
cast (by rw [← h.eq_dynamic_type]) build
|
||||
|
||||
@[inline] def recBuildModuleFacet {m : Type → Type v}
|
||||
(mod : Module) (facet : WfName) [DynamicType ModuleData facet α]
|
||||
(build : (info : BuildInfo) → m (BuildData info.key)) : m α :=
|
||||
let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
|
||||
cast to_data <| build <| BuildInfo.module mod facet
|
||||
|
||||
@[inline] def mkPackageBuild {facet : WfName} (build : Package → IndexBuild m → m α)
|
||||
[h : DynamicType PackageData facet α] : Package → IndexBuild m → m (PackageData facet) :=
|
||||
cast (by rw [← h.eq_dynamic_type]) build
|
||||
|
||||
@[inline] def recBuildPackageFacet {m : Type → Type v}
|
||||
(pkg : Package) (facet : WfName) [DynamicType PackageData facet α]
|
||||
(build : (info : BuildInfo) → m (BuildData info.key)) : m α :=
|
||||
let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type]
|
||||
cast to_data <| build <| BuildInfo.package pkg facet
|
||||
|
||||
abbrev ModuleBuildMap (m : Type → Type v) :=
|
||||
DRBMap WfName (cmp := WfName.quickCmp) fun k =>
|
||||
Module → IndexBuild m → m (ModuleData k)
|
||||
|
||||
@[inline] def ModuleBuildMap.empty : ModuleBuildMap m := DRBMap.empty
|
||||
|
||||
abbrev PackageBuildMap (m : Type → Type v) :=
|
||||
DRBMap WfName (cmp := WfName.quickCmp) fun k =>
|
||||
Package → IndexBuild m → m (PackageData k)
|
||||
|
||||
@[inline] def PackageBuildMap.empty : PackageBuildMap m := DRBMap.empty
|
||||
|
||||
-- # Solo Module Targets
|
||||
|
||||
def Module.soloTarget (mod : Module)
|
||||
(dynlibs : Array FilePath) (depTarget : BuildTarget x) (c := true) : OpaqueTarget :=
|
||||
Target.opaque <| depTarget.bindOpaqueSync fun depTrace => do
|
||||
let argTrace : BuildTrace := pureHash mod.leanArgs
|
||||
let srcTrace : BuildTrace ← computeTrace mod.leanFile
|
||||
let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace
|
||||
let modUpToDate ← modTrace.checkAgainstFile mod mod.traceFile
|
||||
if c then
|
||||
let cUpToDate ← modTrace.checkAgainstFile mod.cFile mod.cTraceFile
|
||||
unless modUpToDate && cUpToDate do
|
||||
compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
|
||||
(← getOleanPath) mod.pkg.rootDir dynlibs mod.leanArgs (← getLean)
|
||||
modTrace.writeToFile mod.cTraceFile
|
||||
else
|
||||
unless modUpToDate do
|
||||
compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile none
|
||||
(← getOleanPath) mod.pkg.rootDir dynlibs mod.leanArgs (← getLean)
|
||||
modTrace.writeToFile mod.traceFile
|
||||
return depTrace
|
||||
|
||||
def Module.mkCTarget (modTarget : BuildTarget x) (self : Module) : FileTarget :=
|
||||
Target.mk self.cFile <| modTarget.bindOpaqueSync fun _ =>
|
||||
return mixTrace (← computeTrace self.cFile) (← getLeanTrace)
|
||||
|
||||
@[inline]
|
||||
def Module.mkOTarget (cTarget : FileTarget) (self : Module) : FileTarget :=
|
||||
leanOFileTarget self.oFile cTarget self.leancArgs
|
||||
|
||||
@[inline]
|
||||
def Module.mkDynlibTarget (linkTargets : Array FileTarget) (self : Module) : FileTarget :=
|
||||
leanSharedLibTarget self.dynlib linkTargets self.linkArgs
|
||||
|
||||
-- # Recursive Building
|
||||
-- # Index Recursive Build
|
||||
|
||||
section
|
||||
variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
|
||||
|
||||
/--
|
||||
Recursively build a module and its (transitive, local) imports,
|
||||
optionally outputting a `.c` file as well if `c` is set to `true`.
|
||||
-/
|
||||
@[specialize] def Module.recBuildLeanModule (mod : Module) (c : Bool)
|
||||
(recurse : IndexBuild m) : m ActiveOpaqueTarget := do
|
||||
have : MonadLift BuildM m := ⟨liftM⟩
|
||||
let extraDepTarget ← recBuildPackageFacet mod.pkg &`extraDep recurse
|
||||
let (imports, transImports) ← recBuildModuleFacet mod &`lean.imports recurse
|
||||
let dynlibsTarget ←
|
||||
if mod.shouldPrecompile then
|
||||
ActiveTarget.collectArray
|
||||
<| ← transImports.mapM (recBuildModuleFacet · &`lean.dynlib recurse)
|
||||
else
|
||||
pure <| ActiveTarget.nil.withInfo #[]
|
||||
let importTarget ←
|
||||
if c then
|
||||
ActiveTarget.collectOpaqueArray
|
||||
<| ← imports.mapM (recBuildModuleFacet · &`lean.c recurse)
|
||||
else
|
||||
ActiveTarget.collectOpaqueArray
|
||||
<| ← imports.mapM (recBuildModuleFacet · &`lean recurse)
|
||||
let depTarget := Target.active <| ← extraDepTarget.mixOpaqueAsync
|
||||
<| ← dynlibsTarget.mixOpaqueAsync importTarget
|
||||
let modTarget ← mod.soloTarget dynlibsTarget.info depTarget c |>.activate
|
||||
store (mod.mkBuildKey &`lean) modTarget
|
||||
store (mod.mkBuildKey &`olean) modTarget
|
||||
store (mod.mkBuildKey &`ilean) modTarget
|
||||
if c then
|
||||
let cTarget ← mod.mkCTarget (Target.active modTarget) |>.activate
|
||||
store (mod.mkBuildKey &`lean.c) cTarget
|
||||
return cTarget.withoutInfo
|
||||
else
|
||||
return modTarget
|
||||
|
||||
/--
|
||||
A module facet name to build function map that contains builders for
|
||||
the initial set of Lake module facets (e.g., `lean.{imports, c, o, dynlib]`).
|
||||
-/
|
||||
@[specialize] def moduleBuildMap : ModuleBuildMap m :=
|
||||
have : MonadLift BuildM m := ⟨liftM⟩
|
||||
ModuleBuildMap.empty.insert
|
||||
-- Compute unique imports (direct × transitive)
|
||||
&`lean.imports (mkModuleBuild <| fun mod recurse => do
|
||||
let contents ← IO.FS.readFile mod.leanFile
|
||||
let (imports, _, _) ← Elab.parseImports contents mod.leanFile.toString
|
||||
let importSet ← imports.foldlM (init := ModuleSet.empty) fun a imp => do
|
||||
if let some mod ← findModule? imp.module then return a.insert mod else return a
|
||||
let mut imports := #[]
|
||||
let mut transImports := ModuleSet.empty
|
||||
for imp in importSet do
|
||||
let (_, impTransImports) ← recBuildModuleFacet imp &`lean.imports recurse
|
||||
for imp in impTransImports do
|
||||
transImports := transImports.insert imp
|
||||
transImports := transImports.insert imp
|
||||
imports := imports.push imp
|
||||
return (imports, transImports.toArray)
|
||||
) |>.insert
|
||||
-- Build module (`.olean` and `.ilean`)
|
||||
&`lean (mkModuleBuild <| fun mod recurse => do
|
||||
mod.recBuildLeanModule false recurse
|
||||
) |>.insert
|
||||
&`olean (mkModuleBuild <| fun mod recurse => do
|
||||
recBuildModuleFacet mod &`lean recurse
|
||||
) |>.insert
|
||||
&`ilean (mkModuleBuild <| fun mod recurse => do
|
||||
recBuildModuleFacet mod &`lean recurse
|
||||
) |>.insert
|
||||
-- Build module `.c` (and `.olean` and `.ilean`)
|
||||
&`lean.c (mkModuleBuild <| fun mod recurse => do
|
||||
mod.recBuildLeanModule true recurse <&> (·.withInfo mod.cFile)
|
||||
) |>.insert
|
||||
-- Build module `.o`
|
||||
&`lean.o (mkModuleBuild <| fun mod recurse => do
|
||||
let cTarget ← recBuildModuleFacet mod &`lean.c recurse
|
||||
mod.mkOTarget (Target.active cTarget) |>.activate
|
||||
) |>.insert
|
||||
-- Build shared library for `--load-dynlb`
|
||||
&`lean.dynlib (mkModuleBuild <| fun mod recurse => do
|
||||
let oTarget ← recBuildModuleFacet mod &`lean.o recurse
|
||||
let dynlibTargets ←
|
||||
if mod.shouldPrecompile then
|
||||
let (_, transImports) ← recBuildModuleFacet mod &`lean.imports recurse
|
||||
transImports.mapM fun mod => recBuildModuleFacet mod &`lean.dynlib recurse
|
||||
else
|
||||
pure #[]
|
||||
-- TODO: Link in external libraries
|
||||
-- let externLibTargets ← mod.pkg.externLibTargets.mapM (·.activate)
|
||||
-- let linkTargets := #[oTarget] ++ sharedLibTargets ++ externLibTargets |>.map Target.active
|
||||
let linkTargets := #[oTarget] ++ dynlibTargets |>.map Target.active
|
||||
mod.mkDynlibTarget linkTargets |>.activate
|
||||
)
|
||||
|
||||
/--
|
||||
A package facet name to build function map that contains builders for
|
||||
the initial set of Lake package facets (e.g., `extraDep`).
|
||||
-/
|
||||
@[specialize] def packageBuildMap : PackageBuildMap m :=
|
||||
have : MonadLift BuildM m := ⟨liftM⟩
|
||||
PackageBuildMap.empty.insert
|
||||
-- Build the `extraDepTarget` for the package and its transitive dependencies
|
||||
&`extraDep (mkPackageBuild <| fun pkg recurse => do
|
||||
let mut target := ActiveTarget.nil
|
||||
for dep in pkg.dependencies do
|
||||
if let some depPkg ← findPackage? dep.name then
|
||||
let extraDepTarget ← recBuildPackageFacet depPkg &`extraDep recurse
|
||||
target ← target.mixOpaqueAsync extraDepTarget
|
||||
target.mixOpaqueAsync <| ← pkg.extraDepTarget.activate
|
||||
)
|
||||
|
||||
/-- Recursive builder for anything in the Lake build index. -/
|
||||
@[specialize] def recBuildIndex : RecIndexBuild m := fun info recurse => do
|
||||
have : MonadLift BuildM m := ⟨liftM⟩
|
||||
match info with
|
||||
| .module mod facet =>
|
||||
if let some build := moduleBuildMap.find? facet then
|
||||
build mod recurse
|
||||
else
|
||||
error s!"do not know how to build module facet `{facet}`"
|
||||
| .package pkg facet =>
|
||||
if let some build := packageBuildMap.find? facet then
|
||||
build pkg recurse
|
||||
else
|
||||
error s!"do not know how to build package facet `{facet}`"
|
||||
| _ =>
|
||||
error s!"do not know how to build `{info.key}`"
|
||||
|
||||
/--
|
||||
Recursively build the given info using the Lake build index
|
||||
and a topological / suspending scheduler.
|
||||
-/
|
||||
@[specialize] def buildIndexTop (info : BuildInfo) : CycleT BuildKey m (BuildData info.key) :=
|
||||
buildDTop BuildData BuildInfo.key recBuildIndex info
|
||||
|
||||
/--
|
||||
Build the module's specified facet recursively using a topological-based
|
||||
scheduler, storing the results in the monad's store and returning the result
|
||||
|
|
@ -548,36 +31,9 @@ scheduler, storing the results in the monad's store and returning nothing.
|
|||
@[inline] def buildModuleTop' (mod : Module) (facet : WfName) : CycleT BuildKey m PUnit :=
|
||||
discard <| buildIndexTop (m := m) <| BuildInfo.module mod facet
|
||||
|
||||
/--
|
||||
Build the package's specified facet recursively using a topological-based
|
||||
scheduler, storing the results in the monad's store and returning the result
|
||||
of the top-level build.
|
||||
-/
|
||||
@[inline] def buildPackageTop (pkg : Package) (facet : WfName)
|
||||
[h : DynamicType PackageData facet α] : CycleT BuildKey m α :=
|
||||
have of_data := by unfold BuildData, BuildInfo.key; simp [h.eq_dynamic_type]
|
||||
cast of_data <| buildIndexTop (m := m) <| BuildInfo.package pkg facet
|
||||
|
||||
end
|
||||
|
||||
-- ## Build Store
|
||||
|
||||
abbrev BuildStore :=
|
||||
DRBMap BuildKey BuildData BuildKey.quickCmp
|
||||
|
||||
@[inline] def BuildStore.empty : BuildStore := DRBMap.empty
|
||||
|
||||
-- ## Facet Builders
|
||||
|
||||
/--
|
||||
Recursively build the specified facet of the given package,
|
||||
returning the result.
|
||||
-/
|
||||
def buildPackageFacet
|
||||
(pkg : Package) (facet : WfName)
|
||||
[DynamicType PackageData facet α] : BuildM α := do
|
||||
failOnBuildCycle <| ← EStateT.run' BuildStore.empty do
|
||||
buildPackageTop pkg facet
|
||||
-- # Module Facet Builders
|
||||
|
||||
/--
|
||||
Recursively build the specified facet of the given module,
|
||||
|
|
@ -617,3 +73,21 @@ def buildModuleFacetMap
|
|||
simp [h, eq_dynamic_type]
|
||||
res := res.insert (k.module h.1) <| cast of_data v
|
||||
return res
|
||||
|
||||
-- # Module Facet Targets
|
||||
|
||||
def Module.facetTarget (facet : WfName) (self : Module)
|
||||
[DynamicType ModuleData facet (ActiveBuildTarget α)] : OpaqueTarget :=
|
||||
BuildTarget.mk' () do return (← buildModuleFacet self facet).task
|
||||
|
||||
@[inline] def Module.oleanTarget (self : Module) : FileTarget :=
|
||||
self.facetTarget &`lean |>.withInfo self.oleanFile
|
||||
|
||||
@[inline] def Module.ileanTarget (self : Module) : FileTarget :=
|
||||
self.facetTarget &`lean |>.withInfo self.ileanFile
|
||||
|
||||
@[inline] def Module.cTarget (self : Module) : FileTarget :=
|
||||
self.facetTarget &`lean.c |>.withInfo self.cFile
|
||||
|
||||
@[inline] def Module.oTarget (self : Module) : FileTarget :=
|
||||
self.facetTarget &`lean.o |>.withInfo self.oFile
|
||||
|
|
|
|||
134
Lake/Build/Module1.lean
Normal file
134
Lake/Build/Module1.lean
Normal file
|
|
@ -0,0 +1,134 @@
|
|||
/-
|
||||
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Ullrich, Mac Malone
|
||||
-/
|
||||
import Lean.Elab.Import
|
||||
import Lake.Build.Info
|
||||
import Lake.Build.Store
|
||||
import Lake.Build.Targets
|
||||
|
||||
open Std System
|
||||
open Lean hiding SearchPath
|
||||
|
||||
namespace Lake
|
||||
|
||||
abbrev ModuleSet := RBTree Module (·.name.quickCmp ·.name)
|
||||
@[inline] def ModuleSet.empty : ModuleSet := RBTree.empty
|
||||
|
||||
abbrev ModuleMap (α) := RBMap Module α (·.name.quickCmp ·.name)
|
||||
@[inline] def ModuleMap.empty : ModuleMap α := RBMap.empty
|
||||
|
||||
-- # Solo Module Targets
|
||||
|
||||
def Module.soloTarget (mod : Module)
|
||||
(dynlibs : Array FilePath) (depTarget : BuildTarget x) (c := true) : OpaqueTarget :=
|
||||
Target.opaque <| depTarget.bindOpaqueSync fun depTrace => do
|
||||
let argTrace : BuildTrace := pureHash mod.leanArgs
|
||||
let srcTrace : BuildTrace ← computeTrace mod.leanFile
|
||||
let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace
|
||||
let modUpToDate ← modTrace.checkAgainstFile mod mod.traceFile
|
||||
if c then
|
||||
let cUpToDate ← modTrace.checkAgainstFile mod.cFile mod.cTraceFile
|
||||
unless modUpToDate && cUpToDate do
|
||||
compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
|
||||
(← getOleanPath) mod.pkg.rootDir dynlibs mod.leanArgs (← getLean)
|
||||
modTrace.writeToFile mod.cTraceFile
|
||||
else
|
||||
unless modUpToDate do
|
||||
compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile none
|
||||
(← getOleanPath) mod.pkg.rootDir dynlibs mod.leanArgs (← getLean)
|
||||
modTrace.writeToFile mod.traceFile
|
||||
return depTrace
|
||||
|
||||
def Module.mkCTarget (modTarget : BuildTarget x) (self : Module) : FileTarget :=
|
||||
Target.mk self.cFile <| modTarget.bindOpaqueSync fun _ =>
|
||||
return mixTrace (← computeTrace self.cFile) (← getLeanTrace)
|
||||
|
||||
@[inline]
|
||||
def Module.mkOTarget (cTarget : FileTarget) (self : Module) : FileTarget :=
|
||||
leanOFileTarget self.oFile cTarget self.leancArgs
|
||||
|
||||
@[inline]
|
||||
def Module.mkDynlibTarget (linkTargets : Array FileTarget) (self : Module) : FileTarget :=
|
||||
leanSharedLibTarget self.dynlib linkTargets self.linkArgs
|
||||
|
||||
-- # Recursive Building
|
||||
|
||||
section
|
||||
variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
|
||||
|
||||
/--
|
||||
Recursively build a module and its (transitive, local) imports,
|
||||
optionally outputting a `.c` file as well if `c` is set to `true`.
|
||||
-/
|
||||
@[specialize] def Module.recBuildLean (mod : Module) (c : Bool)
|
||||
(recurse : IndexBuildFn m) : m ActiveOpaqueTarget := do
|
||||
have : MonadLift BuildM m := ⟨liftM⟩
|
||||
let extraDepTarget ← mod.pkg.recBuildFacet &`extraDep recurse
|
||||
let (imports, transImports) ← mod.recBuildFacet &`lean.imports recurse
|
||||
let dynlibsTarget ←
|
||||
if mod.shouldPrecompile then
|
||||
ActiveTarget.collectArray
|
||||
<| ← transImports.mapM (·.recBuildFacet &`lean.dynlib recurse)
|
||||
else
|
||||
pure <| ActiveTarget.nil.withInfo #[]
|
||||
let importTarget ←
|
||||
if c then
|
||||
ActiveTarget.collectOpaqueArray
|
||||
<| ← imports.mapM (·.recBuildFacet &`lean.c recurse)
|
||||
else
|
||||
ActiveTarget.collectOpaqueArray
|
||||
<| ← imports.mapM (·.recBuildFacet &`lean recurse)
|
||||
let depTarget := Target.active <| ← extraDepTarget.mixOpaqueAsync
|
||||
<| ← dynlibsTarget.mixOpaqueAsync importTarget
|
||||
let modTarget ← mod.soloTarget dynlibsTarget.info depTarget c |>.activate
|
||||
store (mod.mkBuildKey &`lean) modTarget
|
||||
store (mod.mkBuildKey &`olean) modTarget
|
||||
store (mod.mkBuildKey &`ilean) modTarget
|
||||
if c then
|
||||
let cTarget ← mod.mkCTarget (Target.active modTarget) |>.activate
|
||||
store (mod.mkBuildKey &`lean.c) cTarget
|
||||
return cTarget.withoutInfo
|
||||
else
|
||||
return modTarget
|
||||
|
||||
/--
|
||||
Recursively parse the Lean files of a module and its imports
|
||||
building an `Array` product of its direct and transitive local imports.
|
||||
-/
|
||||
@[specialize] def Module.recParseImports (mod : Module)
|
||||
(recurse : IndexBuildFn m) : m (Array Module × Array Module) := do
|
||||
have : MonadLift BuildM m := ⟨liftM⟩
|
||||
let contents ← IO.FS.readFile mod.leanFile
|
||||
let (imports, _, _) ← Elab.parseImports contents mod.leanFile.toString
|
||||
let importSet ← imports.foldlM (init := ModuleSet.empty) fun a imp => do
|
||||
if let some mod ← findModule? imp.module then return a.insert mod else return a
|
||||
let mut imports := #[]
|
||||
let mut transImports := ModuleSet.empty
|
||||
for imp in importSet do
|
||||
let (_, impTransImports) ← imp.recBuildFacet &`lean.imports recurse
|
||||
for imp in impTransImports do
|
||||
transImports := transImports.insert imp
|
||||
transImports := transImports.insert imp
|
||||
imports := imports.push imp
|
||||
return (imports, transImports.toArray)
|
||||
|
||||
/--
|
||||
Recursively build the shared library of a module (e.g., for `--load-dynlib`).
|
||||
-/
|
||||
@[specialize] def Module.recBuildDynLib (mod : Module)
|
||||
(recurse : IndexBuildFn m) : m ActiveFileTarget := do
|
||||
have : MonadLift BuildM m := ⟨liftM⟩
|
||||
let oTarget ← mod.recBuildFacet &`lean.o recurse
|
||||
let dynlibTargets ←
|
||||
if mod.shouldPrecompile then
|
||||
let (_, transImports) ← mod.recBuildFacet &`lean.imports recurse
|
||||
transImports.mapM fun mod => mod.recBuildFacet &`lean.dynlib recurse
|
||||
else
|
||||
pure #[]
|
||||
-- TODO: Link in external libraries
|
||||
-- let externLibTargets ← mod.pkg.externLibTargets.mapM (·.activate)
|
||||
-- let linkTargets := #[oTarget] ++ sharedLibTargets ++ externLibTargets |>.map Target.active
|
||||
let linkTargets := #[oTarget] ++ dynlibTargets |>.map Target.active
|
||||
mod.mkDynlibTarget linkTargets |>.activate
|
||||
|
|
@ -1,93 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
|
||||
-/
|
||||
import Lake.Build.Module
|
||||
|
||||
open Std System
|
||||
open Lean hiding SearchPath
|
||||
|
||||
namespace Lake
|
||||
|
||||
-- # Build Packages
|
||||
|
||||
-- # Build Package Modules
|
||||
|
||||
|
||||
|
||||
def Package.getLibModuleArray (lib : LeanLibConfig) (self : Package) : IO (Array Module) := do
|
||||
return (← lib.getModuleArray self.srcDir).map (⟨self, WfName.ofName ·⟩)
|
||||
|
||||
/--
|
||||
Build the `extraDepTarget` of a package and its (transitive) dependencies
|
||||
and then build the target `facet` of library's modules recursively, constructing
|
||||
a single opaque target for the whole build.
|
||||
-/
|
||||
def Package.buildLibModules
|
||||
(self : Package) (lib : LeanLibConfig) (facet : WfName)
|
||||
[DynamicType ModuleData facet (ActiveBuildTarget α)] : SchedulerM Job := do
|
||||
let buildMods : BuildM _ := do
|
||||
let mods ← self.getLibModuleArray lib
|
||||
let modTargets ← buildModuleFacetArray mods facet
|
||||
(·.task) <$> ActiveTarget.collectOpaqueArray modTargets
|
||||
buildMods.catchFailure fun _ => pure <| failure
|
||||
|
||||
def Package.mkLibTarget (self : Package) (lib : LeanLibConfig) : OpaqueTarget :=
|
||||
Target.opaque <| self.buildLibModules lib &`lean
|
||||
|
||||
def Package.libTarget (self : Package) : OpaqueTarget :=
|
||||
self.mkLibTarget self.builtinLibConfig
|
||||
|
||||
-- # Build Specific Modules of the Package
|
||||
|
||||
def Module.facetTarget (facet : WfName) (self : Module)
|
||||
[DynamicType ModuleData facet (ActiveBuildTarget α)] : OpaqueTarget :=
|
||||
BuildTarget.mk' () do return (← buildModuleFacet self facet).task
|
||||
|
||||
@[inline] def Module.oleanTarget (self : Module) : FileTarget :=
|
||||
self.facetTarget &`lean |>.withInfo self.oleanFile
|
||||
|
||||
@[inline] def Module.ileanTarget (self : Module) : FileTarget :=
|
||||
self.facetTarget &`lean |>.withInfo self.ileanFile
|
||||
|
||||
@[inline] def Module.cTarget (self : Module) : FileTarget :=
|
||||
self.facetTarget &`lean.c |>.withInfo self.cFile
|
||||
|
||||
@[inline] def Module.oTarget (self : Module) : FileTarget :=
|
||||
self.facetTarget &`lean.o |>.withInfo self.oFile
|
||||
|
||||
-- # Build Imports
|
||||
|
||||
/--
|
||||
Construct an `Array` of `Module`s for the workspace-local modules of
|
||||
a `List` of import strings.
|
||||
-/
|
||||
def Workspace.processImportList
|
||||
(imports : List String) (self : Workspace) : Array Module := Id.run do
|
||||
let mut localImports := #[]
|
||||
for imp in imports do
|
||||
if let some mod := self.findModule? imp.toName then
|
||||
localImports := localImports.push mod
|
||||
return localImports
|
||||
|
||||
/--
|
||||
Build the workspace-local modules of list of imports.
|
||||
|
||||
Build only module `.olean` and `.ilean` files if
|
||||
the default package build does not include any binary targets
|
||||
Otherwise, also build `.c` files.
|
||||
-/
|
||||
def Package.buildImportsAndDeps (imports : List String) (self : Package) : BuildM PUnit := do
|
||||
if imports.isEmpty then
|
||||
-- build the package's (and its dependencies') `extraDepTarget`
|
||||
buildPackageFacet self &`extraDep >>= (·.buildOpaque)
|
||||
else
|
||||
-- build local imports from list
|
||||
let mods := (← getWorkspace).processImportList imports
|
||||
if self.leanExes.isEmpty && self.defaultFacet matches .none | .leanLib | .oleans then
|
||||
let targets ← buildModuleFacetArray mods &`lean
|
||||
targets.forM (·.buildOpaque)
|
||||
else
|
||||
let targets ← buildModuleFacetArray mods &`lean.c
|
||||
targets.forM (·.buildOpaque)
|
||||
|
|
@ -1,101 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Ullrich, Mac Malone
|
||||
-/
|
||||
import Lake.Util.DRBMap
|
||||
|
||||
open Std
|
||||
namespace Lake
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- # Build Store
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
/-- A monad equipped with a dependently typed key-value store for a particular key. -/
|
||||
class MonadStore1 {κ : Type u} (k : κ) (α : outParam $ Type v) (m : Type v → Type w) where
|
||||
fetch? : m (Option α)
|
||||
store : α → m PUnit
|
||||
|
||||
export MonadStore1 (fetch? store)
|
||||
|
||||
/-- A monad equipped with a dependently typed key-object store. -/
|
||||
class MonadDStore (κ : Type u) (β : outParam $ κ → Type v) (m : Type v → Type w) where
|
||||
fetch? : (key : κ) → m (Option (β key))
|
||||
store : (key : κ) → β key → m PUnit
|
||||
|
||||
instance [MonadDStore κ β m] : MonadStore1 k (β k) m where
|
||||
fetch? := MonadDStore.fetch? k
|
||||
store o := MonadDStore.store k o
|
||||
|
||||
/-- A monad equipped with a key-object store. -/
|
||||
abbrev MonadStore κ α m := MonadDStore κ (fun _ => α) m
|
||||
|
||||
instance [MonadLiftT m n] [MonadDStore κ β m] : MonadDStore κ β n where
|
||||
fetch? k := liftM (m := m) <| fetch? k
|
||||
store k a := liftM (m := m) <| store k a
|
||||
|
||||
instance [Monad m] [EqOfCmpWrt κ β cmp] : MonadDStore κ β (StateT (DRBMap κ β cmp) m) where
|
||||
fetch? k := return (← get).find? k
|
||||
store k a := modify (·.insert k a)
|
||||
|
||||
instance [Monad m] : MonadStore κ α (StateT (RBMap κ α cmp) m) where
|
||||
fetch? k := return (← get).find? k
|
||||
store k a := modify (·.insert k a)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- # Topological / Suspending Builder
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- ## Abstractions
|
||||
|
||||
/-- A dependently typed object builder. -/
|
||||
abbrev DBuild.{u,v,w} (ι : Type u) (β : ι → Type v) (m : Type v → Type w) :=
|
||||
(i : ι) → m (β i)
|
||||
|
||||
/-- A dependently typed recursive object builder. -/
|
||||
abbrev DRecBuild.{u,v,w} (ι : Type u) (β : ι → Type v) (m : Type v → Type w) :=
|
||||
(i : ι) → DBuild ι β m → m (β i)
|
||||
|
||||
/-- A recursive object builder. -/
|
||||
abbrev RecBuild ι α m := DRecBuild ι (fun _ => α) m
|
||||
|
||||
/-- `ExceptT` for build cycles. -/
|
||||
abbrev CycleT (κ) :=
|
||||
ExceptT (List κ)
|
||||
|
||||
-- ## Algorithm
|
||||
|
||||
/-- Auxiliary function for `buildTop`. -/
|
||||
@[specialize] partial def buildTopCore [BEq κ] [Monad m] [MonadDStore κ β m]
|
||||
(parents : List κ) (keyOf : ι → κ) (build : DRecBuild ι (β ∘ keyOf) (CycleT κ m))
|
||||
(info : ι) : CycleT κ m (β (keyOf info)) := do
|
||||
let key := keyOf info
|
||||
-- return previous output if already built
|
||||
if let some output ← fetch? key then
|
||||
return output
|
||||
-- detect cyclic builds
|
||||
if parents.contains key then
|
||||
throw <| key :: (parents.partition (· != key)).1 ++ [key]
|
||||
-- build the key recursively
|
||||
let output ← build info <| buildTopCore (key :: parents) keyOf build
|
||||
-- save the output (to prevent repeated builds of the same key)
|
||||
store key output
|
||||
return output
|
||||
|
||||
/-- Dependently typed version of `buildTop`. -/
|
||||
@[inline] def buildDTop (β) [BEq κ] [Monad m] [MonadDStore κ β m]
|
||||
(keyOf : ι → κ) (build : DRecBuild ι (β ∘ keyOf) (CycleT κ m))
|
||||
(info : ι) : CycleT κ m (β (keyOf info)) :=
|
||||
buildTopCore [] keyOf build info
|
||||
|
||||
/--
|
||||
Recursively fills a `MonadStore` of key-object pairs by
|
||||
building objects topologically (ι.e., via a depth-first search with memoization).
|
||||
If a cycle is detected, the list of keys traversed is thrown.
|
||||
|
||||
Called a suspending scheduler in "Build systems à la carte".
|
||||
-/
|
||||
@[inline] def buildTop [BEq κ] [Monad m] [MonadStore κ α m]
|
||||
(keyOf : ι → κ) (build : RecBuild ι α (CycleT κ m)) (info : ι) : CycleT κ m α :=
|
||||
buildDTop (fun _ => α) keyOf build info
|
||||
50
Lake/Build/Store.lean
Normal file
50
Lake/Build/Store.lean
Normal file
|
|
@ -0,0 +1,50 @@
|
|||
/-
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lake.Build.Data
|
||||
import Lake.Build.Topological
|
||||
import Lake.Util.StoreInsts
|
||||
|
||||
/-!
|
||||
# The Lake Build Store
|
||||
|
||||
The Lake build store is the map of Lake build keys to build task and/or
|
||||
build results that is slowly filled during a recursive build (e.g., via
|
||||
topological-based build of an initial key's dependencies).
|
||||
-/
|
||||
|
||||
namespace Lake
|
||||
|
||||
/-- The type of the Lake build store. -/
|
||||
abbrev BuildStore :=
|
||||
DRBMap BuildKey BuildData BuildKey.quickCmp
|
||||
|
||||
@[inline] def BuildStore.empty : BuildStore := DRBMap.empty
|
||||
|
||||
/-- A monad equipped with a Lake build store. -/
|
||||
abbrev MonadBuildStore (m) := MonadDStore BuildKey BuildData m
|
||||
|
||||
instance (k : ModuleBuildKey f)
|
||||
[t : DynamicType ModuleData f α] : DynamicType BuildData k α where
|
||||
eq_dynamic_type := by
|
||||
unfold BuildData
|
||||
simp [k.is_module_key, k.facet_eq_fixed, t.eq_dynamic_type]
|
||||
|
||||
@[inline] instance [MonadBuildStore m]
|
||||
[DynamicType ModuleData f α] : MonadStore (ModuleBuildKey f) α m where
|
||||
fetch? k := fetch? k.toBuildKey
|
||||
store k a := store k.toBuildKey a
|
||||
|
||||
instance (k : PackageBuildKey f)
|
||||
[t : DynamicType PackageData f α] : DynamicType BuildData k α where
|
||||
eq_dynamic_type := by
|
||||
unfold BuildData, BuildKey.isModuleKey
|
||||
have has_pkg := of_decide_eq_true (of_decide_eq_true k.is_package_key |>.1)
|
||||
simp [has_pkg, k.is_package_key, k.facet_eq_fixed, t.eq_dynamic_type]
|
||||
|
||||
@[inline] instance [MonadBuildStore m]
|
||||
[DynamicType PackageData f α] : MonadStore (PackageBuildKey f) α m where
|
||||
fetch? k := fetch? k.toBuildKey
|
||||
store k a := store k.toBuildKey a
|
||||
70
Lake/Build/Topological.lean
Normal file
70
Lake/Build/Topological.lean
Normal file
|
|
@ -0,0 +1,70 @@
|
|||
/-
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lake.Util.Store
|
||||
|
||||
/-!
|
||||
# Topological / Suspending Recursive Builder
|
||||
|
||||
This module defines a recursive build function that topologically
|
||||
(ι.e., via a depth-first search with memoization) builds the elements of
|
||||
a build store.
|
||||
|
||||
This is called a suspending scheduler in *Build systems à la carte*.
|
||||
-/
|
||||
|
||||
open Std
|
||||
namespace Lake
|
||||
|
||||
-- ## Abstractions
|
||||
|
||||
/-- A dependently typed object builder. -/
|
||||
abbrev DBuildFn.{u,v,w} (ι : Type u) (β : ι → Type v) (m : Type v → Type w) :=
|
||||
(i : ι) → m (β i)
|
||||
|
||||
/-- A dependently typed recursive object builder. -/
|
||||
abbrev DRecBuildFn.{u,v,w} (ι : Type u) (β : ι → Type v) (m : Type v → Type w) :=
|
||||
(i : ι) → DBuildFn ι β m → m (β i)
|
||||
|
||||
/-- A recursive object builder. -/
|
||||
abbrev RecBuildFn ι α m := DRecBuildFn ι (fun _ => α) m
|
||||
|
||||
/-- `ExceptT` for build cycles. -/
|
||||
abbrev CycleT (κ) :=
|
||||
ExceptT (List κ)
|
||||
|
||||
-- ## Algorithm
|
||||
|
||||
/-- Auxiliary function for `buildTop`. -/
|
||||
@[specialize] partial def buildTopCore [BEq κ] [Monad m] [MonadDStore κ β m]
|
||||
(parents : List κ) (keyOf : ι → κ) (build : DRecBuildFn ι (β ∘ keyOf) (CycleT κ m))
|
||||
(info : ι) : CycleT κ m (β (keyOf info)) := do
|
||||
let key := keyOf info
|
||||
-- return previous output if already built
|
||||
if let some output ← fetch? key then
|
||||
return output
|
||||
-- detect cyclic builds
|
||||
if parents.contains key then
|
||||
throw <| key :: (parents.partition (· != key)).1 ++ [key]
|
||||
-- build the key recursively
|
||||
let output ← build info <| buildTopCore (key :: parents) keyOf build
|
||||
-- save the output (to prevent repeated builds of the same key)
|
||||
store key output
|
||||
return output
|
||||
|
||||
/-- Dependently typed version of `buildTop`. -/
|
||||
@[inline] def buildDTop (β) [BEq κ] [Monad m] [MonadDStore κ β m]
|
||||
(keyOf : ι → κ) (build : DRecBuildFn ι (β ∘ keyOf) (CycleT κ m))
|
||||
(info : ι) : CycleT κ m (β (keyOf info)) :=
|
||||
buildTopCore [] keyOf build info
|
||||
|
||||
/--
|
||||
Recursively fills a `MonadStore` of key-object pairs by
|
||||
building objects topologically (ι.e., via a depth-first search with memoization).
|
||||
If a cycle is detected, the list of keys traversed is thrown.
|
||||
-/
|
||||
@[inline] def buildTop [BEq κ] [Monad m] [MonadStore κ α m]
|
||||
(keyOf : ι → κ) (build : RecBuildFn ι α (CycleT κ m)) (info : ι) : CycleT κ m α :=
|
||||
buildDTop (fun _ => α) keyOf build info
|
||||
|
|
@ -5,10 +5,11 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
|
|||
-/
|
||||
import Lake.Util.Git
|
||||
import Lake.Util.EStateT
|
||||
import Lake.Util.StoreInsts
|
||||
import Lake.Config.Load
|
||||
import Lake.Config.Manifest
|
||||
import Lake.Config.Workspace
|
||||
import Lake.Build.Recursive
|
||||
import Lake.Build.Topological
|
||||
|
||||
open Std System
|
||||
open Lean (Name NameMap)
|
||||
|
|
|
|||
42
Lake/Util/DynamicType.lean
Normal file
42
Lake/Util/DynamicType.lean
Normal file
|
|
@ -0,0 +1,42 @@
|
|||
/-
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lean.Parser.Command
|
||||
|
||||
open Lean
|
||||
namespace Lake
|
||||
|
||||
class DynamicType {α : Type u} (Δ : α → Type v) (a : α) (β : outParam $ Type v) : Prop where
|
||||
eq_dynamic_type : Δ a = β
|
||||
|
||||
export DynamicType (eq_dynamic_type)
|
||||
|
||||
@[inline] def toDynamic (a : α) [DynamicType Δ a β] (b : β) : Δ a :=
|
||||
cast eq_dynamic_type.symm b
|
||||
|
||||
@[inline] def ofDynamic (a : α) [DynamicType Δ a β] (b : Δ a) : β :=
|
||||
cast eq_dynamic_type b
|
||||
|
||||
/--
|
||||
The syntax:
|
||||
|
||||
```lean
|
||||
dynamic_data foo : Data 0 := Nat
|
||||
```
|
||||
|
||||
Declares a new alternative for the dynamic `Data` type via the
|
||||
production of an axiom `foo : Data 0 = Nat` and an instance of `DynamicType`
|
||||
that uses this axiom for key `0`.
|
||||
-/
|
||||
scoped macro (name := dynamicDataDecl) doc?:optional(Parser.Command.docComment)
|
||||
"dynamic_data " id:ident " : " dty:ident key:term " := " ty:term : command => do
|
||||
let tid := extractMacroScopes dty.getId |>.name
|
||||
if let (tid, _) :: _ ← Macro.resolveGlobalName tid then
|
||||
let app := Syntax.mkApp dty #[key]
|
||||
let axm := mkIdentFrom dty <| `_root_ ++ tid ++ id.getId
|
||||
`($[$doc?]? @[simp] axiom $axm : $app = $ty
|
||||
instance : DynamicType $dty $key $ty := ⟨$axm⟩)
|
||||
else
|
||||
Macro.throwErrorAt dty s!"unknown identifier '{tid}'"
|
||||
29
Lake/Util/Store.lean
Normal file
29
Lake/Util/Store.lean
Normal file
|
|
@ -0,0 +1,29 @@
|
|||
/-
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
namespace Lake
|
||||
|
||||
/-- A monad equipped with a dependently typed key-value store for a particular key. -/
|
||||
class MonadStore1 {κ : Type u} (k : κ) (α : outParam $ Type v) (m : Type v → Type w) where
|
||||
fetch? : m (Option α)
|
||||
store : α → m PUnit
|
||||
|
||||
export MonadStore1 (fetch? store)
|
||||
|
||||
/-- A monad equipped with a dependently typed key-object store. -/
|
||||
class MonadDStore (κ : Type u) (β : outParam $ κ → Type v) (m : Type v → Type w) where
|
||||
fetch? : (key : κ) → m (Option (β key))
|
||||
store : (key : κ) → β key → m PUnit
|
||||
|
||||
instance [MonadDStore κ β m] : MonadStore1 k (β k) m where
|
||||
fetch? := MonadDStore.fetch? k
|
||||
store o := MonadDStore.store k o
|
||||
|
||||
/-- A monad equipped with a key-object store. -/
|
||||
abbrev MonadStore κ α m := MonadDStore κ (fun _ => α) m
|
||||
|
||||
instance [MonadLiftT m n] [MonadDStore κ β m] : MonadDStore κ β n where
|
||||
fetch? k := liftM (m := m) <| fetch? k
|
||||
store k a := liftM (m := m) <| store k a
|
||||
23
Lake/Util/StoreInsts.lean
Normal file
23
Lake/Util/StoreInsts.lean
Normal file
|
|
@ -0,0 +1,23 @@
|
|||
/-
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lake.Util.DRBMap
|
||||
import Lake.Util.DynamicType
|
||||
import Lake.Util.Store
|
||||
|
||||
open Std
|
||||
namespace Lake
|
||||
|
||||
instance [Monad m] [EqOfCmpWrt κ β cmp] : MonadDStore κ β (StateT (DRBMap κ β cmp) m) where
|
||||
fetch? k := return (← get).find? k
|
||||
store k a := modify (·.insert k a)
|
||||
|
||||
instance [Monad m] : MonadStore κ α (StateT (RBMap κ α cmp) m) where
|
||||
fetch? k := return (← get).find? k
|
||||
store k a := modify (·.insert k a)
|
||||
|
||||
@[inline] instance [MonadDStore κ β m] [t : DynamicType β k α] : MonadStore1 k α m where
|
||||
fetch? := cast (by rw [t.eq_dynamic_type]) <| fetch? (m := m) k
|
||||
store a := store k <| cast t.eq_dynamic_type.symm a
|
||||
Loading…
Add table
Reference in a new issue