From d68029092ad809cb61d28de828afad9df2a9a1be Mon Sep 17 00:00:00 2001 From: tydeu Date: Sat, 23 Jul 2022 19:39:47 -0400 Subject: [PATCH] refactor: simplify `FacetConifg` and build monads ala leanprover/lake#107 closes leanprover/lake#107 --- Lake/Build.lean | 2 + Lake/Build/Context.lean | 13 ++- Lake/Build/Facets.lean | 31 +++---- Lake/Build/Imports.lean | 1 - Lake/Build/Index.lean | 164 +++++++---------------------------- Lake/Build/IndexTargets.lean | 24 ++--- Lake/Build/Info.lean | 9 +- Lake/Build/Module.lean | 79 ++++++++++++----- Lake/Build/Package.lean | 47 ++++++++++ Lake/Build/Roots.lean | 24 ++--- Lake/CLI/Build.lean | 20 ++--- Lake/Config/FacetConfig.lean | 63 ++++---------- Lake/Config/Opaque.lean | 6 -- Lake/Config/Package.lean | 1 + Lake/Config/Workspace.lean | 18 ++-- Lake/DSL/Facets.lean | 17 +--- Lake/Load/Main.lean | 8 +- 17 files changed, 227 insertions(+), 300 deletions(-) create mode 100644 Lake/Build/Package.lean diff --git a/Lake/Build.lean b/Lake/Build.lean index f536774042..48d1d6c01b 100644 --- a/Lake/Build.lean +++ b/Lake/Build.lean @@ -6,4 +6,6 @@ Authors: Mac Malone import Lake.Build.Monad import Lake.Build.Actions import Lake.Build.IndexTargets +import Lake.Build.Module +import Lake.Build.Package import Lake.Build.Imports diff --git a/Lake/Build/Context.lean b/Lake/Build/Context.lean index 3d4652e96f..febcd65b52 100644 --- a/Lake/Build/Context.lean +++ b/Lake/Build/Context.lean @@ -9,6 +9,8 @@ import Lake.Util.Error import Lake.Util.OptionIO import Lake.Config.Context import Lake.Build.Trace +import Lake.Build.Store +import Lake.Build.Topological open System namespace Lake @@ -29,9 +31,18 @@ abbrev BuildT := ReaderT BuildContext /-- The monad for the Lake build manager. -/ abbrev SchedulerM := BuildT <| LogT BaseIO -/-- The monad for Lake builds. -/ +/-- The core monad for Lake builds. -/ abbrev BuildM := BuildT <| MonadLogT BaseIO OptionIO +/-- A transformer to equip a monad with a Lake build store. -/ +abbrev BuildStoreT := StateT BuildStore + +/-- A transformer for monads that may encounter a build cycle. -/ +abbrev BuildCycleT := CycleT BuildKey + +/-- A recursive build of a Lake build store that may encounter a cycle. -/ +abbrev RecBuildM := BuildCycleT <| BuildStoreT BuildM + instance : MonadError BuildM := ⟨MonadLog.error⟩ instance : MonadLift IO BuildM := ⟨MonadError.runIO⟩ diff --git a/Lake/Build/Facets.lean b/Lake/Build/Facets.lean index b868a2875d..8b164f33a6 100644 --- a/Lake/Build/Facets.lean +++ b/Lake/Build/Facets.lean @@ -11,7 +11,7 @@ import Lake.Build.TargetTypes This module declares most of the builtin facets an targets and their build data builtin facets and targets. Some of these definitions -are needed for configurations, so we define them here before we need to +are needed for configurations, so we define them here before we need to import said configurations for `BuildInfo`. -/ @@ -33,62 +33,59 @@ instance (facet : ModuleFacet α) : FamilyDef ModuleData facet.name α := instance [FamilyDef ModuleData facet α] : CoeDep Name facet (ModuleFacet α) := ⟨facet, family_key_eq_type⟩ -namespace Module -abbrev leanBinFacet := `lean.bin -abbrev oleanFacet := `olean -abbrev ileanFacet := `ilean -abbrev cFacet := `lean.c -abbrev oFacet := `lean.o -abbrev dynlibFacet := `dynlib -end Module - /-- The core compilation / elaboration of the Lean file via `lean`, which produce the Lean binaries of the module (i.e., `olean` and `ilean`). It is thus the facet used by default for building imports of a module. Also, if the module is not lean-only, it produces `c` files as well. -/ +abbrev Module.leanBinFacet := `lean.bin module_data lean.bin : ActiveOpaqueTarget /-- The `olean` file produced by `lean` -/ +abbrev Module.oleanFacet := `olean module_data olean : ActiveFileTarget /-- The `ilean` file produced by `lean` -/ +abbrev Module.ileanFacet := `ilean module_data ilean : ActiveFileTarget /-- The C file built from the Lean file via `lean` -/ +abbrev Module.cFacet := `lean.c module_data lean.c : ActiveFileTarget /-- The object file built from `lean.c` -/ +abbrev Module.oFacet := `lean.o module_data lean.o : ActiveFileTarget /-- Shared library for `--load-dynlib` -/ +abbrev Module.dynlibFacet := `dynlib module_data dynlib : ActiveFileTarget /-! ## Package Facets -/ -/-- The package's `extraDepTarget`. -/ +/-- The package's `extraDepTarget` mixed with its transitive dependencies `extraDepTarget`. -/ +abbrev Package.extraDepFacet := `extraDep package_data extraDep : ActiveOpaqueTarget /-! ## Target Facets -/ -abbrev LeanLib.staticFacet := `leanLib.static -abbrev LeanLib.sharedFacet := `leanLib.shared -abbrev LeanExe.exeFacet := `leanExe -abbrev ExternLib.staticFacet := `externLib.static -abbrev ExternLib.sharedFacet := `externLib.shared - /-- A Lean library's static binary. -/ +abbrev LeanLib.staticFacet := `leanLib.static target_data leanLib.static : ActiveFileTarget /-- A Lean library's shared binary. -/ +abbrev LeanLib.sharedFacet := `leanLib.shared target_data leanLib.shared : ActiveFileTarget /-- A Lean binary executable. -/ +abbrev LeanExe.exeFacet := `leanExe target_data leanExe : ActiveFileTarget /-- A external library's static binary. -/ +abbrev ExternLib.staticFacet := `externLib.static target_data externLib.static : ActiveFileTarget /-- A external library's shared binary. -/ +abbrev ExternLib.sharedFacet := `externLib.shared target_data externLib.shared : ActiveFileTarget diff --git a/Lake/Build/Imports.lean b/Lake/Build/Imports.lean index f049f828d4..a7f0a2cf24 100644 --- a/Lake/Build/Imports.lean +++ b/Lake/Build/Imports.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ import Lake.Build.Index -import Lake.Config.Workspace /-! Definitions to support `lake print-paths` builds. diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean index 4394a00fb0..cd837eaf7a 100644 --- a/Lake/Build/Index.lean +++ b/Lake/Build/Index.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ import Lake.Build.Roots -import Lake.Build.Module import Lake.Build.Topological import Lake.Util.EStateT @@ -14,146 +13,35 @@ import Lake.Util.EStateT 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 topologically-based recursive builds. +This module leverages the index to perform topologically-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 Name (cmp := Name.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 Name (cmp := Name.quickCmp) fun k => - Package → IndexBuildFn m → m (PackageData k) - -@[inline] def PackageBuildMap.empty : PackageBuildMap m := DRBMap.empty - -/-- A map from target facet names to build functions. -/ -abbrev TargetBuildMap (m : Type → Type v) := - DRBMap Name (cmp := Name.quickCmp) fun k => - Package → IndexBuildFn m → m (PackageData k) - -@[inline] def TargetBuildMap.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 : Name} (build : Module → IndexT m α) -[h : FamilyDef ModuleData facet α] : Module → IndexT m (ModuleData facet) := - cast (by rw [← h.family_key_eq_type]) build - -/-- -Converts a conveniently typed package facet build function into its -dynamically typed equivalent. --/ -@[inline] def mkPackageFacetBuild {facet : Name} (build : Package → IndexT m α) -[h : FamilyDef PackageData facet α] : Package → IndexT m (PackageData facet) := - cast (by rw [← h.family_key_eq_type]) build - /-- Converts a conveniently typed target facet build function into its dynamically typed equivalent. -/ -@[inline] def mkTargetFacetBuild (facet : Name) (build : IndexT m α) -[h : FamilyDef TargetData facet α] : IndexT m (TargetData facet) := +@[macroInline] def mkTargetFacetBuild (facet : Name) (build : IndexBuildM α) +[h : FamilyDef TargetData facet α] : IndexBuildM (TargetData facet) := cast (by rw [← h.family_key_eq_type]) build -section -variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m] - -/-! -## Initial Facet Maps --/ - -open Module in -/-- -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 (m := m) - -- Compute unique imports (direct × transitive) - |>.insert importFacet (mkModuleFacetBuild (·.recParseImports)) - -- Build module (`.olean`, `.ilean`, and possibly `.c`) - |>.insert leanBinFacet (mkModuleFacetBuild (·.recBuildLean .leanBin)) - |>.insert oleanFacet (mkModuleFacetBuild (·.recBuildLean .olean)) - |>.insert ileanFacet (mkModuleFacetBuild (·.recBuildLean .ilean)) - |>.insert cFacet (mkModuleFacetBuild (·.recBuildLean .c)) - -- Build module `.o` - |>.insert oFacet (mkModuleFacetBuild <| fun mod => do - mod.mkOTarget (Target.active (← mod.c.recBuild)) |>.activate - ) - -- Build shared library for `--load-dynlb` - |>.insert dynlibFacet (mkModuleFacetBuild (·.recBuildDynlib)) - -/-- -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 (m := m) - -- Compute the package's transitive dependencies - |>.insert `deps (mkPackageFacetBuild <| fun pkg => do - let mut deps := #[] - let mut depSet := PackageSet.empty - for dep in pkg.deps do - for depDep in (← recBuild <| dep.facet `deps) do - unless depSet.contains depDep do - deps := deps.push depDep - depSet := depSet.insert depDep - unless depSet.contains dep do - deps := deps.push dep - depSet := depSet.insert dep - return deps - ) - -- Build the `extraDepTarget` for the package and its transitive dependencies - |>.insert `extraDep (mkPackageFacetBuild <| fun pkg => do - let mut target := ActiveTarget.nil - for dep in pkg.deps do - target ← target.mixOpaqueAsync (← dep.extraDep.recBuild) - target.mixOpaqueAsync <| ← pkg.extraDepTarget.activate - ) - /-! ## Topologically-based Recursive Build Using the Index -/ /-- Recursive build function for anything in the Lake build index. -/ -@[specialize] def recBuildIndex (info : BuildInfo) : IndexT m (BuildData info.key) := do - have : MonadLift BuildM m := ⟨liftM⟩ +def recBuildWithIndex (info : BuildInfo) : IndexBuildM (BuildData info.key) := do match info with | .moduleFacet mod facet => - if let some build := moduleBuildMap.find? facet then - build mod - else if let some config := (← getWorkspace).findModuleFacetConfig? facet then - have := config.familyDef - mkModuleFacetBuild config.build mod + if let some config := (← getWorkspace).findModuleFacetConfig? facet then + config.build mod else error s!"do not know how to build module facet `{facet}`" | .packageFacet pkg facet => - if let some build := packageBuildMap.find? facet then - build pkg - else if let some config := (← getWorkspace).findPackageFacetConfig? facet then - have := config.familyDef - mkPackageFacetBuild config.build pkg + if let some config := (← getWorkspace).findPackageFacetConfig? facet then + config.build pkg else error s!"do not know how to build package facet `{facet}`" | .customTarget pkg target => @@ -170,7 +58,7 @@ the initial set of Lake package facets (e.g., `extraDep`). | .sharedLeanLib lib => mkTargetFacetBuild LeanLib.sharedFacet lib.recBuildShared | .leanExe exe => - mkTargetFacetBuild LeanExe.exeFacet exe.recBuild + mkTargetFacetBuild LeanExe.exeFacet exe.recBuildExe | .staticExternLib lib => mkTargetFacetBuild ExternLib.staticFacet lib.target.activate | .sharedExternLib lib => @@ -182,31 +70,41 @@ the initial set of Lake package facets (e.g., `extraDep`). 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 +def buildIndexTop' (info : BuildInfo) : RecBuildM (BuildData info.key) := + buildDTop BuildData BuildInfo.key recBuildWithIndex info /-- Recursively build the given info using the Lake build index and a topological / suspending scheduler and return the dynamic result. -/ -@[inline] def buildIndexTop (info : BuildInfo) -[FamilyDef BuildData info.key α] : CycleT BuildKey m α := do - cast (by simp) <| buildIndexTop' (m := m) info - -end +@[macroInline] def buildIndexTop (info : BuildInfo) +[FamilyDef BuildData info.key α] : RecBuildM α := do + cast (by simp) <| buildIndexTop' info /-- Build the given Lake target using the given Lake build store. -/ -@[inline] def BuildInfo.buildIn (store : BuildStore) (self : BuildInfo) -[FamilyDef BuildData self.key α] : BuildM α := do - failOnBuildCycle <| ← EStateT.run' (m := BuildM) store <| buildIndexTop self +@[inline] def BuildInfo.buildIn +(store : BuildStore) (self : BuildInfo) [FamilyDef BuildData self.key α] : BuildM α := do + failOnBuildCycle <| ← EStateT.run' store <| buildIndexTop self /-- Build the given Lake target in a fresh build store. -/ -@[inline] def BuildInfo.build (self : BuildInfo) [FamilyDef BuildData self.key α] : BuildM α := +@[macroInline] def BuildInfo.build +(self : BuildInfo) [FamilyDef BuildData self.key α] : BuildM α := buildIn BuildStore.empty self export BuildInfo (build buildIn) -/-- An opaque target that builds the Lake target in a fresh build store. -/ +/-! ## Targets Using the Build Index -/ + +/-- An opaque target that builds the info in a fresh build store. -/ @[inline] def BuildInfo.target (self : BuildInfo) [FamilyDef BuildData self.key (ActiveBuildTarget α)] : OpaqueTarget := BuildTarget.mk' () <| self.build <&> (·.task) + +/-- A smart constructor for facet configurations that generate targets. -/ +@[inline] def mkFacetTargetConfig (build : ι → IndexBuildM (ActiveBuildTarget α)) +[h : FamilyDef Fam facet (ActiveBuildTarget α)] : FacetConfig Fam ι facet where + build := cast (by rw [← h.family_key_eq_type]) build + toTarget? := fun info key_eq_type => + have : FamilyDef BuildData info.key (ActiveBuildTarget α) := + ⟨h.family_key_eq_type ▸ key_eq_type⟩ + info.target diff --git a/Lake/Build/IndexTargets.lean b/Lake/Build/IndexTargets.lean index b3f2471e5d..e5fdb416d8 100644 --- a/Lake/Build/IndexTargets.lean +++ b/Lake/Build/IndexTargets.lean @@ -10,25 +10,14 @@ open Lean hiding SearchPath namespace Lake -/-! # Module Facet Targets -/ +/-! ## Module Facet Targets -/ +/-- An opaque target thats build the module facet in a fresh build store. -/ @[inline] def Module.facetTarget (facet : Name) (self : Module) [FamilyDef ModuleData facet (ActiveBuildTarget α)] : OpaqueTarget := self.facet facet |>.target -@[inline] def Module.oleanTarget (self : Module) : FileTarget := - self.facetTarget oleanFacet |>.withInfo self.oleanFile - -@[inline] def Module.ileanTarget (self : Module) : FileTarget := - self.facetTarget ileanFacet |>.withInfo self.ileanFile - -@[inline] def Module.cTarget (self : Module) : FileTarget := - self.facetTarget cFacet |>.withInfo self.cFile - -@[inline] def Module.oTarget (self : Module) : FileTarget := - self.facetTarget oFacet |>.withInfo self.oFile - -/-! # Pure Lean Lib Targets -/ +/-! ## Pure Lean Lib Targets -/ /-- Build the `extraDepTarget` of a package and its (transitive) dependencies @@ -50,7 +39,7 @@ def LeanLib.buildModules (self : LeanLib) (facet : Name) @[inline] protected def Package.leanLibTarget (self : Package) : OpaqueTarget := self.builtinLib.leanTarget -/-! # Native Lean Lib Targets -/ +/-! ## Native Lean Lib Targets -/ @[inline] protected def LeanLib.staticLibTarget (self : LeanLib) : FileTarget := self.static.target.withInfo self.sharedLibFile @@ -64,11 +53,14 @@ def LeanLib.buildModules (self : LeanLib) (facet : Name) @[inline] protected def Package.sharedLibTarget (self : Package) : FileTarget := self.builtinLib.sharedLibTarget -/-! # Lean Executable Targets -/ +/-! ## Lean Executable Targets -/ @[inline] protected def LeanExe.build (self : LeanExe) : BuildM ActiveFileTarget := self.exe.build +@[inline] protected def LeanExe.recBuild (self : LeanExe) : IndexBuildM ActiveFileTarget := + self.exe.recBuild + @[inline] protected def LeanExe.target (self : LeanExe) : FileTarget := self.exe.target.withInfo self.file diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean index 56ae364c8b..13aa4714c7 100644 --- a/Lake/Build/Info.lean +++ b/Lake/Build/Info.lean @@ -118,6 +118,9 @@ abbrev IndexBuildFn (m : Type → Type v) := /-- A transformer to equip a monad with a build function for the Lake index. -/ abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m +/-- The monad for build functions that are part of the index. -/ +abbrev IndexBuildM := IndexT RecBuildM + /-- Build the given info using the Lake build index. -/ @[inline] def BuildInfo.recBuild (self : BuildInfo) [FamilyDef BuildData self.key α] : IndexT m α := fun build => cast (by simp) <| build self @@ -136,12 +139,12 @@ Defined here because they need to import configurations, whereas the definitions there need to be imported by configurations. -/ -abbrev Module.importFacet := `lean.imports - /-- The direct × transitive imports of the Lean module. -/ +abbrev Module.importFacet := `lean.imports module_data lean.imports : Array Module × Array Module /-- The package's complete array of transitive dependencies. -/ +abbrev Package.depsFacet := `deps package_data deps : Array Package @@ -174,7 +177,7 @@ end Module abbrev Package.facet (facet : Name) (self : Package) : BuildInfo := .packageFacet self facet -/-- Build info for the package's `extraDepTarget`. -/ +/-- Build info for the package and its dependencies collective `extraDepTarget`. -/ abbrev Package.extraDep (self : Package) : BuildInfo := self.facet `extraDep diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean index 9c8f899610..26cd9883b3 100644 --- a/Lake/Build/Module.lean +++ b/Lake/Build/Module.lean @@ -4,9 +4,7 @@ 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 +import Lake.Build.Index open System @@ -64,12 +62,9 @@ def Module.mkDynlibTarget (self : Module) (linkTargets : Array FileTarget) /-! # Recursive Building -/ -section -variable [Monad m] [MonadBuildStore m] - /-- Compute library directories and build external library targets of the given packages. -/ def recBuildExternalDynlibs (pkgs : Array Package) -[MonadLog m] : IndexT m (Array ActiveFileTarget × Array FilePath) := do +: IndexBuildM (Array ActiveFileTarget × Array FilePath) := do let mut libDirs := #[] let mut targets : Array ActiveFileTarget := #[] for pkg in pkgs do @@ -90,8 +85,8 @@ def recBuildExternalDynlibs (pkgs : Array Package) return (targets, libDirs) /-- Build the dynlibs of all imports. -/ -@[specialize] def recBuildDynlibs (pkg : Package) (imports : Array Module) -[MonadLog m] : IndexT m (Array ActiveFileTarget × Array ActiveFileTarget × Array FilePath) := do +def recBuildDynlibs (pkg : Package) (imports : Array Module) +: IndexBuildM (Array ActiveFileTarget × Array ActiveFileTarget × Array FilePath) := do let mut pkgs := #[] let mut pkgSet := PackageSet.empty.insert pkg let mut targets := #[] @@ -103,8 +98,8 @@ def recBuildExternalDynlibs (pkgs : Array Package) return (targets, ← recBuildExternalDynlibs <| pkgs.push pkg) /-- Build the dynlibs of the imports that want precompilation (and *their* imports). -/ -@[specialize] def recBuildPrecompileDynlibs (pkg : Package) (imports : Array Module) -[MonadLog m] : IndexT m (Array ActiveFileTarget × Array ActiveFileTarget × Array FilePath) := do +def recBuildPrecompileDynlibs (pkg : Package) (imports : Array Module) +: IndexBuildM (Array ActiveFileTarget × Array ActiveFileTarget × Array FilePath) := do let mut pkgs := #[] let mut pkgSet := PackageSet.empty.insert pkg let mut modSet := ModuleSet.empty @@ -134,9 +129,8 @@ optionally outputting a `.c` file if the modules' is not lean-only or the requested artifact is `c`. Returns an active target producing the requested artifact. -/ -@[specialize] def Module.recBuildLean (mod : Module) (art : LeanArtifact) -: IndexT m (ActiveBuildTarget (if art = .leanBin then PUnit else FilePath)) := do - have : MonadLift BuildM m := ⟨liftM⟩ +def Module.recBuildLean (mod : Module) (art : LeanArtifact) +: IndexBuildM (ActiveBuildTarget (if art = .leanBin then PUnit else FilePath)) := do let leanOnly := mod.isLeanOnly ∧ art ≠ .c -- Compute and build dependencies @@ -176,14 +170,38 @@ artifact. | .ilean => ileanTarget | .c => cTarget +/-- The `ModuleFacetConfig` for the builtin `leanBinFacet`. -/ +def Module.leanBinFacetConfig : ModuleFacetConfig leanBinFacet := + mkFacetTargetConfig (·.recBuildLean .leanBin) + +/-- The `ModuleFacetConfig` for the builtin `oleanFacet`. -/ +def Module.oleanFacetConfig : ModuleFacetConfig oleanFacet := + mkFacetTargetConfig (·.recBuildLean .olean) + +/-- The `ModuleFacetConfig` for the builtin `ileanFacet`. -/ +def Module.ileanFacetConfig : ModuleFacetConfig ileanFacet := + mkFacetTargetConfig (·.recBuildLean .ilean) + +/-- The `ModuleFacetConfig` for the builtin `cFacet`. -/ +def Module.cFacetConfig : ModuleFacetConfig cFacet := + mkFacetTargetConfig (·.recBuildLean .c) + +/-- +Recursively build the module's object file from its C file produced by `lean`. +-/ +def Module.recBuildLeanO (self : Module) : IndexBuildM ActiveFileTarget := do + self.mkOTarget (Target.active (← self.c.recBuild)) |>.activate + +/-- The `ModuleFacetConfig` for the builtin `oFacet`. -/ +def Module.oFacetConfig : ModuleFacetConfig oFacet := + mkFacetTargetConfig (·.recBuildLeanO) /-- 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) -: IndexT m (Array Module × Array Module) := do - have : MonadLift BuildM m := ⟨liftM⟩ +def Module.recParseImports (mod : Module) +: IndexBuildM (Array Module × Array Module) := do let mut transImports := #[] let mut directImports := #[] let mut importSet := ModuleSet.empty @@ -202,15 +220,36 @@ building an `Array` product of its direct and transitive local imports. directImports := directImports.push mod return (directImports, transImports) +/-- The `ModuleFacetConfig` for the builtin `importFacet`. -/ +def Module.importFacetConfig : ModuleFacetConfig importFacet := + mkFacetConfig (·.recParseImports) + /-- Recursively build the shared library of a module (e.g., for `--load-dynlib`). -/ -@[specialize] def Module.recBuildDynlib (mod : Module) -: IndexT m ActiveFileTarget := do - have : MonadLift BuildM m := ⟨liftM⟩ +def Module.recBuildDynlib (mod : Module) : IndexBuildM ActiveFileTarget := do let (_, transImports) ← mod.imports.recBuild let linkTargets ← mod.nativeFacets.mapM fun facet => do return Target.active <| ← recBuild <| mod.facet facet.name let (modTargets, pkgTargets, libDirs) ← recBuildDynlibs mod.pkg transImports let libTargets := modTargets ++ pkgTargets |>.map Target.active mod.mkDynlibTarget linkTargets libDirs libTargets |>.activate + +/-- The `ModuleFacetConfig` for the builtin `dynlibFacet`. -/ +def Module.dynlibFacetConfig : ModuleFacetConfig dynlibFacet := + mkFacetTargetConfig (·.recBuildDynlib) + +open Module in +/-- +A name-configuration map for the initial set of +Lake module facets (e.g., `lean.{imports, c, o, dynlib]`). +-/ +def initModuleFacetConfigs : DNameMap ModuleFacetConfig := + DNameMap.empty + |>.insert importFacet importFacetConfig + |>.insert leanBinFacet leanBinFacetConfig + |>.insert oleanFacet oleanFacetConfig + |>.insert ileanFacet ileanFacetConfig + |>.insert cFacet cFacetConfig + |>.insert oFacet oFacetConfig + |>.insert dynlibFacet dynlibFacetConfig diff --git a/Lake/Build/Package.lean b/Lake/Build/Package.lean new file mode 100644 index 0000000000..48ca4d51dd --- /dev/null +++ b/Lake/Build/Package.lean @@ -0,0 +1,47 @@ +/- +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.Index + +namespace Lake + +/-- Compute a topological ordering of the package's transitive dependencies. -/ +def Package.recComputeDeps (self : Package) : IndexBuildM (Array Package) := do + let mut deps := #[] + let mut depSet := PackageSet.empty + for dep in self.deps do + for depDep in (← recBuild <| dep.facet `deps) do + unless depSet.contains depDep do + deps := deps.push depDep + depSet := depSet.insert depDep + unless depSet.contains dep do + deps := deps.push dep + depSet := depSet.insert dep + return deps + +/-- The `PackageFacetConfig` for the builtin `depsFacet`. -/ +def Package.depsFacetConfig : PackageFacetConfig depsFacet := + mkFacetConfig (·.recComputeDeps) + +/-- Build the `extraDepTarget` for the package and its transitive dependencies. -/ +def Package.recBuildExtraDepTargets (self : Package) : IndexBuildM ActiveOpaqueTarget := do + let mut target := ActiveTarget.nil + for dep in self.deps do + target ← target.mixOpaqueAsync (← dep.extraDep.recBuild) + target.mixOpaqueAsync <| ← self.extraDepTarget.activate + +/-- The `PackageFacetConfig` for the builtin `dynlibFacet`. -/ +def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet := + mkFacetTargetConfig (·.recBuildExtraDepTargets) + +open Package in +/-- +A package facet name to build function map that contains builders for +the initial set of Lake package facets (e.g., `extraDep`). +-/ +def initPackageFacetConfigs : DNameMap PackageFacetConfig := + DNameMap.empty + |>.insert depsFacet depsFacetConfig + |>.insert extraDepFacet extraDepFacetConfig diff --git a/Lake/Build/Roots.lean b/Lake/Build/Roots.lean index 9d91ac7ece..975e302d37 100644 --- a/Lake/Build/Roots.lean +++ b/Lake/Build/Roots.lean @@ -9,14 +9,11 @@ import Lake.Build.Targets namespace Lake -variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m] - /-! # Build Static Lib -/ /-- Build and collect the specified facet of the library's local modules. -/ -@[specialize] def LeanLib.recBuildLocalModules -(facets : Array (ModuleFacet α)) (self : LeanLib) : IndexT m (Array α) := do - have : MonadLift BuildM m := ⟨liftM⟩ +def LeanLib.recBuildLocalModules +(facets : Array (ModuleFacet α)) (self : LeanLib) : IndexT RecBuildM (Array α) := do let mut results := #[] let mut modSet := ModuleSet.empty let mods ← self.getModuleArray @@ -31,9 +28,7 @@ variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m] modSet := modSet.insert mod return results -@[specialize] protected -def LeanLib.recBuildStatic (self : LeanLib) : IndexT m ActiveFileTarget := do - have : MonadLift BuildM m := ⟨liftM⟩ +protected def LeanLib.recBuildStatic (self : LeanLib) : IndexT RecBuildM ActiveFileTarget := do let oTargets := (← self.recBuildLocalModules self.nativeFacets).map Target.active staticLibTarget self.staticLibFile oTargets |>.activate @@ -43,10 +38,9 @@ def LeanLib.recBuildStatic (self : LeanLib) : IndexT m ActiveFileTarget := do Build and collect the local object files and external libraries of a library and its modules' imports. -/ -@[specialize] def LeanLib.recBuildLinks +def LeanLib.recBuildLinks (facets : Array (ModuleFacet ActiveFileTarget)) (self : LeanLib) -: IndexT m (Array ActiveFileTarget) := do - have : MonadLift BuildM m := ⟨liftM⟩ +: IndexT RecBuildM (Array ActiveFileTarget) := do -- Build and collect modules let mut pkgs := #[] let mut pkgSet := PackageSet.empty @@ -72,17 +66,13 @@ of a library and its modules' imports. targets := targets.push target return targets -@[specialize] protected -def LeanLib.recBuildShared (self : LeanLib) : IndexT m ActiveFileTarget := do - have : MonadLift BuildM m := ⟨liftM⟩ +protected def LeanLib.recBuildShared (self : LeanLib) : IndexT RecBuildM ActiveFileTarget := do let linkTargets := (← self.recBuildLinks self.nativeFacets).map Target.active leanSharedLibTarget self.sharedLibFile linkTargets self.linkArgs |>.activate /-! # Build Executable -/ -@[specialize] protected -def LeanExe.recBuild (self : LeanExe) : IndexT m ActiveFileTarget := do - have : MonadLift BuildM m := ⟨liftM⟩ +protected def LeanExe.recBuildExe (self : LeanExe) : IndexT RecBuildM ActiveFileTarget := do let (_, imports) ← self.root.imports.recBuild let linkTargets := #[Target.active <| ← self.root.o.recBuild] let mut linkTargets ← imports.foldlM (init := linkTargets) fun arr mod => do diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean index 8b7f9e44d3..1211f35502 100644 --- a/Lake/CLI/Build.lean +++ b/Lake/CLI/Build.lean @@ -38,12 +38,10 @@ def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : Name) : Except return mod.facetTarget oFacet else if facet == `dynlib then return mod.facetTarget dynlibFacet - else if let some config := ws.findModuleFacetConfig? facet then - if let some (.up ⟨_, h⟩) := config.result_eq_target? then - have := config.familyDefTarget h - return mod.facetTarget facet - else - throw <| CliError.nonTargetFacet "module" facet + else if let some config := ws.findModuleFacetConfig? facet then do + let some target := config.toTarget? (mod.facet facet) rfl + | throw <| CliError.nonTargetFacet "module" facet + return target else throw <| CliError.unknownFacet "module" facet @@ -105,12 +103,10 @@ def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : Name) : Excep return pkg.sharedLibTarget.withoutInfo else if facet == `leanLib then return pkg.leanLibTarget.withoutInfo - else if let some config := ws.findPackageFacetConfig? facet then - if let some (.up ⟨_, h⟩) := config.result_eq_target? then - have := config.familyDefTarget h - return pkg.facet facet |>.target - else - throw <| CliError.nonTargetFacet "package" facet + else if let some config := ws.findPackageFacetConfig? facet then do + let some target := config.toTarget? (pkg.facet facet) rfl + | throw <| CliError.nonTargetFacet "package" facet + return target else throw <| CliError.unknownFacet "package" facet diff --git a/Lake/Config/FacetConfig.lean b/Lake/Config/FacetConfig.lean index 6e54e0643a..ee2b56222a 100644 --- a/Lake/Config/FacetConfig.lean +++ b/Lake/Config/FacetConfig.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Mac Malone +Authors: Mac Malone, Mario Carneiro -/ import Lake.Build.Info import Lake.Build.Store @@ -9,67 +9,34 @@ import Lake.Build.Store namespace Lake /-- A facet's declarative configuration. -/ -structure FacetConfig (DataFam : Name → Type u) (BuildFn : Type u → Type v) (name : Name) where - /-- The type of the target's build result. -/ - resultType : Type u - /-- The facet's build function. -/ - build : BuildFn resultType - /-- Proof that the facet's build result data type is properly registered. -/ - data_eq_result : DataFam name = resultType - /-- Is this facet a buildable target? -/ - result_eq_target? : Option <| PLift <| PSigma fun α => resultType = ActiveBuildTarget α +structure FacetConfig (DataFam : Name → Type) (ι : Type) (name : Name) : Type where + /-- The facet's build (function). -/ + build : ι → IndexBuildM (DataFam name) + /-- Is this facet a buildable target? -/ + toTarget? : (info : BuildInfo) → BuildData info.key = DataFam name → Option (OpaqueTarget.{0}) + deriving Inhabited -instance [(α : Type u) → Inhabited (BuildFn α)] : Inhabited (FacetConfig DataFam BuildFn name) := ⟨{ - resultType := DataFam name - build := default - data_eq_result := rfl - result_eq_target? := none -}⟩ +protected abbrev FacetConfig.name (_ : FacetConfig DataFam ι name) := name -abbrev FacetBuildFn (ι) := - fun resultType => {m : Type → Type} → - [Monad m] → [MonadLift BuildM m] → [MonadBuildStore m] → - ι → IndexT m resultType - -instance : Inhabited (FacetBuildFn ι α) := - ⟨fun _ => liftM (m := BuildM) failure⟩ - -namespace FacetConfig - -protected def name (_ : FacetConfig DataFam BuildFn name) := - name - -instance (cfg : FacetConfig Fam Fn name) : - FamilyDef Fam cfg.name cfg.resultType := ⟨cfg.data_eq_result⟩ - -def familyDef (cfg : FacetConfig Fam Fn name) : FamilyDef Fam name cfg.resultType := - ⟨cfg.data_eq_result⟩ - -def familyDefTarget (cfg : FacetConfig Fam Fn name) -(h : cfg.resultType = ActiveBuildTarget α) : FamilyDef Fam name (ActiveBuildTarget α) := - ⟨h ▸ cfg.data_eq_result⟩ - -end FacetConfig +/-- A smart constructor for facet configurations that are not known to generate targets. -/ +@[inline] def mkFacetConfig (build : ι → IndexBuildM α) +[h : FamilyDef Fam facet α] : FacetConfig Fam ι facet where + build := cast (by rw [← h.family_key_eq_type]) build + toTarget? := fun _ _ => none /-- A dependently typed configuration based on its registered name. -/ structure NamedConfigDecl (β : Name → Type u) where name : Name config : β name --------------------------------------------------------------------------------- - /-- A module facet's declarative configuration. -/ -abbrev ModuleFacetConfig := FacetConfig ModuleData (FacetBuildFn Module) -hydrate_opaque_type OpaqueModuleFacetConfig ModuleFacetConfig name +abbrev ModuleFacetConfig := FacetConfig ModuleData Module /-- A module facet declaration from a configuration file. -/ abbrev ModuleFacetDecl := NamedConfigDecl ModuleFacetConfig --------------------------------------------------------------------------------- - /-- A package facet's declarative configuration. -/ -abbrev PackageFacetConfig := FacetConfig PackageData (FacetBuildFn Package) -hydrate_opaque_type OpaquePackageFacetConfig PackageFacetConfig name +abbrev PackageFacetConfig := FacetConfig PackageData Package /-- A package facet declaration from a configuration file. -/ abbrev PackageFacetDecl := NamedConfigDecl PackageFacetConfig diff --git a/Lake/Config/Opaque.lean b/Lake/Config/Opaque.lean index 14d7812053..41c8e513df 100644 --- a/Lake/Config/Opaque.lean +++ b/Lake/Config/Opaque.lean @@ -14,11 +14,5 @@ declare_opaque_type OpaquePackage /-- Opaque reference to a `Workspace` used for forward declaration. -/ declare_opaque_type OpaqueWorkspace -/-- Opaque reference to a `ModuleFacetConfig` used for forward declaration. -/ -declare_opaque_type OpaqueModuleFacetConfig (name : Name) - -/-- Opaque reference to a `PackageFacetConfig` used for forward declaration. -/ -declare_opaque_type OpaquePackageFacetConfig (name : Name) - /-- Opaque reference to a `TargetConfig` used for forward declaration. -/ declare_opaque_type OpaqueTargetConfig diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean index 0857f93a46..fbc89c6d4b 100644 --- a/Lake/Config/Package.lean +++ b/Lake/Config/Package.lean @@ -239,6 +239,7 @@ end PackageConfig -------------------------------------------------------------------------------- abbrev DNameMap α := DRBMap Name α Lean.Name.quickCmp +@[inline] def DNameMap.empty : DNameMap α := DRBMap.empty /-- A Lake package -- its location plus its configuration. -/ structure Package where diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean index 30a5813c24..4e27edcab4 100644 --- a/Lake/Config/Workspace.lean +++ b/Lake/Config/Workspace.lean @@ -17,7 +17,7 @@ namespace Lake def manifestFileName := "manifest.json" /-- A Lake workspace -- the top-level package directory. -/ -structure Workspace where +structure Workspace : Type where /-- The root package of the workspace. -/ root : Package /-- The detect `Lake.Env` of the workspace. -/ @@ -28,12 +28,12 @@ structure Workspace where Name-configuration map of (opaque references to) module facets defined in the workspace. -/ - opaqueModuleFacetConfigs : DNameMap OpaqueModuleFacetConfig := {} + moduleFacetConfigs : DNameMap ModuleFacetConfig := {} /-- Name-configuration map of (opaque references to) module facets defined in the workspace. -/ - opaquePackageFacetConfigs : DNameMap OpaquePackageFacetConfig := {} + packageFacetConfigs : DNameMap PackageFacetConfig := {} deriving Inhabited hydrate_opaque_type OpaqueWorkspace Workspace @@ -102,23 +102,19 @@ def findTargetConfig? (name : Name) (self : Workspace) : Option (Package × Targ /-- Add a module facet to the workspace. -/ def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Workspace := - {self with opaqueModuleFacetConfigs := self.opaqueModuleFacetConfigs.insert cfg.name (.mk cfg)} + {self with moduleFacetConfigs := self.moduleFacetConfigs.insert cfg.name cfg} /-- Try to find a module facet configuration in the workspace with the given name. -/ def findModuleFacetConfig? (name : Name) (self : Workspace) : Option (ModuleFacetConfig name) := - match self.opaqueModuleFacetConfigs.find? name with - | some cfg => cfg.get - | none => none + self.moduleFacetConfigs.find? name /-- Add a package facet to the workspace. -/ def addPackageFacetConfig (cfg : PackageFacetConfig name) (self : Workspace) : Workspace := - {self with opaquePackageFacetConfigs := self.opaquePackageFacetConfigs.insert cfg.name (.mk cfg)} + {self with packageFacetConfigs := self.packageFacetConfigs.insert cfg.name cfg} /-- Try to find a package facet configuration in the workspace with the given name. -/ def findPackageFacetConfig? (name : Name) (self : Workspace) : Option (PackageFacetConfig name) := - match self.opaquePackageFacetConfigs.find? name with - | some cfg => cfg.get - | none => none + self.packageFacetConfigs.find? name /-- The `LEAN_PATH` of the workspace. -/ def leanPath (self : Workspace) : SearchPath := diff --git a/Lake/DSL/Facets.lean b/Lake/DSL/Facets.lean index 754a86af5f..f77428e921 100644 --- a/Lake/DSL/Facets.lean +++ b/Lake/DSL/Facets.lean @@ -6,6 +6,7 @@ Authors: Mac Malone import Lake.DSL.DeclUtil import Lake.Config.FacetConfig import Lake.Config.TargetConfig +import Lake.Build.Index /-! Macros for declaring custom facets and targets. @@ -21,17 +22,11 @@ kw:"module_facet " sig:simpleDeclSig : command => do | `(simpleDeclSig| $id:ident : $ty := $defn $[$wds?]?) => let attr ← withRef kw `(Term.attrInstance| moduleFacet) let attrs := #[attr] ++ expandAttrs attrs? - let axm := mkIdentFrom id <| ``ModuleData ++ id.getId let name := Name.quoteFrom id id.getId `(module_data $id : ActiveBuildTarget $ty $[$doc?]? @[$attrs,*] def $id : ModuleFacetDecl := { name := $name - config := { - resultType := ActiveBuildTarget $ty - build := $defn - data_eq_result := $axm - result_eq_target? := some (.up ⟨$ty, rfl⟩) - } + config := Lake.mkFacetTargetConfig $defn }) | stx => Macro.throwErrorAt stx "ill-formed module facet declaration" @@ -42,17 +37,11 @@ kw:"package_facet " sig:simpleDeclSig : command => do | `(simpleDeclSig| $id:ident : $ty := $defn $[$wds?]?) => let attr ← withRef kw `(Term.attrInstance| packageFacet) let attrs := #[attr] ++ expandAttrs attrs? - let axm := mkIdentFrom id <| ``PackageData ++ id.getId let name := Name.quoteFrom id id.getId `(package_data $id : ActiveBuildTarget $ty $[$doc?]? @[$attrs,*] def $id : PackageFacetDecl := { name := $name - config := { - resultType := ActiveBuildTarget $ty - build := $defn - data_eq_result := $axm - result_eq_target? := some (.up ⟨$ty, rfl⟩) - } + config := Lake.mkFacetTargetConfig $defn }) | stx => Macro.throwErrorAt stx "ill-formed package facet declaration" diff --git a/Lake/Load/Main.lean b/Lake/Load/Main.lean index 3c7135b02d..5ca5576743 100644 --- a/Lake/Load/Main.lean +++ b/Lake/Load/Main.lean @@ -7,6 +7,8 @@ import Lake.Util.EStateT import Lake.Util.StoreInsts import Lake.Config.Workspace import Lake.Build.Topological +import Lake.Build.Module +import Lake.Build.Package import Lake.Load.Materialize import Lake.Load.Package import Lake.Load.Elab @@ -69,7 +71,11 @@ elaborating its configuration file and resolve its dependencies. def loadWorkspace (config : LoadConfig) : LogIO Workspace := do Lean.searchPathRef.set config.env.leanSearchPath let root ← loadPkg config.rootDir config.configOpts config.leanOpts config.configFile - let ws : Workspace := {root, lakeEnv := config.env} + let ws : Workspace := { + root, lakeEnv := config.env + moduleFacetConfigs := initModuleFacetConfigs + packageFacetConfigs := initPackageFacetConfigs + } let deps ← IO.ofExcept <| loadDeps root.configEnv config.leanOpts let manifest ← Manifest.loadFromFile ws.manifestFile |>.catchExceptions fun _ => pure {} let ((ws, deps), manifest) ← resolveDeps ws root