refactor; replace ActiveTarget with Job
This commit is contained in:
tydeu
parent
dd30925ba6
commit
bc8c809d66
22 changed files with 264 additions and 275 deletions
|
|
@ -3,15 +3,16 @@ 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.Monad
|
||||
import Lake.Build.Job
|
||||
import Lake.Config.Env
|
||||
|
||||
namespace Lake
|
||||
open System
|
||||
|
||||
def createParentDirs (path : FilePath) : IO PUnit := do
|
||||
def createParentDirs (path : FilePath) : IO Unit := do
|
||||
if let some dir := path.parent then IO.FS.createDirAll dir
|
||||
|
||||
def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do
|
||||
def proc (args : IO.Process.SpawnArgs) : JobM Unit := do
|
||||
let envStr := String.join <| args.env.toList.filterMap fun (k, v) =>
|
||||
if k == "PATH" then none else some s!"{k}={v.getD ""} " -- PATH too big
|
||||
let cmdStr := " ".intercalate (args.cmd :: args.args.toList)
|
||||
|
|
@ -20,7 +21,7 @@ def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do
|
|||
| some cwd => s!"{cmdStr} # in directory {cwd}"
|
||||
| none => cmdStr
|
||||
let out ← IO.Process.output args
|
||||
let logOutputWith (log : String → BuildM PUnit) := do
|
||||
let logOutputWith (log : String → JobM PUnit) := do
|
||||
unless out.stdout.isEmpty do
|
||||
log s!"stdout:\n{out.stdout}"
|
||||
unless out.stderr.isEmpty do
|
||||
|
|
@ -37,7 +38,7 @@ def compileLeanModule (leanFile : FilePath)
|
|||
(leanPath : SearchPath := []) (rootDir : FilePath := ".")
|
||||
(dynlibs : Array FilePath := #[]) (dynlibPath : SearchPath := {})
|
||||
(leanArgs : Array String := #[]) (lean : FilePath := "lean")
|
||||
: BuildM PUnit := do
|
||||
: JobM PUnit := do
|
||||
let mut args := leanArgs ++
|
||||
#[leanFile.toString, "-R", rootDir.toString]
|
||||
if let some oleanFile := oleanFile? then
|
||||
|
|
@ -61,7 +62,7 @@ def compileLeanModule (leanFile : FilePath)
|
|||
}
|
||||
|
||||
def compileO (oFile srcFile : FilePath)
|
||||
(moreArgs : Array String := #[]) (compiler : FilePath := "cc") : BuildM PUnit := do
|
||||
(moreArgs : Array String := #[]) (compiler : FilePath := "cc") : JobM Unit := do
|
||||
createParentDirs oFile
|
||||
proc {
|
||||
cmd := compiler.toString
|
||||
|
|
@ -69,7 +70,7 @@ def compileO (oFile srcFile : FilePath)
|
|||
}
|
||||
|
||||
def compileStaticLib (libFile : FilePath)
|
||||
(oFiles : Array FilePath) (ar : FilePath := "ar") : BuildM PUnit := do
|
||||
(oFiles : Array FilePath) (ar : FilePath := "ar") : JobM Unit := do
|
||||
createParentDirs libFile
|
||||
proc {
|
||||
cmd := ar.toString
|
||||
|
|
@ -77,7 +78,7 @@ def compileStaticLib (libFile : FilePath)
|
|||
}
|
||||
|
||||
def compileSharedLib (libFile : FilePath)
|
||||
(linkArgs : Array String) (linker : FilePath := "cc") : BuildM PUnit := do
|
||||
(linkArgs : Array String) (linker : FilePath := "cc") : JobM Unit := do
|
||||
createParentDirs libFile
|
||||
proc {
|
||||
cmd := linker.toString
|
||||
|
|
@ -85,7 +86,7 @@ def compileSharedLib (libFile : FilePath)
|
|||
}
|
||||
|
||||
def compileExe (binFile : FilePath) (linkFiles : Array FilePath)
|
||||
(linkArgs : Array String := #[]) (linker : FilePath := "cc") : BuildM PUnit := do
|
||||
(linkArgs : Array String := #[]) (linker : FilePath := "cc") : JobM Unit := do
|
||||
createParentDirs binFile
|
||||
proc {
|
||||
cmd := linker.toString
|
||||
|
|
|
|||
|
|
@ -15,12 +15,6 @@ import Lake.Build.Topological
|
|||
open System
|
||||
namespace Lake
|
||||
|
||||
/-- The `Task` monad for Lake builds. -/
|
||||
abbrev BuildTask := OptionIOTask
|
||||
|
||||
/-- A Lake build job. -/
|
||||
abbrev Job := BuildTask Unit
|
||||
|
||||
/-- A Lake context with some additional caching for builds. -/
|
||||
structure BuildContext extends Context where
|
||||
leanTrace : BuildTrace
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@ namespace Lake
|
|||
/-! # Build Executable -/
|
||||
|
||||
protected def LeanExe.recBuildExe
|
||||
(self : LeanExe) : IndexBuildM ActiveFileTarget := do
|
||||
(self : LeanExe) : IndexBuildM (BuildJob FilePath) := 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
|
||||
|
|
|
|||
|
|
@ -40,60 +40,60 @@ 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 := `bin
|
||||
module_data bin : ActiveOpaqueTarget
|
||||
module_data bin : BuildJob Unit
|
||||
|
||||
/-- The `olean` file produced by `lean` -/
|
||||
abbrev Module.oleanFacet := `olean
|
||||
module_data olean : ActiveFileTarget
|
||||
module_data olean : BuildJob FilePath
|
||||
|
||||
/-- The `ilean` file produced by `lean` -/
|
||||
abbrev Module.ileanFacet := `ilean
|
||||
module_data ilean : ActiveFileTarget
|
||||
module_data ilean : BuildJob FilePath
|
||||
|
||||
/-- The C file built from the Lean file via `lean` -/
|
||||
abbrev Module.cFacet := `c
|
||||
module_data c : ActiveFileTarget
|
||||
module_data c : BuildJob FilePath
|
||||
|
||||
/-- The object file built from `lean.c` -/
|
||||
abbrev Module.oFacet := `o
|
||||
module_data o : ActiveFileTarget
|
||||
module_data o : BuildJob FilePath
|
||||
|
||||
/-- Shared library for `--load-dynlib` -/
|
||||
/-- Shared library for `--load-dynlib`. Returns just the library name. -/
|
||||
abbrev Module.dynlibFacet := `dynlib
|
||||
module_data dynlib : ActiveFileTarget
|
||||
module_data dynlib : BuildJob String
|
||||
|
||||
/-! ## Package Facets -/
|
||||
|
||||
/-- The package's `extraDepTarget` mixed with its transitive dependencies `extraDepTarget`. -/
|
||||
abbrev Package.extraDepFacet := `extraDep
|
||||
package_data extraDep : ActiveOpaqueTarget
|
||||
package_data extraDep : BuildJob Unit
|
||||
|
||||
/-! ## Target Facets -/
|
||||
|
||||
/-- A Lean library's Lean libraries. -/
|
||||
abbrev LeanLib.leanFacet := `lean
|
||||
library_data lean : ActiveOpaqueTarget
|
||||
library_data lean : BuildJob Unit
|
||||
|
||||
/-- A Lean library's static binary. -/
|
||||
abbrev LeanLib.staticFacet := `static
|
||||
library_data static : ActiveFileTarget
|
||||
library_data static : BuildJob FilePath
|
||||
|
||||
/-- A Lean library's shared binary. -/
|
||||
abbrev LeanLib.sharedFacet := `shared
|
||||
library_data shared : ActiveFileTarget
|
||||
library_data shared : BuildJob FilePath
|
||||
|
||||
/-- A Lean binary executable. -/
|
||||
abbrev LeanExe.exeFacet := `leanExe
|
||||
target_data leanExe : ActiveFileTarget
|
||||
target_data leanExe : BuildJob FilePath
|
||||
|
||||
/-- A external library's static binary. -/
|
||||
abbrev ExternLib.staticFacet := `externLib.static
|
||||
target_data externLib.static : ActiveFileTarget
|
||||
target_data externLib.static : BuildJob FilePath
|
||||
|
||||
/-- A external library's shared binary. -/
|
||||
abbrev ExternLib.sharedFacet := `externLib.shared
|
||||
target_data externLib.shared : ActiveFileTarget
|
||||
target_data externLib.shared : BuildJob FilePath
|
||||
|
||||
/-- A external library's dynlib. -/
|
||||
abbrev ExternLib.dynlibFacet := `externLib.dynlib
|
||||
target_data externLib.dynlib : ActiveDynlibTarget
|
||||
target_data externLib.dynlib : BuildJob Dynlib
|
||||
|
|
|
|||
|
|
@ -35,22 +35,22 @@ as "Lean-only". Otherwise, also build `.c` files.
|
|||
def Package.buildImportsAndDeps (imports : List String) (self : Package) : BuildM (Array FilePath) := do
|
||||
if imports.isEmpty then
|
||||
-- build the package's (and its dependencies') `extraDepTarget`
|
||||
self.extraDep.build >>= (·.buildOpaque)
|
||||
self.extraDep.build >>= (·.materialize)
|
||||
return #[]
|
||||
else
|
||||
-- build local imports from list
|
||||
let mods := (← getWorkspace).processImportList imports
|
||||
let (importTargets, bStore) ← RecBuildM.runIn {} <| mods.mapM fun mod =>
|
||||
if mod.shouldPrecompile then
|
||||
(discard ·.task) <$> buildIndexTop mod.dynlib
|
||||
(discard ·.toJob) <$> buildIndexTop mod.dynlib
|
||||
else
|
||||
(discard ·.task) <$> buildIndexTop mod.leanBin
|
||||
let dynlibTargets := bStore.collectModuleFacetArray Module.dynlibFacet
|
||||
let externLibTargets := bStore.collectSharedExternLibs
|
||||
importTargets.forM (liftM <| await ·)
|
||||
(discard ·.toJob) <$> buildIndexTop mod.leanBin
|
||||
let dynlibJobs := bStore.collectModuleFacetArray Module.dynlibFacet
|
||||
let externLibJobs := bStore.collectSharedExternLibs
|
||||
importTargets.forM (·.await)
|
||||
-- NOTE: Unix requires the full file name of the dynlib (Windows doesn't care)
|
||||
let dynlibs ← dynlibTargets.mapM fun dynlib => do
|
||||
return FilePath.mk <| nameToSharedLib (← dynlib.build).toString
|
||||
let externLibs ← externLibTargets.mapM (·.build)
|
||||
let dynlibs ← dynlibJobs.mapM fun dynlib => do
|
||||
return FilePath.mk <| nameToSharedLib (← dynlib.await)
|
||||
let externLibs ← externLibJobs.mapM (·.await)
|
||||
-- NOTE: Lean wants the external library symbols before module symbols
|
||||
return externLibs ++ dynlibs
|
||||
|
|
|
|||
|
|
@ -45,7 +45,7 @@ def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key)
|
|||
| .customTarget pkg target =>
|
||||
if let some config := pkg.findTargetConfig? target then
|
||||
if h : pkg.name = config.package ∧ target = config.name then
|
||||
have h' : CustomData (pkg.name, target) = ActiveBuildTarget config.resultType := by simp [h]
|
||||
have h' : CustomData (pkg.name, target) = BuildJob config.resultType := by simp [h]
|
||||
liftM <| cast (by rw [← h']) <| config.target.activate
|
||||
else
|
||||
error "target's name in the configuration does not match the name it was registered with"
|
||||
|
|
@ -95,19 +95,19 @@ export BuildInfo (build)
|
|||
|
||||
/-- An opaque target that builds the info in a fresh build store. -/
|
||||
@[inline] def BuildInfo.target (self : BuildInfo)
|
||||
[FamilyDef BuildData self.key (ActiveBuildTarget α)] : BuildTarget α :=
|
||||
Target.mk <| (self.build <&> (·.task)) |>.catchFailure fun _ => pure failure
|
||||
[FamilyDef BuildData self.key (BuildJob α)] : BuildTarget α :=
|
||||
Target.mk <| self.build |>.catchFailure fun _ => pure failure
|
||||
|
||||
/-- A smart constructor for facet configurations that generate targets. -/
|
||||
@[inline] def mkFacetTargetConfig (build : ι → IndexBuildM (ActiveBuildTarget α))
|
||||
[h : FamilyDef Fam facet (ActiveBuildTarget α)] : FacetConfig Fam ι facet where
|
||||
/-- A smart constructor for facet configurations that generate CLI targets. -/
|
||||
@[inline] def mkFacetTargetConfig (build : ι → IndexBuildM (BuildJob α))
|
||||
[h : FamilyDef Fam facet (BuildJob α)] : FacetConfig Fam ι facet where
|
||||
build := cast (by rw [← h.family_key_eq_type]) build
|
||||
getJob? := some fun data => discard <| ofFamily data
|
||||
|
||||
/-! ### Lean Executable Builds -/
|
||||
|
||||
@[inline] protected def LeanExe.build (self : LeanExe) : BuildM ActiveFileTarget :=
|
||||
@[inline] protected def LeanExe.build (self : LeanExe) : BuildM (BuildJob FilePath) :=
|
||||
self.exe.build
|
||||
|
||||
@[inline] protected def LeanExe.recBuild (self : LeanExe) : IndexBuildM ActiveFileTarget :=
|
||||
@[inline] protected def LeanExe.recBuild (self : LeanExe) : IndexBuildM (BuildJob FilePath) :=
|
||||
self.exe.recBuild
|
||||
|
|
|
|||
99
Lake/Build/Job.lean
Normal file
99
Lake/Build/Job.lean
Normal file
|
|
@ -0,0 +1,99 @@
|
|||
/-
|
||||
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.Async
|
||||
import Lake.Build.Trace
|
||||
import Lake.Build.Context
|
||||
|
||||
open System
|
||||
namespace Lake
|
||||
|
||||
/-- A Lake job. -/
|
||||
abbrev Job α := OptionIOTask α
|
||||
|
||||
/-- The monad of Lake jobs. -/
|
||||
abbrev JobM := BuildM
|
||||
|
||||
/-- The monad of a finished Lake job. -/
|
||||
abbrev ResultM := OptionIO
|
||||
|
||||
namespace Job
|
||||
|
||||
@[inline] def nil : Job Unit :=
|
||||
pure ()
|
||||
|
||||
@[inline] protected def await (self : Job α) : ResultM α :=
|
||||
await self
|
||||
|
||||
@[inline] protected def bindSync
|
||||
(self : Job α) (f : α → JobM β) : SchedulerM (Job β) :=
|
||||
bindSync self f
|
||||
|
||||
@[inline] protected def bindAsync
|
||||
(self : Job α) (f : α → SchedulerM (Job β)) : SchedulerM (Job β) :=
|
||||
bindAsync self f
|
||||
|
||||
end Job
|
||||
|
||||
/-- A Lake build job. -/
|
||||
abbrev BuildJob α := Job (α × BuildTrace)
|
||||
|
||||
namespace BuildJob
|
||||
|
||||
@[inline] def mk (job : Job (α × BuildTrace)) : BuildJob α :=
|
||||
job
|
||||
|
||||
@[inline] def ofJob (self : Job BuildTrace) : BuildJob Unit :=
|
||||
mk <| ((), ·) <$> self
|
||||
|
||||
@[inline] def toJob (self : BuildJob α) : Job (α × BuildTrace) :=
|
||||
self
|
||||
|
||||
@[inline] def nil : BuildJob Unit :=
|
||||
mk <| pure ((), nilTrace)
|
||||
|
||||
@[inline] protected def pure (a : α) : BuildJob α :=
|
||||
mk <| pure (a, nilTrace)
|
||||
|
||||
instance : Pure BuildJob := ⟨BuildJob.pure⟩
|
||||
|
||||
@[inline] protected def bindSync
|
||||
(self : BuildJob α) (f : α → BuildTrace → JobM β) : SchedulerM (Job β) :=
|
||||
self.toJob.bindSync fun (a, t) => f a t
|
||||
|
||||
@[inline] protected def bindAsync
|
||||
(self : BuildJob α) (f : α → BuildTrace → SchedulerM (Job β)) : SchedulerM (Job β) :=
|
||||
self.toJob.bindAsync fun (a, t) => f a t
|
||||
|
||||
@[inline] protected def await (self : BuildJob α) : ResultM α :=
|
||||
(·.1) <$> await self.toJob
|
||||
|
||||
instance : Await BuildJob ResultM := ⟨BuildJob.await⟩
|
||||
|
||||
@[inline] def materialize (self : BuildJob α) : ResultM Unit :=
|
||||
discard <| await self.toJob
|
||||
|
||||
def mix (t1 : BuildJob α) (t2 : BuildJob β) : BaseIO (BuildJob Unit) :=
|
||||
mk <$> seqWithAsync (fun (_,t) (_,t') => ((), mixTrace t t')) t1.toJob t2.toJob
|
||||
|
||||
def mixList (jobs : List (BuildJob α)) : BaseIO (BuildJob Unit) := ofJob <$> do
|
||||
jobs.foldrM (init := pure nilTrace) fun j a =>
|
||||
seqWithAsync (fun (_,t') t => mixTrace t t') j.toJob a
|
||||
|
||||
def mixArray (jobs : Array (BuildJob α)) : BaseIO (BuildJob Unit) := ofJob <$> do
|
||||
jobs.foldlM (init := pure nilTrace) fun a j =>
|
||||
seqWithAsync (fun t (_,t') => mixTrace t t') a j.toJob
|
||||
|
||||
protected def seqWithAsync
|
||||
(f : α → β → γ) (t1 : BuildJob α) (t2 : BuildJob β) : BaseIO (BuildJob γ) :=
|
||||
mk <$> seqWithAsync (fun (a,t) (b,t') => (f a b, mixTrace t t')) t1.toJob t2.toJob
|
||||
|
||||
instance : SeqWithAsync BaseIO BuildJob := ⟨BuildJob.seqWithAsync⟩
|
||||
|
||||
def collectList (jobs : List (BuildJob α)) : BaseIO (BuildJob (List α)) :=
|
||||
jobs.foldrM (seqWithAsync List.cons) (pure [])
|
||||
|
||||
def collectArray (jobs : Array (BuildJob α)) : BaseIO (BuildJob (Array α)) :=
|
||||
jobs.foldlM (seqWithAsync Array.push) (pure #[])
|
||||
|
|
@ -27,16 +27,15 @@ def LeanLib.recBuildLocalModules
|
|||
return results
|
||||
|
||||
protected def LeanLib.recBuildLean
|
||||
(self : LeanLib) : IndexBuildM ActiveOpaqueTarget := do
|
||||
ActiveTarget.collectOpaqueArray (ι := PUnit) <|
|
||||
← self.recBuildLocalModules #[Module.leanBinFacet]
|
||||
(self : LeanLib) : IndexBuildM (BuildJob Unit) := do
|
||||
BuildJob.mixArray (α := Unit) <| ← self.recBuildLocalModules #[Module.leanBinFacet]
|
||||
|
||||
/-- The `LibraryFacetConfig` for the builtin `leanFacet`. -/
|
||||
def LeanLib.leanFacetConfig : LibraryFacetConfig leanFacet :=
|
||||
mkFacetTargetConfig (·.recBuildLean)
|
||||
|
||||
protected def LeanLib.recBuildStatic
|
||||
(self : LeanLib) : IndexBuildM ActiveFileTarget := do
|
||||
(self : LeanLib) : IndexBuildM (BuildJob FilePath) := do
|
||||
let oTargets := (← self.recBuildLocalModules self.nativeFacets).map Target.active
|
||||
staticLibTarget self.staticLibFile oTargets |>.activate
|
||||
|
||||
|
|
@ -51,12 +50,12 @@ Build and collect the local object files and external libraries
|
|||
of a library and its modules' imports.
|
||||
-/
|
||||
def LeanLib.recBuildLinks
|
||||
(self : LeanLib) : IndexBuildM (Array ActiveFileTarget) := do
|
||||
(self : LeanLib) : IndexBuildM (Array (BuildJob FilePath)) := do
|
||||
-- Build and collect modules
|
||||
let mut jobs := #[]
|
||||
let mut pkgs := #[]
|
||||
let mut pkgSet := PackageSet.empty
|
||||
let mut modSet := ModuleSet.empty
|
||||
let mut targets := #[]
|
||||
let mods ← self.getModuleArray
|
||||
for mod in mods do
|
||||
let (_, mods) ← mod.imports.recBuild
|
||||
|
|
@ -68,19 +67,19 @@ def LeanLib.recBuildLinks
|
|||
pkgs := pkgs.push mod.pkg
|
||||
if self.isLocalModule mod.name then
|
||||
for facet in self.nativeFacets do
|
||||
targets := targets.push <| ← recBuild <| mod.facet facet.name
|
||||
jobs := jobs.push <| ← recBuild <| mod.facet facet.name
|
||||
modSet := modSet.insert mod
|
||||
-- Build and collect external library targets
|
||||
-- Build and collect external library jobs
|
||||
for pkg in pkgs do
|
||||
let externLibTargets ← pkg.externLibs.mapM (·.shared.recBuild)
|
||||
for target in externLibTargets do
|
||||
targets := targets.push target
|
||||
return targets
|
||||
let externLibJobs ← pkg.externLibs.mapM (·.shared.recBuild)
|
||||
for job in externLibJobs do
|
||||
jobs := jobs.push job
|
||||
return jobs
|
||||
|
||||
protected def LeanLib.recBuildShared
|
||||
(self : LeanLib) : IndexBuildM ActiveFileTarget := do
|
||||
let linkTargets := (← self.recBuildLinks).map Target.active
|
||||
leanSharedLibTarget self.sharedLibFile linkTargets self.linkArgs |>.activate
|
||||
(self : LeanLib) : IndexBuildM (BuildJob FilePath) := do
|
||||
let linkJobs := (← self.recBuildLinks).map Target.active
|
||||
leanSharedLibTarget self.sharedLibFile linkJobs self.linkArgs |>.activate
|
||||
|
||||
/-- The `LibraryFacetConfig` for the builtin `sharedFacet`. -/
|
||||
def LeanLib.sharedFacetConfig : LibraryFacetConfig sharedFacet :=
|
||||
|
|
|
|||
|
|
@ -10,8 +10,6 @@ open System
|
|||
|
||||
namespace Lake
|
||||
|
||||
/-! # Solo Module Targets -/
|
||||
|
||||
def Module.buildUnlessUpToDate (mod : Module)
|
||||
(dynlibPath : SearchPath) (dynlibs : Array FilePath)
|
||||
(depTrace : BuildTrace) (leanOnly : Bool) : BuildM BuildTrace := do
|
||||
|
|
@ -32,23 +30,23 @@ def Module.buildUnlessUpToDate (mod : Module)
|
|||
modTrace.writeToFile mod.traceFile
|
||||
return mixTrace (← computeTrace mod) depTrace
|
||||
|
||||
/-- Compute library directories and build external library targets of the given packages. -/
|
||||
/-- Compute library directories and build external library Jobs of the given packages. -/
|
||||
def recBuildExternalDynlibs (pkgs : Array Package)
|
||||
: IndexBuildM (Array ActiveDynlibTarget × Array FilePath) := do
|
||||
: IndexBuildM (Array (BuildJob Dynlib) × Array FilePath) := do
|
||||
let mut libDirs := #[]
|
||||
let mut targets : Array ActiveDynlibTarget := #[]
|
||||
let mut Jobs : Array (BuildJob Dynlib) := #[]
|
||||
for pkg in pkgs do
|
||||
libDirs := libDirs.push pkg.libDir
|
||||
targets := targets.append <| ← pkg.externLibs.mapM (·.dynlib.recBuild)
|
||||
return (targets, libDirs)
|
||||
Jobs := Jobs.append <| ← pkg.externLibs.mapM (·.dynlib.recBuild)
|
||||
return (Jobs, libDirs)
|
||||
|
||||
/-- Build the dynlibs of the imports that want precompilation (and *their* imports). -/
|
||||
def recBuildPrecompileDynlibs (pkg : Package) (imports : Array Module)
|
||||
: IndexBuildM (Array ActiveFileTarget × Array ActiveDynlibTarget × Array FilePath) := do
|
||||
: IndexBuildM (Array (BuildJob String) × Array (BuildJob Dynlib) × Array FilePath) := do
|
||||
let mut pkgs := #[]
|
||||
let mut pkgSet := PackageSet.empty.insert pkg
|
||||
let mut modSet := ModuleSet.empty
|
||||
let mut targets := #[]
|
||||
let mut Jobs := #[]
|
||||
for imp in imports do
|
||||
if imp.shouldPrecompile then
|
||||
let (_, transImports) ← imp.imports.recBuild
|
||||
|
|
@ -58,8 +56,8 @@ def recBuildPrecompileDynlibs (pkg : Package) (imports : Array Module)
|
|||
pkgs := pkgs.push mod.pkg
|
||||
unless modSet.contains mod do
|
||||
modSet := modSet.insert mod
|
||||
targets := targets.push <| ← mod.dynlib.recBuild
|
||||
return (targets, ← recBuildExternalDynlibs <| pkgs.push pkg)
|
||||
Jobs := Jobs.push <| ← mod.dynlib.recBuild
|
||||
return (Jobs, ← recBuildExternalDynlibs <| pkgs.push pkg)
|
||||
|
||||
variable [MonadLiftT BuildM m]
|
||||
|
||||
|
|
@ -71,60 +69,60 @@ deriving Inhabited, Repr, DecidableEq
|
|||
/--
|
||||
Recursively build a module and its (transitive, local) imports,
|
||||
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
|
||||
requested artifact is `c`. Returns an build job producing the requested
|
||||
artifact.
|
||||
-/
|
||||
def Module.recBuildLean (mod : Module) (art : LeanArtifact)
|
||||
: IndexBuildM (ActiveBuildTarget (if art = .leanBin then PUnit else FilePath)) := do
|
||||
: IndexBuildM (BuildJob (if art = .leanBin then PUnit else FilePath)) := do
|
||||
let leanOnly := mod.isLeanOnly ∧ art ≠ .c
|
||||
|
||||
-- Compute and build dependencies
|
||||
let extraDepTarget ← mod.pkg.extraDep.recBuild
|
||||
let extraDepJob ← mod.pkg.extraDep.recBuild
|
||||
let (imports, _) ← mod.imports.recBuild
|
||||
let (modTargets, externTargets, libDirs) ← recBuildPrecompileDynlibs mod.pkg imports
|
||||
let importTarget ← ActiveTarget.collectOpaqueArray <| ← imports.mapM (·.leanBin.recBuild)
|
||||
let externDynlibsTarget ← ActiveTarget.collectArray externTargets
|
||||
let modDynlibsTarget ← ActiveTarget.collectArray modTargets
|
||||
let (modJobs, externJobs, libDirs) ← recBuildPrecompileDynlibs mod.pkg imports
|
||||
let importJob ← BuildJob.mixArray <| ← imports.mapM (·.leanBin.recBuild)
|
||||
let externDynlibsJob ← BuildJob.collectArray externJobs
|
||||
let modDynlibsJob ← BuildJob.collectArray modJobs
|
||||
|
||||
-- Build Module
|
||||
let modTarget : ActiveOpaqueTarget ← show SchedulerM _ from do
|
||||
importTarget.bindOpaqueAsync fun importTrace => do
|
||||
modDynlibsTarget.bindAsync fun modDynlibs modTrace => do
|
||||
externDynlibsTarget.bindAsync fun externDynlibs externTrace => do
|
||||
extraDepTarget.bindOpaqueSync fun depTrace => do
|
||||
let modJob : BuildJob Unit ← show SchedulerM _ from do
|
||||
importJob.bindAsync fun _ importTrace => do
|
||||
modDynlibsJob.bindAsync fun modDynlibs modTrace => do
|
||||
externDynlibsJob.bindAsync fun externDynlibs externTrace => do
|
||||
extraDepJob.bindSync fun _ depTrace => do
|
||||
let depTrace := importTrace.mix <| modTrace.mix <| externTrace.mix depTrace
|
||||
let dynlibPath := libDirs ++ externDynlibs.filterMap ( ·.1)
|
||||
-- NOTE: Lean wants the external library symbols before module symbols
|
||||
-- NOTE: Unix requires the full file name of the dynlib (Windows doesn't care)
|
||||
let dynlibs :=
|
||||
externDynlibs.map (.mk <| nameToSharedLib ·.2) ++
|
||||
modDynlibs.map (.mk <| nameToSharedLib ·.toString)
|
||||
modDynlibs.map (.mk <| nameToSharedLib ·)
|
||||
let trace ← mod.buildUnlessUpToDate dynlibPath.toList dynlibs depTrace leanOnly
|
||||
return ((), trace)
|
||||
|
||||
-- Save All Resulting Targets & Return Requested One
|
||||
store mod.leanBin.key modTarget
|
||||
let oleanTarget ← modTarget.bindOpaqueSync fun depTrace =>
|
||||
-- Save All Resulting Jobs & Return Requested One
|
||||
store mod.leanBin.key modJob
|
||||
let oleanJob ← modJob.bindSync fun _ depTrace =>
|
||||
return (mod.oleanFile, mixTrace (← computeTrace mod.oleanFile) depTrace)
|
||||
store mod.olean.key <| oleanTarget
|
||||
let ileanTarget ← modTarget.bindOpaqueSync fun depTrace =>
|
||||
store mod.olean.key <| oleanJob
|
||||
let ileanJob ← modJob.bindSync fun _ depTrace =>
|
||||
return (mod.ileanFile, mixTrace (← computeTrace mod.ileanFile) depTrace)
|
||||
store mod.ilean.key <| ileanTarget
|
||||
store mod.ilean.key <| ileanJob
|
||||
if h : leanOnly then
|
||||
have : art ≠ .c := h.2
|
||||
return match art with
|
||||
| .leanBin => modTarget
|
||||
| .olean => oleanTarget
|
||||
| .ilean => ileanTarget
|
||||
| .leanBin => modJob
|
||||
| .olean => oleanJob
|
||||
| .ilean => ileanJob
|
||||
else
|
||||
let cTarget ← modTarget.bindOpaqueSync fun _ =>
|
||||
let cJob ← modJob.bindSync fun _ _ =>
|
||||
return (mod.cFile, mixTrace (← computeTrace mod.cFile) (← getLeanTrace))
|
||||
store mod.c.key cTarget
|
||||
store mod.c.key cJob
|
||||
return match art with
|
||||
| .leanBin => modTarget
|
||||
| .olean => oleanTarget
|
||||
| .ilean => ileanTarget
|
||||
| .c => cTarget
|
||||
| .leanBin => modJob
|
||||
| .olean => oleanJob
|
||||
| .ilean => ileanJob
|
||||
| .c => cJob
|
||||
|
||||
/-- The `ModuleFacetConfig` for the builtin `leanBinFacet`. -/
|
||||
def Module.leanBinFacetConfig : ModuleFacetConfig leanBinFacet :=
|
||||
|
|
@ -143,9 +141,9 @@ 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
|
||||
let cTarget := Target.active (← self.c.recBuild)
|
||||
leanOFileTarget self.oFile cTarget self.leancArgs |>.activate
|
||||
def Module.recBuildLeanO (self : Module) : IndexBuildM (BuildJob FilePath) := do
|
||||
let cJob := Target.active (← self.c.recBuild)
|
||||
leanOFileTarget self.oFile cJob self.leancArgs |>.activate
|
||||
|
||||
/-- The `ModuleFacetConfig` for the builtin `oFacet`. -/
|
||||
def Module.oFacetConfig : ModuleFacetConfig oFacet :=
|
||||
|
|
@ -182,43 +180,43 @@ def Module.importFacetConfig : ModuleFacetConfig importFacet :=
|
|||
|
||||
/-- Build the dynlibs of all imports. -/
|
||||
def recBuildDynlibs (pkg : Package) (imports : Array Module)
|
||||
: IndexBuildM (Array ActiveFileTarget × Array ActiveDynlibTarget × Array FilePath) := do
|
||||
: IndexBuildM (Array (BuildJob String) × Array (BuildJob Dynlib) × Array FilePath) := do
|
||||
let mut pkgs := #[]
|
||||
let mut pkgSet := PackageSet.empty.insert pkg
|
||||
let mut targets := #[]
|
||||
let mut Jobs := #[]
|
||||
for imp in imports do
|
||||
unless pkgSet.contains imp.pkg do
|
||||
pkgSet := pkgSet.insert imp.pkg
|
||||
pkgs := pkgs.push imp.pkg
|
||||
targets := targets.push <| ← imp.dynlib.recBuild
|
||||
return (targets, ← recBuildExternalDynlibs <| pkgs.push pkg)
|
||||
Jobs := Jobs.push <| ← imp.dynlib.recBuild
|
||||
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 ActiveFileTarget := do
|
||||
def Module.recBuildDynlib (mod : Module) : IndexBuildM (BuildJob String) := do
|
||||
|
||||
-- Compute dependencies
|
||||
let (_, transImports) ← mod.imports.recBuild
|
||||
let linkTargets ← mod.nativeFacets.mapM (recBuild <| mod.facet ·.name)
|
||||
let (modTargets, externTargets, pkgLibDirs) ← recBuildDynlibs mod.pkg transImports
|
||||
let linkJobs ← mod.nativeFacets.mapM (recBuild <| mod.facet ·.name)
|
||||
let (modJobs, externJobs, pkgLibDirs) ← recBuildDynlibs mod.pkg transImports
|
||||
|
||||
-- Collect targets
|
||||
let linksTarget ← ActiveTarget.collectArray linkTargets
|
||||
let modDynlibsTarget ← ActiveTarget.collectArray modTargets
|
||||
let externDynlibsTarget : ActiveBuildTarget _ ← ActiveTarget.collectArray externTargets
|
||||
-- Collect Jobs
|
||||
let linksJob ← BuildJob.collectArray linkJobs
|
||||
let modDynlibsJob ← BuildJob.collectArray modJobs
|
||||
let externDynlibsJob ← BuildJob.collectArray externJobs
|
||||
|
||||
-- Build dynlib
|
||||
show SchedulerM _ from do
|
||||
linksTarget.bindAsync fun links oTrace => do
|
||||
modDynlibsTarget.bindAsync fun modDynlibs libTrace => do
|
||||
externDynlibsTarget.bindSync fun externDynlibs externTrace => do
|
||||
let libNames := modDynlibs ++ externDynlibs.map (.mk ·.2)
|
||||
linksJob.bindAsync fun links oTrace => do
|
||||
modDynlibsJob.bindAsync fun modDynlibs libTrace => do
|
||||
externDynlibsJob.bindSync fun externDynlibs externTrace => do
|
||||
let libNames := modDynlibs ++ externDynlibs.map (·.2)
|
||||
let libDirs := pkgLibDirs ++ externDynlibs.filterMap (·.1)
|
||||
let depTrace := oTrace.mix <| libTrace.mix externTrace
|
||||
let trace ← buildFileUnlessUpToDate mod.dynlibFile depTrace do
|
||||
let args := links.map toString ++
|
||||
libDirs.map (s!"-L{·}") ++ libNames.map (s!"-l{·}")
|
||||
compileSharedLib mod.dynlibFile args (← getLeanc)
|
||||
return (.mk mod.dynlibName, trace)
|
||||
return (mod.dynlibName, trace)
|
||||
|
||||
/-- The `ModuleFacetConfig` for the builtin `dynlibFacet`. -/
|
||||
def Module.dynlibFacetConfig : ModuleFacetConfig dynlibFacet :=
|
||||
|
|
|
|||
|
|
@ -26,11 +26,11 @@ 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
|
||||
def Package.recBuildExtraDepTargets (self : Package) : IndexBuildM (BuildJob Unit) := do
|
||||
let mut job := BuildJob.nil
|
||||
for dep in self.deps do
|
||||
target ← target.mixOpaqueAsync (← dep.extraDep.recBuild)
|
||||
target.mixOpaqueAsync <| ← self.extraDepTarget.activate
|
||||
job ← job.mix (← dep.extraDep.recBuild)
|
||||
job.mix <| ← self.extraDepTarget.activate
|
||||
|
||||
/-- The `PackageFacetConfig` for the builtin `dynlibFacet`. -/
|
||||
def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
|
||||
|
|
|
|||
|
|
@ -9,119 +9,43 @@ import Lake.Build.Trace
|
|||
open System
|
||||
namespace Lake
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
/-! # Active Targets -/
|
||||
--------------------------------------------------------------------------------
|
||||
structure Target.{u,v,w} (α : Type u) (n : Type v → Type w) (k : Type u → Type v) (τ : Type u) where
|
||||
task : n (k (α × τ))
|
||||
|
||||
def ActiveTarget.{u,v} (ι : Type u) (k : Type u → Type v) (τ : Type u) :=
|
||||
k (ι × τ)
|
||||
|
||||
namespace ActiveTarget
|
||||
|
||||
@[inline] def mk (task : k (ι × τ)) : ActiveTarget ι k τ :=
|
||||
task
|
||||
|
||||
@[inline] def task (target : ActiveTarget ι k τ) : k (ι × τ) :=
|
||||
target
|
||||
|
||||
instance [Inhabited ι] [Inhabited τ] [Pure k] : Inhabited (ActiveTarget ι k τ) :=
|
||||
⟨mk <| pure default⟩
|
||||
|
||||
@[inline] def «opaque» [Functor k] (task : k t) : ActiveTarget PUnit k t :=
|
||||
mk <| ((), ·) <$> task
|
||||
|
||||
@[inline] def nil [NilTrace τ] [Pure k] : ActiveTarget PUnit k τ :=
|
||||
mk <| pure ((), nilTrace)
|
||||
|
||||
@[inline] protected def bindSync [BindSync m n k]
|
||||
(self : ActiveTarget ι k α) (f : ι → α → m β) : n (k β) :=
|
||||
bindSync self fun (i, a) => f i a
|
||||
|
||||
@[inline] protected def bindOpaqueSync [BindSync m n k]
|
||||
(self : ActiveTarget ι k α) (f : α → m β) : n (k β) :=
|
||||
bindSync self fun (_, a) => f a
|
||||
|
||||
@[inline] protected def bindAsync [BindAsync n k]
|
||||
(self : ActiveTarget ι k α) (f : ι → α → n (k β)) : n (k β) :=
|
||||
bindAsync self fun (i, a) => f i a
|
||||
|
||||
@[inline] protected def bindOpaqueAsync [BindAsync n k]
|
||||
(self : ActiveTarget ι k α) (f : α → n (k β)) : n (k β) :=
|
||||
bindAsync self fun (_, a) => f a
|
||||
|
||||
@[inline] def build
|
||||
[Await k n] [MonadLiftT n m] [Functor m] (self : ActiveTarget ι k τ) : m ι :=
|
||||
(·.1) <$> liftM (await self.task)
|
||||
|
||||
@[inline] def buildOpaque
|
||||
[Await k n] [MonadLiftT n m] [Functor m] (self : ActiveTarget ι k τ) : m PUnit :=
|
||||
discard <| liftM (await self.task)
|
||||
|
||||
variable [MixTrace τ] [SeqWithAsync n k] [MonadLiftT n m] [Monad m]
|
||||
|
||||
def mixOpaqueAsync
|
||||
(t1 : ActiveTarget α k τ) (t2 : ActiveTarget β k τ) : m (ActiveTarget PUnit k τ) :=
|
||||
mk <$> liftM (seqWithAsync (fun (_,t) (_,t') => ((), mixTrace t t')) t1 t2)
|
||||
|
||||
variable [NilTrace τ] [Monad n] [Pure k]
|
||||
|
||||
def collectList (targets : List (ActiveTarget ι k τ)) : m (ActiveTarget (List ι) k τ) := mk <$> do
|
||||
liftM <| foldLeftListAsync (fun (i,t') (a,t) => (i :: a, mixTrace t t')) ([], nilTrace) targets
|
||||
|
||||
def collectArray (targets : Array (ActiveTarget ι k τ)) : m (ActiveTarget (Array ι) k τ) := mk <$> do
|
||||
liftM <| foldRightArrayAsync (fun (a,t) (i,t') => (a.push i, mixTrace t t')) (#[], nilTrace) targets
|
||||
|
||||
variable [Functor k]
|
||||
|
||||
def collectOpaqueList (targets : List (ActiveTarget ι k τ)) : m (ActiveTarget PUnit k τ) := «opaque» <$> do
|
||||
liftM <| foldLeftListAsync (fun (_,t') t => mixTrace t t') nilTrace targets
|
||||
|
||||
def collectOpaqueArray (targets : Array (ActiveTarget ι k τ)) : m (ActiveTarget PUnit k τ) := «opaque» <$> do
|
||||
liftM <| foldRightArrayAsync (fun t (_,t') => mixTrace t t') nilTrace targets
|
||||
|
||||
end ActiveTarget
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
/-! # Inactive Target -/
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
structure Target.{u,v,w} (ι : Type u) (n : Type v → Type w) (k : Type u → Type v) (τ : Type u) where
|
||||
task : n (k (ι × τ))
|
||||
|
||||
instance [Inhabited ι] [Inhabited τ] [Pure n] [Pure k] : Inhabited (Target ι n k τ) :=
|
||||
instance [Inhabited α] [Inhabited τ] [Pure n] [Pure k] : Inhabited (Target α n k τ) :=
|
||||
⟨⟨pure (pure default)⟩⟩
|
||||
|
||||
namespace Target
|
||||
|
||||
@[inline] def active [Pure n] (target : ActiveTarget ι k τ) : Target ι n k τ :=
|
||||
@[inline] def active [Pure n] (target : k (α × τ)) : Target α n k τ :=
|
||||
mk <| pure target
|
||||
|
||||
@[inline] def nil [NilTrace τ] [Pure n] [Pure k] : Target PUnit n k τ :=
|
||||
mk <| pure <| pure <| ((), nilTrace)
|
||||
|
||||
@[inline] def activate [Functor n] (self : Target ι n k τ) : n (ActiveTarget ι k τ) :=
|
||||
(.mk ·) <$> self.task
|
||||
@[inline] def activate (self : Target α n k τ) : n (k (α × τ)) :=
|
||||
self.task
|
||||
|
||||
@[inline] def materializeAsync [Functor n] [Functor k] (self : Target ι n k τ) : n (k τ) :=
|
||||
@[inline] def materializeAsync [Functor n] [Functor k] (self : Target α n k τ) : n (k τ) :=
|
||||
((·.2) <$> ·) <$> self.task
|
||||
|
||||
def materialize [Await k m'] [MonadLiftT m' m] [MonadLiftT n m] [Functor m] [Bind m] (self : Target ι n k τ) : m τ :=
|
||||
def materialize [Await k m'] [MonadLiftT m' m] [MonadLiftT n m] [Functor m] [Bind m] (self : Target α n k τ) : m τ :=
|
||||
liftM self.task >>= fun t => (·.2) <$> liftM (await t)
|
||||
|
||||
@[inline] protected def bindSync [BindSync m n k] [Bind n]
|
||||
(self : Target ι n k τ) (f : ι → τ → m β) : n (k β) :=
|
||||
(self : Target α n k τ) (f : α → τ → m β) : n (k β) :=
|
||||
self.task >>= fun tk => bindSync tk fun (i,t) => f i t
|
||||
|
||||
@[inline] protected def bindOpaqueSync
|
||||
[BindSync m n k] [Bind n] (self : Target ι n k τ) (f : τ → m β) : n (k β) :=
|
||||
[BindSync m n k] [Bind n] (self : Target α n k τ) (f : τ → m β) : n (k β) :=
|
||||
self.task >>= fun tk => bindSync tk fun (_,t) => f t
|
||||
|
||||
@[inline] protected def bindAsync
|
||||
[BindAsync n k] [Bind n] (self : Target ι n k τ) (f : ι → τ → n (k β)) : n (k β) :=
|
||||
[BindAsync n k] [Bind n] (self : Target α n k τ) (f : α → τ → n (k β)) : n (k β) :=
|
||||
self.task >>= fun tk => bindAsync tk fun (i,t) => f i t
|
||||
|
||||
@[inline] protected def bindOpaqueAsync
|
||||
[BindAsync n k] [Bind n] (self : Target ι n k τ) (f : τ → n (k β)) : n (k β) :=
|
||||
[BindAsync n k] [Bind n] (self : Target α n k τ) (f : τ → n (k β)) : n (k β) :=
|
||||
self.task >>= fun tk => bindAsync tk fun (_,t) => f t
|
||||
|
||||
def mixOpaqueAsync
|
||||
|
|
@ -131,31 +55,29 @@ def mixOpaqueAsync
|
|||
let tk2 ← t2.materializeAsync
|
||||
((fun t => ((),t)) <$> ·) <$> seqWithAsync mixTrace tk1 tk2
|
||||
|
||||
section
|
||||
variable [NilTrace τ] [MixTrace τ]
|
||||
variable [SeqWithAsync n' k] [Monad n'] [MonadLiftT n' n] [Monad n] [Pure k] [Functor k]
|
||||
|
||||
def materializeListAsync (targets : List (Target ι n k τ)) : n (k τ) := do
|
||||
def materializeListAsync (targets : List (Target α n k τ)) : n (k τ) := do
|
||||
liftM <| foldRightListAsync mixTrace nilTrace (← targets.mapM (·.materializeAsync))
|
||||
|
||||
def materializeArrayAsync (targets : Array (Target ι n k τ)) : n (k τ) := do
|
||||
def materializeArrayAsync (targets : Array (Target α n k τ)) : n (k τ) := do
|
||||
liftM <| foldRightArrayAsync mixTrace nilTrace (← targets.mapM (·.materializeAsync))
|
||||
|
||||
def collectList (targets : List (Target ι n k τ)) : Target (List ι) n k τ := mk do
|
||||
def collectList (targets : List (Target α n k τ)) : Target (List α) n k τ := mk do
|
||||
let tasks ← targets.mapM (·.task)
|
||||
let f := fun (i,t') (a,t) => (i :: a, mixTrace t t')
|
||||
liftM <| foldLeftListAsync f ([], nilTrace) tasks
|
||||
|
||||
def collectArray (targets : Array (Target ι n k τ)) : Target (Array ι) n k τ := mk do
|
||||
def collectArray (targets : Array (Target α n k τ)) : Target (Array α) n k τ := mk do
|
||||
let tasks ← targets.mapM (·.task)
|
||||
let f := fun (a,t) (i,t') => (a.push i, mixTrace t t')
|
||||
liftM <| foldRightArrayAsync f (#[], nilTrace) tasks
|
||||
|
||||
def collectOpaqueList (targets : List (Target ι n k τ)) : Target PUnit n k τ :=
|
||||
def collectOpaqueList (targets : List (Target α n k τ)) : Target PUnit n k τ :=
|
||||
mk <| ((fun t => ((), t)) <$> ·) <$> materializeListAsync targets
|
||||
|
||||
def collectOpaqueArray (targets : Array (Target ι n k τ)) : Target PUnit n k τ :=
|
||||
def collectOpaqueArray (targets : Array (Target α n k τ)) : Target PUnit n k τ :=
|
||||
mk <| ((fun t => ((), t)) <$> ·) <$> materializeArrayAsync targets
|
||||
|
||||
end
|
||||
end Target
|
||||
|
|
|
|||
|
|
@ -3,10 +3,9 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
|
|||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lake.Build.Job
|
||||
import Lake.Build.Target
|
||||
import Lake.Build.Context
|
||||
|
||||
open System
|
||||
namespace Lake
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
|
@ -14,14 +13,11 @@ namespace Lake
|
|||
--------------------------------------------------------------------------------
|
||||
|
||||
/-- A Lake build target. -/
|
||||
abbrev BuildTarget i := Target i SchedulerM BuildTask BuildTrace
|
||||
|
||||
/-- An active Lake build target. -/
|
||||
abbrev ActiveBuildTarget i := ActiveTarget i BuildTask BuildTrace
|
||||
abbrev BuildTarget i := Target i SchedulerM Job BuildTrace
|
||||
|
||||
namespace BuildTarget
|
||||
|
||||
abbrev activate (self : BuildTarget i) : SchedulerM (ActiveBuildTarget i) :=
|
||||
abbrev activate (self : BuildTarget i) : SchedulerM (BuildJob i) :=
|
||||
Target.activate self
|
||||
|
||||
abbrev bindSync (self : BuildTarget i) (f : i → BuildTrace → BuildM β) :=
|
||||
|
|
@ -32,44 +28,23 @@ abbrev bindOpaqueSync (self : BuildTarget i) (f : BuildTrace → BuildM β) :=
|
|||
|
||||
end BuildTarget
|
||||
|
||||
namespace ActiveBuildTarget
|
||||
|
||||
abbrev bindSync (self : ActiveBuildTarget i) (f : i → BuildTrace → BuildM β) :=
|
||||
ActiveTarget.bindSync self f
|
||||
|
||||
abbrev bindOpaqueSync (self : ActiveBuildTarget i) (f : BuildTrace → BuildM β) :=
|
||||
ActiveTarget.bindOpaqueSync self f
|
||||
|
||||
end ActiveBuildTarget
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
/-! # File Targets -/
|
||||
/-! # Common Targets -/
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
export System (FilePath)
|
||||
|
||||
/-- A `BuildTarget` that produces a file. -/
|
||||
abbrev FileTarget := BuildTarget FilePath
|
||||
|
||||
/--
|
||||
A `BuildTarget` that produces a dynamic/shared library for lining.
|
||||
A dynamic/shared library for linking.
|
||||
Represented by an optional `-L` library directory × a `-l` library name.
|
||||
-/
|
||||
abbrev DynlibTarget := BuildTarget (Option FilePath × String)
|
||||
abbrev Dynlib := Option FilePath × String
|
||||
|
||||
/-- An `ActiveBuildTarget` that produces a file. -/
|
||||
abbrev ActiveFileTarget := ActiveBuildTarget FilePath
|
||||
|
||||
/--
|
||||
A `ActiveBuildTarget` that produces a dynamic/shared library for lining.
|
||||
Represented by an optional `-L` library directory × a `-l` library name.
|
||||
-/
|
||||
abbrev ActiveDynlibTarget := ActiveBuildTarget (Option FilePath × String)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
/-! # Opaque Targets -/
|
||||
--------------------------------------------------------------------------------
|
||||
/-- A `BuildTarget` that produces a `Dynlib`. -/
|
||||
abbrev DynlibTarget := BuildTarget Dynlib
|
||||
|
||||
/-- A `BuildTarget` with no artifact information. -/
|
||||
abbrev OpaqueTarget := BuildTarget Unit
|
||||
|
||||
/-- An `ActiveBuildTarget` with no artifact information. -/
|
||||
abbrev ActiveOpaqueTarget := ActiveBuildTarget Unit
|
||||
|
|
|
|||
|
|
@ -5,6 +5,7 @@ Authors: Mac Malone
|
|||
-/
|
||||
import Lake.Build.Actions
|
||||
import Lake.Build.TargetTypes
|
||||
import Lake.Build.Monad
|
||||
|
||||
open System
|
||||
namespace Lake
|
||||
|
|
|
|||
|
|
@ -12,15 +12,15 @@ namespace Lake
|
|||
|
||||
structure BuildSpec where
|
||||
info : BuildInfo
|
||||
getJob : BuildData info.key → Job
|
||||
getJob : BuildData info.key → Job Unit
|
||||
|
||||
/-- Get the `Job` associated with some `ActiveBuildTarget` `BuildData`. -/
|
||||
/-- Get the `Job` associated with some `BuildJob` `BuildData`. -/
|
||||
@[inline] def BuildData.toJob
|
||||
[FamilyDef BuildData k (ActiveBuildTarget α)] (data : BuildData k) : Job :=
|
||||
[FamilyDef BuildData k (BuildJob α)] (data : BuildData k) : Job Unit :=
|
||||
discard <| ofFamily data
|
||||
|
||||
@[inline] def mkBuildSpec (info : BuildInfo)
|
||||
[FamilyDef BuildData info.key (ActiveBuildTarget α)] : BuildSpec :=
|
||||
[FamilyDef BuildData info.key (BuildJob α)] : BuildSpec :=
|
||||
{info, getJob := BuildData.toJob}
|
||||
|
||||
@[inline] def mkConfigBuildSpec (facetType : String)
|
||||
|
|
@ -30,7 +30,7 @@ structure BuildSpec where
|
|||
| throw <| CliError.nonTargetFacet facetType facet
|
||||
return {info, getJob := h ▸ getJob}
|
||||
|
||||
def BuildSpec.build (self : BuildSpec) : RecBuildM Job := do
|
||||
def BuildSpec.build (self : BuildSpec) : RecBuildM (Job Unit) := do
|
||||
return self.getJob <| ← buildIndexTop' self.info
|
||||
|
||||
def buildSpecs (specs : Array BuildSpec) : BuildM PUnit := do
|
||||
|
|
@ -83,7 +83,7 @@ def resolveCustomTarget (pkg : Package)
|
|||
if !facet.isAnonymous then
|
||||
throw <| CliError.invalidFacet target facet
|
||||
else if h : pkg.name = config.package then
|
||||
have : FamilyDef CustomData (pkg.name, config.name) (ActiveBuildTarget config.resultType) :=
|
||||
have : FamilyDef CustomData (pkg.name, config.name) (BuildJob config.resultType) :=
|
||||
⟨by simp [h]⟩
|
||||
return mkBuildSpec <| pkg.customTarget config.name
|
||||
else
|
||||
|
|
|
|||
|
|
@ -204,7 +204,7 @@ def exe (name : Name) (args : Array String := #[]) : LakeT IO UInt32 := do
|
|||
let ws ← getWorkspace
|
||||
if let some exe := ws.findLeanExe? name then
|
||||
let ctx ← mkBuildContext ws
|
||||
let exeFile ← (exe.build >>= (·.build)).run MonadLog.eio ctx
|
||||
let exeFile ← (exe.build >>= (·.await)).run MonadLog.eio ctx
|
||||
env exeFile.toString args
|
||||
else
|
||||
error s!"unknown executable `{name}`"
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ structure FacetConfig (DataFam : Name → Type) (ι : Type) (name : Name) : Type
|
|||
/-- The facet's build (function). -/
|
||||
build : ι → IndexBuildM (DataFam name)
|
||||
/-- Does this facet produce an associated asynchronous job? -/
|
||||
getJob? : Option (DataFam name → Job)
|
||||
getJob? : Option (DataFam name → Job Unit)
|
||||
deriving Inhabited
|
||||
|
||||
protected abbrev FacetConfig.name (_ : FacetConfig DataFam ι name) := name
|
||||
|
|
|
|||
|
|
@ -70,7 +70,7 @@ Is true if either the package or the library have `precompileModules` set.
|
|||
self.pkg.precompileModules || self.config.precompileModules
|
||||
|
||||
/-- The library's `nativeFacets` configuration. -/
|
||||
@[inline] def nativeFacets (self : LeanLib) : Array (ModuleFacet ActiveFileTarget) :=
|
||||
@[inline] def nativeFacets (self : LeanLib) : Array (ModuleFacet (BuildJob FilePath)) :=
|
||||
self.config.nativeFacets
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -66,7 +66,7 @@ structure LeanLibConfig extends LeanConfig where
|
|||
and shared libraries. Defaults to ``#[Module.oFacet]`` (i.e., the object file
|
||||
compiled from the Lean source).
|
||||
-/
|
||||
nativeFacets : Array (ModuleFacet ActiveFileTarget) := #[Module.oFacet]
|
||||
nativeFacets : Array (ModuleFacet (BuildJob FilePath)) := #[Module.oFacet]
|
||||
|
||||
deriving Inhabited
|
||||
|
||||
|
|
|
|||
|
|
@ -100,7 +100,7 @@ abbrev pkg (self : Module) : Package :=
|
|||
@[inline] def shouldPrecompile (self : Module) : Bool :=
|
||||
self.lib.precompileModules
|
||||
|
||||
@[inline] def nativeFacets (self : Module) : Array (ModuleFacet ActiveFileTarget) :=
|
||||
@[inline] def nativeFacets (self : Module) : Array (ModuleFacet (BuildJob FilePath)) :=
|
||||
self.lib.nativeFacets
|
||||
|
||||
@[inline] def isLeanOnly (self : Module) : Bool :=
|
||||
|
|
|
|||
|
|
@ -19,9 +19,9 @@ structure TargetConfig where
|
|||
/-- The target's build function. -/
|
||||
target : BuildTarget resultType
|
||||
/-- Proof that target's build result is the correctly typed target.-/
|
||||
data_eq_target : CustomData (package, name) = ActiveBuildTarget resultType
|
||||
data_eq_target : CustomData (package, name) = BuildJob resultType
|
||||
|
||||
family_def _nil_ : CustomData (.anonymous, .anonymous) := ActiveOpaqueTarget
|
||||
family_def _nil_ : CustomData (.anonymous, .anonymous) := BuildJob Unit
|
||||
|
||||
instance : Inhabited TargetConfig := ⟨{
|
||||
name := .anonymous
|
||||
|
|
@ -34,7 +34,7 @@ instance : Inhabited TargetConfig := ⟨{
|
|||
hydrate_opaque_type OpaqueTargetConfig TargetConfig
|
||||
|
||||
instance FamilyDefOfTargetConfig {cfg : TargetConfig}
|
||||
: FamilyDef CustomData (cfg.package, cfg.name) (ActiveBuildTarget cfg.resultType) :=
|
||||
: FamilyDef CustomData (cfg.package, cfg.name) (BuildJob cfg.resultType) :=
|
||||
⟨cfg.data_eq_target⟩
|
||||
|
||||
/-- Try to find a target configuration in the package with the given name . -/
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ kw:"module_facet " sig:simpleDeclSig : command => do
|
|||
let attr ← withRef kw `(Term.attrInstance| moduleFacet)
|
||||
let attrs := #[attr] ++ expandAttrs attrs?
|
||||
let name := Name.quoteFrom id id.getId
|
||||
`(module_data $id : ActiveBuildTarget $ty
|
||||
`(module_data $id : BuildJob $ty
|
||||
$[$doc?]? @[$attrs,*] def $id : ModuleFacetDecl := {
|
||||
name := $name
|
||||
config := Lake.mkFacetTargetConfig $defn
|
||||
|
|
@ -38,7 +38,7 @@ kw:"package_facet " sig:simpleDeclSig : command => do
|
|||
let attr ← withRef kw `(Term.attrInstance| packageFacet)
|
||||
let attrs := #[attr] ++ expandAttrs attrs?
|
||||
let name := Name.quoteFrom id id.getId
|
||||
`(package_data $id : ActiveBuildTarget $ty
|
||||
`(package_data $id : BuildJob $ty
|
||||
$[$doc?]? @[$attrs,*] def $id : PackageFacetDecl := {
|
||||
name := $name
|
||||
config := Lake.mkFacetTargetConfig $defn
|
||||
|
|
@ -53,7 +53,7 @@ kw:"library_facet " sig:simpleDeclSig : command => do
|
|||
let attr ← withRef kw `(Term.attrInstance| libraryFacet)
|
||||
let attrs := #[attr] ++ expandAttrs attrs?
|
||||
let name := Name.quoteFrom id id.getId
|
||||
`(library_data $id : ActiveBuildTarget $ty
|
||||
`(library_data $id : BuildJob $ty
|
||||
$[$doc?]? @[$attrs,*] def $id : LibraryFacetDecl := {
|
||||
name := $name
|
||||
config := Lake.mkFacetTargetConfig $defn
|
||||
|
|
@ -70,7 +70,7 @@ kw:"target " sig:simpleDeclSig : command => do
|
|||
let axm := mkIdentFrom id <| ``CustomData ++ id.getId
|
||||
let name := Name.quoteFrom id id.getId
|
||||
let pkgName := mkIdentFrom id `_package.name
|
||||
`(family_def $id : CustomData ($pkgName, $name) := ActiveBuildTarget $ty
|
||||
`(family_def $id : CustomData ($pkgName, $name) := BuildJob $ty
|
||||
$[$doc?]? @[$attrs,*] def $id : TargetConfig := {
|
||||
name := $name
|
||||
package := $pkgName
|
||||
|
|
|
|||
|
|
@ -27,4 +27,4 @@ target bark : PUnit := Target.mk <| sync (m := BuildM) do
|
|||
|
||||
package_facet print_name : PUnit := fun pkg => do
|
||||
IO.println pkg.name
|
||||
return ActiveTarget.nil
|
||||
return BuildJob.nil
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue