max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: renames + cleanup

Browse source
This commit is contained in:
tydeu 2022-08-04 18:30:53 -04:00
parent b8ed74e89f
commit f2bcba7c73
8 changed files with 45 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
Lake/Build/Executable.lean
View file

@ -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

10
Lake/Build/Index.lean
View file

@ -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

16
Lake/Build/Info.lean
View file

@ -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 :=

10
Lake/Build/Library.lean
View file

@ -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

34
Lake/Build/Module.lean
View file

@ -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

4
Lake/Build/Package.lean
View file

@ -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`. -/

2
Lake/CLI/Build.lean
View file

@ -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

2
examples/ffi/lib/lakefile.lean
View file

@ -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]