From f2bcba7c7398aac817090d24ff6a1e67458a6de0 Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 4 Aug 2022 18:30:53 -0400 Subject: [PATCH] refactor: renames + cleanup --- Lake/Build/Executable.lean | 15 ++++++--------- Lake/Build/Index.lean | 10 +++++----- Lake/Build/Info.lean | 16 ++++++++-------- Lake/Build/Library.lean | 10 +++++----- Lake/Build/Module.lean | 34 +++++++++++++++++----------------- Lake/Build/Package.lean | 4 ++-- Lake/CLI/Build.lean | 2 +- examples/ffi/lib/lakefile.lean | 2 +- 8 files changed, 45 insertions(+), 48 deletions(-) diff --git a/Lake/Build/Executable.lean b/Lake/Build/Executable.lean index ee7ddefbf2..bf27e2099d 100644 --- a/Lake/Build/Executable.lean +++ b/Lake/Build/Executable.lean @@ -11,14 +11,11 @@ namespace Lake protected def LeanExe.recBuildExe (self : LeanExe) : IndexBuildM (BuildJob FilePath) := do - let (_, imports) ← self.root.imports.recBuild - let linkJobs := #[← self.root.o.recBuild] - let mut linkJobs ← imports.foldlM (init := linkJobs) fun arr mod => do - let mut arr := arr - for facet in mod.nativeFacets do - arr := arr.push <| ← recBuild <| mod.facet facet.name - return arr - let deps := (← recBuild <| self.pkg.facet `deps).push self.pkg + let (_, imports) ← self.root.imports.fetch + let mut linkJobs := #[← self.root.o.fetch] + for mod in imports do for facet in mod.nativeFacets do + linkJobs := linkJobs.push <| ← fetch <| mod.facet facet.name + let deps := (← fetch <| self.pkg.facet `deps).push self.pkg for dep in deps do for lib in dep.externLibs do - linkJobs := linkJobs.push <| ← lib.static.recBuild + linkJobs := linkJobs.push <| ← lib.static.fetch buildLeanExe self.file linkJobs self.linkArgs diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean index bcf1c0db7a..392ef8a051 100644 --- a/Lake/Build/Index.lean +++ b/Lake/Build/Index.lean @@ -33,10 +33,10 @@ def ExternLib.recBuildStatic (lib : ExternLib) : IndexBuildM (BuildJob FilePath) error "missing target for external library" def ExternLib.recBuildShared (lib : ExternLib) : IndexBuildM (BuildJob FilePath) := do - buildLeanSharedLibOfStatic (← lib.static.recBuild) lib.linkArgs + buildLeanSharedLibOfStatic (← lib.static.fetch) lib.linkArgs def ExternLib.recComputeDynlib (lib : ExternLib) : IndexBuildM (BuildJob Dynlib) := do - computeDynlibOfShared (← lib.shared.recBuild) + computeDynlibOfShared (← lib.shared.fetch) /-! ## Topologically-based Recursive Build Using the Index @@ -54,7 +54,7 @@ def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key) config.build pkg else error s!"do not know how to build package facet `{facet}`" -| .customTarget pkg target => +| .target pkg target => if let some config := pkg.findTargetConfig? target then config.build pkg else @@ -100,5 +100,5 @@ export BuildInfo (build) @[inline] protected def LeanExe.build (self : LeanExe) : BuildM (BuildJob FilePath) := self.exe.build -@[inline] protected def LeanExe.recBuild (self : LeanExe) : IndexBuildM (BuildJob FilePath) := - self.exe.recBuild +@[inline] protected def LeanExe.fetch (self : LeanExe) : IndexBuildM (BuildJob FilePath) := + self.exe.fetch diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean index 5a93ec7948..f43260719f 100644 --- a/Lake/Build/Info.lean +++ b/Lake/Build/Info.lean @@ -28,7 +28,7 @@ inductive BuildInfo | staticExternLib (lib : ExternLib) | sharedExternLib (lib : ExternLib) | dynlibExternLib (lib : ExternLib) -| customTarget (package : Package) (target : Name) +| target (package : Package) (target : Name) -------------------------------------------------------------------------------- /-! ## Build Info & Keys -/ @@ -71,7 +71,7 @@ abbrev BuildInfo.key : (self : BuildInfo) → BuildKey | staticExternLib l => l.staticBuildKey | sharedExternLib l => l.sharedBuildKey | dynlibExternLib l => l.dynlibBuildKey -| customTarget p t => p.targetBuildKey t +| target p t => p.targetBuildKey t /-! ### Instances for deducing data types of `BuildInfo` keys -/ @@ -84,11 +84,11 @@ instance [FamilyDef PackageData f α] family_key_eq_type := by unfold BuildData; simp instance [h : Fact (p.name = n)] [FamilyDef CustomData (n, t) α] -: FamilyDef BuildData (BuildInfo.key (.customTarget p t)) α where +: FamilyDef BuildData (BuildInfo.key (.target p t)) α where family_key_eq_type := by unfold BuildData; simp [h.proof] instance [FamilyDef CustomData (p.name, t) α] -: FamilyDef BuildData (BuildInfo.key (.customTarget p t)) α where +: FamilyDef BuildData (BuildInfo.key (.target p t)) α where family_key_eq_type := by unfold BuildData; simp instance [FamilyDef TargetData (`leanLib ++ f) α] @@ -127,10 +127,10 @@ abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m abbrev IndexBuildM := IndexT RecBuildM /-- Build the given info using the Lake build index. -/ -@[inline] def BuildInfo.recBuild (self : BuildInfo) [FamilyDef BuildData self.key α] : IndexBuildM α := +@[inline] def BuildInfo.fetch (self : BuildInfo) [FamilyDef BuildData self.key α] : IndexBuildM α := fun build => cast (by simp) <| build self -export BuildInfo (recBuild) +export BuildInfo (fetch) -------------------------------------------------------------------------------- /-! ## Build Info & Facets -/ @@ -191,8 +191,8 @@ abbrev Package.extraDep (self : Package) : BuildInfo := self.facet extraDepFacet /-- Build info for a custom package target. -/ -abbrev Package.customTarget (target : Name) (self : Package) : BuildInfo := - .customTarget self target +abbrev Package.target (target : Name) (self : Package) : BuildInfo := + .target self target /-- Build info of the Lean library's Lean binaries. -/ abbrev LeanLib.facet (self : LeanLib) (facet : Name) : BuildInfo := diff --git a/Lake/Build/Library.lean b/Lake/Build/Library.lean index da53bf14f0..4c721aadb4 100644 --- a/Lake/Build/Library.lean +++ b/Lake/Build/Library.lean @@ -16,13 +16,13 @@ def LeanLib.recBuildLocalModules let mut modSet := ModuleSet.empty let mods ← self.getModuleArray for mod in mods do - let (_, mods) ← mod.imports.recBuild + let (_, mods) ← mod.imports.fetch let mods := mods.push mod for mod in mods do if self.isLocalModule mod.name then unless modSet.contains mod do for facet in facets do - results := results.push <| ← recBuild <| mod.facet facet.name + results := results.push <| ← fetch <| mod.facet facet.name modSet := modSet.insert mod return results @@ -58,7 +58,7 @@ def LeanLib.recBuildLinks let mut modSet := ModuleSet.empty let mods ← self.getModuleArray for mod in mods do - let (_, mods) ← mod.imports.recBuild + let (_, mods) ← mod.imports.fetch let mods := mods.push mod for mod in mods do unless modSet.contains mod do @@ -67,11 +67,11 @@ def LeanLib.recBuildLinks pkgs := pkgs.push mod.pkg if self.isLocalModule mod.name then for facet in self.nativeFacets do - jobs := jobs.push <| ← recBuild <| mod.facet facet.name + jobs := jobs.push <| ← fetch <| mod.facet facet.name modSet := modSet.insert mod -- Build and collect external library jobs for pkg in pkgs do - let externLibJobs ← pkg.externLibs.mapM (·.shared.recBuild) + let externLibJobs ← pkg.externLibs.mapM (·.shared.fetch) for job in externLibJobs do jobs := jobs.push job return jobs diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean index b669d89f2e..00278f5735 100644 --- a/Lake/Build/Module.lean +++ b/Lake/Build/Module.lean @@ -46,11 +46,11 @@ def Module.buildUnlessUpToDate (mod : Module) def recBuildExternalDynlibs (pkgs : Array Package) : IndexBuildM (Array (BuildJob Dynlib) × Array FilePath) := do let mut libDirs := #[] - let mut Jobs : Array (BuildJob Dynlib) := #[] + let mut jobs : Array (BuildJob Dynlib) := #[] for pkg in pkgs do libDirs := libDirs.push pkg.libDir - Jobs := Jobs.append <| ← pkg.externLibs.mapM (·.dynlib.recBuild) - return (Jobs, libDirs) + jobs := jobs.append <| ← pkg.externLibs.mapM (·.dynlib.fetch) + return (jobs, libDirs) /-- Build the dynlibs of the imports that want precompilation (and *their* imports). -/ def recBuildPrecompileDynlibs (pkg : Package) (imports : Array Module) @@ -58,18 +58,18 @@ def recBuildPrecompileDynlibs (pkg : Package) (imports : Array Module) let mut pkgs := #[] let mut pkgSet := PackageSet.empty.insert pkg let mut modSet := ModuleSet.empty - let mut Jobs := #[] + let mut jobs := #[] for imp in imports do if imp.shouldPrecompile then - let (_, transImports) ← imp.imports.recBuild + let (_, transImports) ← imp.imports.fetch for mod in transImports.push imp do unless pkgSet.contains mod.pkg do pkgSet := pkgSet.insert mod.pkg pkgs := pkgs.push mod.pkg unless modSet.contains mod do modSet := modSet.insert mod - Jobs := Jobs.push <| ← mod.dynlib.recBuild - return (Jobs, ← recBuildExternalDynlibs <| pkgs.push pkg) + jobs := jobs.push <| ← mod.dynlib.fetch + return (jobs, ← recBuildExternalDynlibs <| pkgs.push pkg) variable [MonadLiftT BuildM m] @@ -92,14 +92,14 @@ def Module.recBuildLean (mod : Module) (art : LeanArtifact) let isDepPkgModule := mod.pkg.name ≠ (← getWorkspace).root.name let releaseJob ← do if isDepPkgModule ∧ mod.pkg.preferReleaseBuild then - mod.pkg.release.recBuild + mod.pkg.release.fetch else pure .nil -- Compute and build dependencies - let (imports, _) ← mod.imports.recBuild + let (imports, _) ← mod.imports.fetch let (modJobs, externJobs, libDirs) ← recBuildPrecompileDynlibs mod.pkg imports - let importJob ← BuildJob.mixArray <| ← imports.mapM (·.leanBin.recBuild) + let importJob ← BuildJob.mixArray <| ← imports.mapM (·.leanBin.fetch) let externDynlibsJob ← BuildJob.collectArray externJobs let modDynlibsJob ← BuildJob.collectArray modJobs @@ -161,7 +161,7 @@ def Module.cFacetConfig : ModuleFacetConfig cFacet := /-- Recursively build the module's object file from its C file produced by `lean`. -/ def Module.recBuildLeanO (self : Module) : IndexBuildM (BuildJob FilePath) := do - buildLeanO self.name.toString self.oFile (← self.c.recBuild) self.leancArgs + buildLeanO self.name.toString self.oFile (← self.c.fetch) self.leancArgs /-- The `ModuleFacetConfig` for the builtin `oFacet`. -/ def Module.oFacetConfig : ModuleFacetConfig oFacet := @@ -180,7 +180,7 @@ def Module.recParseImports (mod : Module) let (imports, _, _) ← Lean.Elab.parseImports contents mod.leanFile.toString for imp in imports do if let some mod ← findModule? imp.module then - let (_, impTransImports) ← mod.imports.recBuild + let (_, impTransImports) ← mod.imports.fetch for transImp in impTransImports do unless importSet.contains transImp do importSet := importSet.insert transImp @@ -200,20 +200,20 @@ def recBuildDynlibs (pkg : Package) (imports : Array Module) : IndexBuildM (Array (BuildJob String) × Array (BuildJob Dynlib) × Array FilePath) := do let mut pkgs := #[] let mut pkgSet := PackageSet.empty.insert pkg - let mut Jobs := #[] + let mut jobs := #[] for imp in imports do unless pkgSet.contains imp.pkg do pkgSet := pkgSet.insert imp.pkg pkgs := pkgs.push imp.pkg - Jobs := Jobs.push <| ← imp.dynlib.recBuild - return (Jobs, ← recBuildExternalDynlibs <| pkgs.push pkg) + jobs := jobs.push <| ← imp.dynlib.fetch + return (jobs, ← recBuildExternalDynlibs <| pkgs.push pkg) /-- Recursively build the shared library of a module (e.g., for `--load-dynlib`). -/ def Module.recBuildDynlib (mod : Module) : IndexBuildM (BuildJob String) := do -- Compute dependencies - let (_, transImports) ← mod.imports.recBuild - let linkJobs ← mod.nativeFacets.mapM (recBuild <| mod.facet ·.name) + let (_, transImports) ← mod.imports.fetch + let linkJobs ← mod.nativeFacets.mapM (fetch <| mod.facet ·.name) let (modJobs, externJobs, pkgLibDirs) ← recBuildDynlibs mod.pkg transImports -- Collect Jobs diff --git a/Lake/Build/Package.lean b/Lake/Build/Package.lean index fa2c75bf24..fa5d5d608d 100644 --- a/Lake/Build/Package.lean +++ b/Lake/Build/Package.lean @@ -14,7 +14,7 @@ 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 + for depDep in (← fetch <| dep.facet `deps) do unless depSet.contains depDep do deps := deps.push depDep depSet := depSet.insert depDep @@ -29,7 +29,7 @@ def Package.depsFacetConfig : PackageFacetConfig depsFacet := /-- Build the `extraDepTarget` for the package and its transitive dependencies. -/ def Package.recBuildExtraDepTargets (self : Package) : IndexBuildM (BuildJob Unit) := do - let job ← self.deps.foldlM (do ·.mix <| ← ·.extraDep.recBuild) BuildJob.nil + let job ← self.deps.foldlM (do ·.mix <| ← ·.extraDep.fetch) BuildJob.nil job.mix <| ← self.extraDepTarget /-- The `PackageFacetConfig` for the builtin `dynlibFacet`. -/ diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean index 7c8913e3d1..9cab7c7de8 100644 --- a/Lake/CLI/Build.lean +++ b/Lake/CLI/Build.lean @@ -83,7 +83,7 @@ def resolveCustomTarget (pkg : Package) if !facet.isAnonymous then throw <| CliError.invalidFacet name facet else do - let info := pkg.customTarget name + let info := pkg.target name let some getJob := config.getJob? | throw <| CliError.nonCliTarget name have h : BuildData info.key = CustomData (pkg.name, name) := rfl diff --git a/examples/ffi/lib/lakefile.lean b/examples/ffi/lib/lakefile.lean index 07a16cfd9c..ee2cad6606 100644 --- a/examples/ffi/lib/lakefile.lean +++ b/examples/ffi/lib/lakefile.lean @@ -21,5 +21,5 @@ target ffi.o : FilePath := fun pkg _ => do extern_lib libleanffi := fun pkg _ => do let name := nameToStaticLib "leanffi" - let ffiO ← recBuild <| pkg.customTarget ``ffi.o + let ffiO ← fetch <| pkg.target ``ffi.o buildStaticLib (pkg.buildDir / "c" / name) #[ffiO]