From 8b402c4ee08f9bed641353651d88ef2ad32d684b Mon Sep 17 00:00:00 2001 From: tydeu Date: Tue, 26 Jul 2022 21:13:43 -0400 Subject: [PATCH] refactor: move info into target task --- Lake/Build/Actions.lean | 2 +- Lake/Build/Facets.lean | 4 + Lake/Build/Index.lean | 12 +- Lake/Build/Info.lean | 13 ++ Lake/Build/Library.lean | 2 +- Lake/Build/Module.lean | 170 +++++++++++++------------- Lake/Build/Target.lean | 238 +++++++++++++++++------------------- Lake/Build/TargetTypes.lean | 18 ++- Lake/Build/Targets.lean | 52 +++++--- Lake/CLI/Build.lean | 2 +- 10 files changed, 273 insertions(+), 240 deletions(-) diff --git a/Lake/Build/Actions.lean b/Lake/Build/Actions.lean index b9f6833ed5..32b9967076 100644 --- a/Lake/Build/Actions.lean +++ b/Lake/Build/Actions.lean @@ -35,7 +35,7 @@ def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do def compileLeanModule (leanFile : FilePath) (oleanFile? ileanFile? cFile? : Option FilePath) (leanPath : SearchPath := []) (rootDir : FilePath := ".") -(dynlibs : Array String := #[]) (dynlibPath : SearchPath := {}) +(dynlibs : Array FilePath := #[]) (dynlibPath : SearchPath := {}) (leanArgs : Array String := #[]) (lean : FilePath := "lean") : BuildM PUnit := do let mut args := leanArgs ++ diff --git a/Lake/Build/Facets.lean b/Lake/Build/Facets.lean index 8516d94351..574e25bac6 100644 --- a/Lake/Build/Facets.lean +++ b/Lake/Build/Facets.lean @@ -93,3 +93,7 @@ target_data externLib.static : ActiveFileTarget /-- A external library's shared binary. -/ abbrev ExternLib.sharedFacet := `externLib.shared target_data externLib.shared : ActiveFileTarget + +/-- A external library's dynlib. -/ +abbrev ExternLib.dynlibFacet := `externLib.dynlib +target_data externLib.dynlib : ActiveDynlibTarget diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean index ab11b3feb1..4058b80022 100644 --- a/Lake/Build/Index.lean +++ b/Lake/Build/Index.lean @@ -63,7 +63,11 @@ def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key) | .sharedExternLib lib => mkTargetFacetBuild ExternLib.sharedFacet do let staticTarget := Target.active <| ← lib.static.recBuild - staticToLeanDynlibTarget staticTarget |>.activate + staticToLeanSharedLibTarget staticTarget |>.activate +| .dynlibExternLib lib => + mkTargetFacetBuild ExternLib.dynlibFacet do + let sharedTarget := Target.active <| ← lib.shared.recBuild + sharedToLeanDynlibTarget sharedTarget |>.activate /-- Recursively build the given info using the Lake build index @@ -91,14 +95,14 @@ 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 α)] : OpaqueTarget := - BuildTarget.mk' () <| self.build <&> (·.task) +[FamilyDef BuildData self.key (ActiveBuildTarget α)] : BuildTarget α := + Target.mk <| (self.build <&> (·.task)) |>.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 build := cast (by rw [← h.family_key_eq_type]) build - getJob? := some (fun data => let_fun target := ofFamily data; target.task) + getJob? := some (fun data => let_fun target := ofFamily data; (·.2) <$> target.task) /-! ### Lean Executable Builds -/ diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean index f9e649472c..588bee11f5 100644 --- a/Lake/Build/Info.lean +++ b/Lake/Build/Info.lean @@ -26,6 +26,7 @@ inductive BuildInfo | leanExe (exe : LeanExe) | staticExternLib (lib : ExternLib) | sharedExternLib (lib : ExternLib) +| dynlibExternLib (lib : ExternLib) | customTarget (package : Package) (target : Name) -------------------------------------------------------------------------------- @@ -55,6 +56,9 @@ abbrev ExternLib.staticBuildKey (self : ExternLib) : BuildKey := abbrev ExternLib.sharedBuildKey (self : ExternLib) : BuildKey := .targetFacet self.pkg.name self.name sharedFacet +abbrev ExternLib.dynlibBuildKey (self : ExternLib) : BuildKey := + .targetFacet self.pkg.name self.name dynlibFacet + /-! ### Build Info to Key -/ /-- The key that identifies the build in the Lake build store. -/ @@ -65,6 +69,7 @@ abbrev BuildInfo.key : (self : BuildInfo) → BuildKey | leanExe x => x.buildKey | staticExternLib l => l.staticBuildKey | sharedExternLib l => l.sharedBuildKey +| dynlibExternLib l => l.dynlibBuildKey | customTarget p t => p.targetBuildKey t /-! ### Instances for deducing data types of `BuildInfo` keys -/ @@ -97,6 +102,10 @@ instance [FamilyDef TargetData ExternLib.sharedFacet α] : FamilyDef BuildData (BuildInfo.key (.sharedExternLib l)) α where family_key_eq_type := by unfold BuildData; simp +instance [FamilyDef TargetData ExternLib.dynlibFacet α] +: FamilyDef BuildData (BuildInfo.key (.dynlibExternLib l)) α where + family_key_eq_type := by unfold BuildData; simp + -------------------------------------------------------------------------------- /-! ## Recursive Building -/ -------------------------------------------------------------------------------- @@ -203,3 +212,7 @@ abbrev ExternLib.static (self : ExternLib) : BuildInfo := /-- Build info of the external library's shared binary. -/ abbrev ExternLib.shared (self : ExternLib) : BuildInfo := .sharedExternLib self + +/-- Build info of the external library's dynlib. -/ +abbrev ExternLib.dynlib (self : ExternLib) : BuildInfo := + .dynlibExternLib self diff --git a/Lake/Build/Library.lean b/Lake/Build/Library.lean index 0758a63990..646dd2edff 100644 --- a/Lake/Build/Library.lean +++ b/Lake/Build/Library.lean @@ -28,7 +28,7 @@ def LeanLib.recBuildLocalModules protected def LeanLib.recBuildLean (self : LeanLib) : IndexT RecBuildM ActiveOpaqueTarget := do - ActiveTarget.collectOpaqueArray (i := PUnit) <| + ActiveTarget.collectOpaqueArray (ι := PUnit) <| ← self.recBuildLocalModules #[Module.leanBinFacet] /-- The `LibraryFacetConfig` for the builtin `leanFacet`. -/ diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean index 344850f2d3..56b4784a4e 100644 --- a/Lake/Build/Module.lean +++ b/Lake/Build/Module.lean @@ -12,94 +12,56 @@ namespace Lake /-! # Solo Module Targets -/ -def Module.soloTarget (mod : Module) (dynlibs : Array String) -(dynlibPath : SearchPath) (depTarget : BuildTarget x) (leanOnly : Bool) : OpaqueTarget := - Target.opaque <| depTarget.bindOpaqueSync fun depTrace => do - let argTrace : BuildTrace := pureHash mod.leanArgs - let srcTrace : BuildTrace ← computeTrace mod.leanFile - let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace - let modUpToDate ← modTrace.checkAgainstFile mod mod.traceFile - if leanOnly then - unless modUpToDate do - compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile none - (← getLeanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean) - else - let cUpToDate ← modTrace.checkAgainstFile mod.cFile mod.cTraceFile - unless modUpToDate && cUpToDate do - compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile mod.cFile - (← getLeanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean) - modTrace.writeToFile mod.cTraceFile - modTrace.writeToFile mod.traceFile - return mixTrace (← computeTrace mod) depTrace +def buildModuleUnlessUpToDate (mod : Module) +(dynlibPath : SearchPath) (dynlibs : Array FilePath) +(depTrace : BuildTrace) (leanOnly : Bool) : BuildM BuildTrace := do + let argTrace : BuildTrace := pureHash mod.leanArgs + let srcTrace : BuildTrace ← computeTrace mod.leanFile + let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace + let modUpToDate ← modTrace.checkAgainstFile mod mod.traceFile + if leanOnly then + unless modUpToDate do + compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile none + (← getLeanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean) + else + let cUpToDate ← modTrace.checkAgainstFile mod.cFile mod.cTraceFile + unless modUpToDate && cUpToDate do + compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile mod.cFile + (← getLeanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean) + modTrace.writeToFile mod.cTraceFile + modTrace.writeToFile mod.traceFile + return mixTrace (← computeTrace mod) depTrace def Module.mkOleanTarget (modTarget : BuildTarget x) (self : Module) : FileTarget := - Target.mk self.oleanFile <| modTarget.bindOpaqueSync fun depTrace => - return mixTrace (← computeTrace self.oleanFile) depTrace + Target.mk <| modTarget.bindOpaqueSync fun depTrace => + return (self.oleanFile, mixTrace (← computeTrace self.oleanFile) depTrace) def Module.mkIleanTarget (modTarget : BuildTarget x) (self : Module) : FileTarget := - Target.mk self.ileanFile <| modTarget.bindOpaqueSync fun depTrace => - return mixTrace (← computeTrace self.ileanFile) depTrace + Target.mk <| modTarget.bindOpaqueSync fun depTrace => + return (self.ileanFile, mixTrace (← computeTrace self.ileanFile) depTrace) def Module.mkCTarget (modTarget : BuildTarget x) (self : Module) : FileTarget := - Target.mk self.cFile <| modTarget.bindOpaqueSync fun _ => - return mixTrace (← computeTrace self.cFile) (← getLeanTrace) + Target.mk <| modTarget.bindOpaqueSync fun _ => + return (self.cFile, mixTrace (← computeTrace self.cFile) (← getLeanTrace)) -@[inline] -def Module.mkOTarget (cTarget : FileTarget) (self : Module) : FileTarget := +@[inline] def Module.mkOTarget (cTarget : FileTarget) (self : Module) : FileTarget := leanOFileTarget self.oFile cTarget self.leancArgs -@[inline] -def Module.mkDynlibTarget (self : Module) (linkTargets : Array FileTarget) -(libDirs : Array FilePath) (libTargets : Array FileTarget) : FileTarget := - let linksTarget : BuildTarget _ := Target.collectArray linkTargets - let libsTarget : BuildTarget _ := Target.collectArray libTargets - Target.mk self.dynlibName do - linksTarget.bindAsync fun links oTrace => do - libsTarget.bindSync fun libFiles libTrace => do - buildFileUnlessUpToDate self.dynlibFile (oTrace.mix libTrace) do - let args := links.map toString ++ libDirs.map (s!"-L{·}") ++ libFiles.map (s!"-l{·}") - compileSharedLib self.dynlibFile args (← getLeanc) - /-! # Recursive Building -/ /-- Compute library directories and build external library targets of the given packages. -/ def recBuildExternalDynlibs (pkgs : Array Package) -: IndexBuildM (Array ActiveFileTarget × Array FilePath) := do +: IndexBuildM (Array ActiveDynlibTarget × Array FilePath) := do let mut libDirs := #[] - let mut targets : Array ActiveFileTarget := #[] + let mut targets : Array ActiveDynlibTarget := #[] for pkg in pkgs do libDirs := libDirs.push pkg.libDir - for lib in pkg.externLibs do - let target ← lib.shared.recBuild - if let some parent := target.info.parent then - libDirs := libDirs.push parent - if let some stem := target.info.fileStem then - if Platform.isWindows then - targets := targets.push <| target.withInfo stem - else if stem.startsWith "lib" then - targets := targets.push <| target.withInfo <| stem.drop 3 - else - logWarning s!"external library `{target.info}` was skipped because it does not start with `lib`" - else - logWarning s!"external library `{target.info}` was skipped because it has no file name" + targets := targets.append <| ← pkg.externLibs.mapM (·.dynlib.recBuild) return (targets, libDirs) -/-- Build the dynlibs of all imports. -/ -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 := #[] - 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) - /-- Build the dynlibs of the imports that want precompilation (and *their* imports). -/ def recBuildPrecompileDynlibs (pkg : Package) (imports : Array Module) -: IndexBuildM (Array ActiveFileTarget × Array ActiveFileTarget × Array FilePath) := do +: IndexBuildM (Array ActiveFileTarget × Array ActiveDynlibTarget × Array FilePath) := do let mut pkgs := #[] let mut pkgSet := PackageSet.empty.insert pkg let mut modSet := ModuleSet.empty @@ -136,18 +98,25 @@ def Module.recBuildLean (mod : Module) (art : LeanArtifact) -- Compute and build dependencies let extraDepTarget ← mod.pkg.extraDep.recBuild let (imports, _) ← mod.imports.recBuild - let (modTargets, pkgTargets, libDirs) ← recBuildPrecompileDynlibs mod.pkg imports - -- NOTE: Lean wants the external library symbols before module symbols - let dynlibsTarget ← ActiveTarget.collectArray <| pkgTargets ++ modTargets - let importTarget ← ActiveTarget.collectOpaqueArray - <| ← imports.mapM (·.leanBin.recBuild) - let depTarget := Target.active <| ← extraDepTarget.mixOpaqueAsync - <| ← dynlibsTarget.mixOpaqueAsync importTarget - -- NOTE: Unix requires the full file name of the dynlib (Windows doesn't care) - let dynlibs := dynlibsTarget.info.map (nameToSharedLib ·.toString) + 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 -- Build Module - let modTarget ← mod.soloTarget dynlibs libDirs.toList depTarget leanOnly |>.activate + let modTarget : OpaqueTarget := Target.mk do + importTarget.bindOpaqueAsync fun importTrace => do + modDynlibsTarget.bindAsync fun modDynlibs modTrace => do + externDynlibsTarget.bindAsync fun externDynlibs externTrace => do + extraDepTarget.bindOpaqueSync 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 + let trace ← buildModuleUnlessUpToDate mod dynlibPath.toList dynlibs depTrace leanOnly + return ((), trace) + let modTarget ← modTarget.activate -- Save All Resulting Targets & Return Requested One store mod.leanBin.key modTarget @@ -224,16 +193,45 @@ def Module.recParseImports (mod : Module) def Module.importFacetConfig : ModuleFacetConfig importFacet := mkFacetConfig (·.recParseImports) -/-- -Recursively build the shared library of a module (e.g., for `--load-dynlib`). --/ + +/-- Build the dynlibs of all imports. -/ +def recBuildDynlibs (pkg : Package) (imports : Array Module) +: IndexBuildM (Array ActiveFileTarget × Array ActiveDynlibTarget × Array FilePath) := do + let mut pkgs := #[] + let mut pkgSet := PackageSet.empty.insert pkg + let mut targets := #[] + 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) + +/-- Recursively build the shared library of a module (e.g., for `--load-dynlib`). -/ def Module.recBuildDynlib (mod : Module) : IndexBuildM ActiveFileTarget := do + + -- Compute dependencies 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 + let linkTargets ← mod.nativeFacets.mapM (recBuild <| mod.facet ·.name) + let (modTargets, externTargets, pkgLibDirs) ← recBuildDynlibs mod.pkg transImports + + -- Build dynlib + let linksTarget ← ActiveTarget.collectArray linkTargets + let modDynlibsTarget ← ActiveTarget.collectArray modTargets + let externDynlibsTarget : ActiveBuildTarget _ ← ActiveTarget.collectArray externTargets + let target : BuildTarget _ := Target.mk 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) + 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) + target.activate /-- The `ModuleFacetConfig` for the builtin `dynlibFacet`. -/ def Module.dynlibFacetConfig : ModuleFacetConfig dynlibFacet := diff --git a/Lake/Build/Target.lean b/Lake/Build/Target.lean index 4af72fa741..485db2c2ec 100644 --- a/Lake/Build/Target.lean +++ b/Lake/Build/Target.lean @@ -13,81 +13,79 @@ namespace Lake /-! # Active Targets -/ -------------------------------------------------------------------------------- -structure ActiveTarget.{u,v,w} (i : Type u) (k : Type v → Type w) (t : Type v) where - info : i - task : k t +structure ActiveTarget.{u,v} (ι : Type u) (k : Type u → Type v) (τ : Type u) where + task : k (ι × τ) -instance [Inhabited i] [Inhabited t] [Pure k] : Inhabited (ActiveTarget i k t) := - ⟨Inhabited.default, pure Inhabited.default⟩ +instance [Inhabited ι] [Inhabited τ] [Pure k] : Inhabited (ActiveTarget ι k τ) := + ⟨⟨pure default⟩⟩ namespace ActiveTarget -def withInfo (info : i') (self : ActiveTarget i k t) : ActiveTarget i' k t := - {self with info} +def withoutInfo [Functor k] (target : ActiveTarget ι k t) : ActiveTarget PUnit k t := + mk <| (fun (_,t) => ((),t)) <$> target.task -def withoutInfo (self : ActiveTarget i k t) : ActiveTarget PUnit k t := - self.withInfo () +def «opaque» [Functor k] (task : k t) : ActiveTarget PUnit k t := + mk <| ((), ·) <$> task -def withTask (task : k' t') (self : ActiveTarget i k t) : ActiveTarget i k' t' := - {self with task} +protected def pure [Pure k] (info : ι) (trace : τ) : ActiveTarget ι k τ := + mk <| pure (info, trace) -def «opaque» (task : k t) : ActiveTarget PUnit k t := - ⟨(), task⟩ +def nil [NilTrace τ] [Pure k] : ActiveTarget PUnit k τ := + mk <| pure ((), nilTrace) -protected def pure [Pure k] (info : i) (trace : t) : ActiveTarget i k t := - ⟨info, pure trace⟩ +protected def bindSync [BindSync m n k] (self : ActiveTarget ι k α) (f : ι → α → m β) : n (k β) := + bindSync self.task fun (i, a) => f i a -def nil [NilTrace t] [Pure k] : ActiveTarget PUnit k t := - mk () <| pure nilTrace +protected def bindOpaqueSync [BindSync m n k] (self : ActiveTarget ι k α) (f : α → m β) : n (k β) := + bindSync self.task fun (_, a) => f a -protected def bindSync [BindSync m n k] (self : ActiveTarget i k α) (f : i → α → m β) : n (k β) := - bindSync self.task (f self.info) +protected def bindAsync [BindAsync n k] (self : ActiveTarget ι k α) (f : ι → α → n (k β)) : n (k β) := + bindAsync self.task fun (i, a) => f i a -protected def bindOpaqueSync [BindSync m n k] (self : ActiveTarget i k α) (f : α → m β) : n (k β) := - bindSync self.task f +protected def bindOpaqueAsync [BindAsync n k] (self : ActiveTarget ι k α) (f : α → n (k β)) : n (k β) := + bindAsync self.task fun (_, a) => f a -protected def bindAsync [BindAsync n k] (self : ActiveTarget i k α) (f : i → α → n (k β)) : n (k β) := - bindAsync self.task (f self.info) +def materialize [Await k n] [MonadLiftT n m] [Functor m] (self : ActiveTarget ι k τ) : m τ := + (·.2) <$> liftM (await self.task) -protected def bindOpaqueAsync [BindAsync n k] (self : ActiveTarget i k α) (f : α → n (k β)) : n (k β) := - bindAsync self.task f +def materializeAsync [Functor k] (self : ActiveTarget ι k τ) : k τ := + (·.2) <$> self.task -def materialize [Await k m'] [MonadLiftT m' m] (self : ActiveTarget i k t) : m t := - liftM <| await self.task +def build [Await k n] [MonadLiftT n m] [Functor m] (self : ActiveTarget ι k τ) : m ι := + (·.1) <$> liftM (await self.task) -def build [Await k m'] [MonadLiftT m' m] [Functor m] (self : ActiveTarget i k t) : m i := - Functor.mapConst self.info self.materialize - -def buildOpaque [Await k m'] [MonadLiftT m' m] [Functor m] (self : ActiveTarget i k t) : m PUnit := +def buildOpaque [Await k n] [MonadLiftT n m] [Functor m] (self : ActiveTarget ι k τ) : m PUnit := discard <| self.materialize def mixOpaqueAsync -[MixTrace t] [SeqWithAsync n k] [MonadLiftT n m] [Monad m] -(t1 : ActiveTarget α k t) (t2 : ActiveTarget β k t) : m (ActiveTarget PUnit k t) := do - pure <| ActiveTarget.opaque <| ← liftM <| seqWithAsync mixTrace t1.task t2.task +[MixTrace τ] [SeqWithAsync n k] [MonadLiftT n m] [Monad m] +(t1 : ActiveTarget α k τ) (t2 : ActiveTarget β k τ) : m (ActiveTarget PUnit k τ) := do + pure <| mk <| ← liftM <| seqWithAsync (fun (_,t) (_,t') => ((), mixTrace t t')) t1.task t2.task section -variable [NilTrace t] [MixTrace t] +variable [NilTrace τ] [MixTrace τ] -def materializeList [Await k n] [MonadLiftT n m] [Monad m] (targets : List (ActiveTarget i k t)) : m t := do - targets.foldlM (fun tr t => return mixTrace tr <| ← liftM <| await t.task) nilTrace +def materializeList [Await k n] [MonadLiftT n m] [Monad m] (targets : List (ActiveTarget ι k τ)) : m τ := do + targets.foldlM (fun tr t => return mixTrace tr <| ← t.materialize) nilTrace -def materializeArray [Await k n] [MonadLiftT n m] [Monad m] (targets : Array (ActiveTarget i k t)) : m t := do - targets.foldlM (fun tr t => return mixTrace tr <| ← liftM <| await t.task) nilTrace +def materializeArray [Await k n] [MonadLiftT n m] [Monad m] (targets : Array (ActiveTarget ι k τ)) : m τ := do + targets.foldlM (fun tr t => return mixTrace tr <| ← t.materialize) nilTrace variable [SeqWithAsync n k] [Monad n] [MonadLiftT n m] [Monad m] [Pure k] -def collectList (targets : List (ActiveTarget i k t)) : m (ActiveTarget (List i) k t) := do - pure <| mk (targets.map (·.info)) <| ← liftM <| foldRightListAsync mixTrace nilTrace <| targets.map (·.task) +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.map (·.task) -def collectArray (targets : Array (ActiveTarget i k t)) : m (ActiveTarget (Array i) k t) := do - pure <| mk (targets.map (·.info)) <| ← liftM <| foldRightArrayAsync mixTrace nilTrace <| targets.map (·.task) +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.map (·.task) -def collectOpaqueList (targets : List (ActiveTarget i k t)) : m (ActiveTarget PUnit k t) := do - pure <| «opaque» <| ← liftM <| foldRightListAsync mixTrace nilTrace <| targets.map (·.task) +variable [Functor k] -def collectOpaqueArray (targets : Array (ActiveTarget i k t)) : m (ActiveTarget PUnit k t) := do - pure <| «opaque» <| ← liftM <| foldRightArrayAsync mixTrace nilTrace <| targets.map (·.task) +def collectOpaqueList (targets : List (ActiveTarget ι k τ)) : m (ActiveTarget PUnit k τ) := «opaque» <$> do + liftM <| foldLeftListAsync (fun (_,t') t => mixTrace t t') nilTrace <| targets.map (·.task) + +def collectOpaqueArray (targets : Array (ActiveTarget ι k τ)) : m (ActiveTarget PUnit k τ) := «opaque» <$> do + liftM <| foldRightArrayAsync (fun t (_,t') => mixTrace t t') nilTrace <| targets.map (·.task) end end ActiveTarget @@ -96,125 +94,119 @@ end ActiveTarget /-! # Inactive Target -/ -------------------------------------------------------------------------------- -structure Target.{u,v,v',w} (i : Type u) (n : Type v → Type w) (k : Type v' → Type v) (t : Type v') where - info : i - task : n (k t) +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 i] [Inhabited t] [Pure n] [Pure k] : Inhabited (Target i n k t) := - ⟨Inhabited.default, pure <| pure Inhabited.default⟩ +instance [Inhabited ι] [Inhabited τ] [Pure n] [Pure k] : Inhabited (Target ι n k τ) := + ⟨⟨pure (pure default)⟩⟩ namespace Target -def withInfo (info : i') (self : Target i n k t) : Target i' n k t := - {self with info} +def «opaque» [Functor n] [Functor k] (task : n (k τ)) : Target PUnit n k τ := + mk <| ((fun t => ((), t)) <$> ·) <$> task -def withoutInfo (self : Target i n k t) : Target PUnit n k t := - self.withInfo () +def opaqueSync [Sync m n k] [Functor m] (act : m τ) : Target PUnit n k τ := + mk <| sync <| ((), ·) <$> act -def withTask (task : n' (k' t')) (self : Target i n k t) : Target i n' k' t' := - {self with task} +def opaqueAsync [Async m n k] [Functor m] (act : m τ) : Target PUnit n k τ := + mk <| async <| ((), ·) <$> act -def «opaque» (task : n (k t)) : Target PUnit n k t := - mk () task +protected def sync [Sync m n k] [Functor m] (info : ι) (act : m τ) : Target ι n k τ := + mk <| sync <| (info, ·) <$> act -def opaqueSync [Sync m n k] (act : m t) : Target PUnit n k t := - mk () <| sync act +protected def async [Async m n k] [Functor m] (info : ι) (act : m τ) : Target ι n k τ := + mk <| async <| (info, ·) <$> act -def opaqueAsync [Async m n k] (act : m t) : Target PUnit n k t := - mk () <| async act +def active [Pure n] (target : ActiveTarget ι k τ) : Target ι n k τ := + mk <| pure target.task -protected def sync [Sync m n k] (info : i) (act : m t) : Target i n k t := - mk info <| sync act +protected def pure [Pure n] [Pure k] (info : ι) (trace : τ) : Target ι n k τ := + mk <| pure <| pure (info, trace) -protected def async [Async m n k] (info : i) (act : m t) : Target i n k t := - mk info <| async act +def nil [NilTrace τ] [Pure n] [Pure k] : Target PUnit n k τ := + mk <| pure <| pure <| ((), nilTrace) -def active [Pure n] (target : ActiveTarget i k t) : Target i n k t := - mk target.info <| pure target.task +def computeSync [Functor m] [ComputeTrace ι m τ] [Sync m n k] (info : ι) : Target ι n k τ := + mk <| sync <| (info, ·) <$> ComputeTrace.computeTrace info -protected def pure [Pure n] [Pure k] (info : i) (trace : t) : Target i n k t := - mk info <| pure <| pure trace +def computeAsync [Functor m] [ComputeTrace ι m τ] [Async m n k] (info : ι) : Target ι n k τ := + mk <| async <| (info, ·) <$> ComputeTrace.computeTrace info -def nil [NilTrace t] [Pure n] [Pure k] : Target PUnit n k t := - mk () <| pure <| pure <| nilTrace +def activate [Functor n] (self : Target ι n k τ) : n (ActiveTarget ι k τ) := + (.mk ·) <$> self.task -def computeSync [ComputeTrace i m t] [Sync m n k] (info : i) : Target i n k t := - mk info <| sync <| ComputeTrace.computeTrace info +def materializeAsync [Functor n] [Functor k] (self : Target ι n k τ) : n (k τ) := + ((·.2) <$> ·) <$> self.task -def computeAsync [ComputeTrace i m t] [Async m n k] (info : i) : Target i n k t := - mk info <| async <| ComputeTrace.computeTrace info +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) -def activate [Functor n] (self : Target i n k t) : n (ActiveTarget i k t) := - Functor.map (fun t => ActiveTarget.mk self.info t) self.task +def build [Await k m'] [MonadLiftT m' m] [MonadLiftT n m] [Functor m] [Bind m] (self : Target ι n k τ) : m ι := + liftM self.task >>= fun t => (·.1) <$> liftM (await t) -def materializeAsync (self : Target i n k t) : n (k t) := - self.task - -def materialize [Await k m'] [MonadLiftT m' m] [MonadLiftT n m] [Bind m] (self : Target i n k t) : m t := - liftM self.task >>= (liftM ∘ await) - -def build [Await k m'] [MonadLiftT m' m] [MonadLiftT n m] [Functor m] [Bind m] (self : Target i n k t) : m i := - Functor.mapConst self.info self.materialize - -def buildOpaque [Await k m'] [MonadLiftT m' m] [MonadLiftT n m] [Functor m] [Bind m] (self : Target i n k t) : m PUnit := +def buildOpaque [Await k m'] [MonadLiftT m' m] [MonadLiftT n m] [Functor m] [Bind m] (self : Target ι n k τ) : m PUnit := discard self.materialize -def buildAsync [Functor n] [Functor k] (self : Target i n k t) : n (k i) := - Functor.mapConst self.info <$> self.task +def buildAsync [Functor n] [Functor k] (self : Target ι n k τ) : n (k ι) := + ((·.1) <$> ·) <$> self.task -def buildOpaqueAsync [Functor n] [Functor k] (self : Target i n k t) : n (k PUnit) := +def buildOpaqueAsync [Functor n] [Functor k] (self : Target ι n k τ) : n (k PUnit) := discard <$> self.task -protected def bindSync [BindSync m n k] [Bind n] (self : Target i n k t) (f : i → t → m β) : n (k β) := - self.task >>= fun tk => bindSync tk (f self.info) +protected def bindSync [BindSync m n k] [Bind n] (self : Target ι n k τ) (f : ι → τ → m β) : n (k β) := + self.task >>= fun tk => bindSync tk fun (i,t) => f i t -protected def bindOpaqueSync [BindSync m n k] [Bind n] (self : Target i n k t) (f : t → m β) : n (k β) := - self.task >>= fun tk => bindSync tk f +protected def bindOpaqueSync [BindSync m n k] [Bind n] (self : Target ι n k τ) (f : τ → m β) : n (k β) := + self.task >>= fun tk => bindSync tk fun (_,t) => f t -protected def bindAsync [BindAsync n k] [Bind n] (self : Target i n k t) (f : i → t → n (k β)) : n (k β) := - self.task >>= fun tk => bindAsync tk (f self.info) +protected def bindAsync [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 -protected def bindOpaqueAsync [BindAsync n k] [Bind n] (self : Target i n k t) (f : t → n (k β)) : n (k β) := - self.task >>= fun tk => bindAsync tk f +protected def bindOpaqueAsync [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 -[MixTrace t] [SeqWithAsync n k] [Monad n] -(t1 : Target α n k t) (t2 : Target β n k t) : Target PUnit n k t := - Target.opaque do +[MixTrace τ] [SeqWithAsync n k] [Functor k] [Monad n] +(t1 : Target α n k τ) (t2 : Target β n k τ) : Target PUnit n k τ := + mk do let tk1 ← t1.materializeAsync let tk2 ← t2.materializeAsync - seqWithAsync mixTrace tk1 tk2 + ((fun t => ((),t)) <$> ·) <$> seqWithAsync mixTrace tk1 tk2 section -variable [NilTrace t] [MixTrace t] +variable [NilTrace τ] [MixTrace τ] -def materializeList [Await k m] [MonadLiftT n m] [Monad m] (targets : List (Target i n k t)) : m t := do - let tasks ← targets.mapM (·.materializeAsync) - tasks.foldlM (fun tr t => return mixTrace tr <| ← liftM <| await t) nilTrace +def materializeList [Await k m] [MonadLiftT n m] [Monad m] (targets : List (Target ι n k τ)) : m τ := do + let tasks ← targets.mapM (·.task) + tasks.foldlM (fun tr τ => return mixTrace tr (← liftM <| await τ).2) nilTrace -def materializeArray [Await k m] [MonadLiftT n m] [Monad m] (targets : Array (Target i n k t)) : m t := do - let tasks ← targets.mapM (·.materializeAsync) - tasks.foldlM (fun tr t => return mixTrace tr <| ← liftM <| await t) nilTrace +def materializeArray [Await k m] [MonadLiftT n m] [Monad m] (targets : Array (Target ι n k τ)) : m τ := do + let tasks ← targets.mapM (·.task) + tasks.foldlM (fun tr τ => return mixTrace tr (← liftM <| await τ).2) nilTrace -variable [SeqWithAsync n' k] [Monad n'] [MonadLiftT n' n] [Monad n] [Pure k] +variable [SeqWithAsync n' k] [Monad n'] [MonadLiftT n' n] [Monad n] [Pure k] [Functor k] -def materializeListAsync (targets : List (Target i n k t)) : n (k t) := do +def materializeListAsync (targets : List (Target ι n k τ)) : n (k τ) := do liftM <| foldRightListAsync mixTrace nilTrace (← targets.mapM (·.materializeAsync)) -def materializeArrayAsync (targets : Array (Target i n k t)) : n (k t) := do +def materializeArrayAsync (targets : Array (Target ι n k τ)) : n (k τ) := do liftM <| foldRightArrayAsync mixTrace nilTrace (← targets.mapM (·.materializeAsync)) -def collectList (targets : List (Target i n k t)) : Target (List i) n k t := - mk (targets.map (·.info)) <| materializeListAsync targets +def collectList (targets : List (Target ι n k τ)) : Target (List ι) n k τ := + mk do + let tasks ← targets.mapM (·.task) + liftM <| foldLeftListAsync (fun (i,t') (a,t) => (i :: a, mixTrace t t')) ([], nilTrace) tasks -def collectArray (targets : Array (Target i n k t)) : Target (Array i) n k t := - mk (targets.map (·.info)) <| materializeArrayAsync targets +def collectArray (targets : Array (Target ι n k τ)) : Target (Array ι) n k τ := + mk do + let tasks ← targets.mapM (·.task) + liftM <| foldRightArrayAsync (fun (a,t) (i,t') => (a.push i, mixTrace t t')) (#[], nilTrace) tasks -def collectOpaqueList (targets : List (Target i n k t)) : Target PUnit n k t := - «opaque» <| materializeListAsync targets +def collectOpaqueList (targets : List (Target ι n k τ)) : Target PUnit n k τ := + mk <| ((fun t => ((), t)) <$> ·) <$> materializeListAsync targets -def collectOpaqueArray (targets : Array (Target i n k t)) : Target PUnit n k t := - «opaque» <| materializeArrayAsync targets +def collectOpaqueArray (targets : Array (Target ι n k τ)) : Target PUnit n k τ := + mk <| ((fun t => ((), t)) <$> ·) <$> materializeArrayAsync targets end end Target diff --git a/Lake/Build/TargetTypes.lean b/Lake/Build/TargetTypes.lean index 9116271205..a802a0fd29 100644 --- a/Lake/Build/TargetTypes.lean +++ b/Lake/Build/TargetTypes.lean @@ -21,12 +21,6 @@ abbrev ActiveBuildTarget i := ActiveTarget i BuildTask BuildTrace namespace BuildTarget -abbrev mk (info : i) (task : SchedulerM Job) : BuildTarget i := - Target.mk info task - -abbrev mk' (info : i) (task : BuildM Job) : BuildTarget i := - Target.mk info <| task.catchFailure fun _ => pure failure - abbrev activate (self : BuildTarget i) : SchedulerM (ActiveBuildTarget i) := Target.activate self @@ -55,9 +49,21 @@ end ActiveBuildTarget /-- A `BuildTarget` that produces a file. -/ abbrev FileTarget := BuildTarget FilePath +/-- +A `BuildTarget` that produces a dynamic/shared library for lining. +Represented by an optional `-L` library directory × a `-l` library name. +-/ +abbrev DynlibTarget := BuildTarget (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 -/ -------------------------------------------------------------------------------- diff --git a/Lake/Build/Targets.lean b/Lake/Build/Targets.lean index 1eb188ddbd..5701f5f2fd 100644 --- a/Lake/Build/Targets.lean +++ b/Lake/Build/Targets.lean @@ -12,11 +12,11 @@ namespace Lake /-! # General Utilities -/ def inputFileTarget (path : FilePath) : FileTarget := - Target.mk path <| async (m := BuildM) <| computeTrace path + Target.mk <| async (m := BuildM) <| (path, ·) <$> computeTrace path instance : Coe FilePath FileTarget := ⟨inputFileTarget⟩ -def buildUnlessUpToDate [CheckExists i] [GetMTime i] (info : i) +def buildUnlessUpToDate [CheckExists ι] [GetMTime ι] (info : ι) (depTrace : BuildTrace) (traceFile : FilePath) (build : BuildM PUnit) : BuildM PUnit := do let upToDate ← depTrace.checkAgainstFile info traceFile unless upToDate do @@ -29,17 +29,19 @@ def buildFileUnlessUpToDate (file : FilePath) buildUnlessUpToDate file depTrace traceFile build computeTrace file -def fileTargetWithDep (file : FilePath) (depTarget : BuildTarget i) -(build : i → BuildM PUnit) (extraDepTrace : BuildM _ := pure BuildTrace.nil) : FileTarget := - Target.mk file <| depTarget.bindSync fun depInfo depTrace => do - buildFileUnlessUpToDate file (depTrace.mix (← extraDepTrace)) <| build depInfo +def fileTargetWithDep (file : FilePath) (depTarget : BuildTarget ι) +(build : ι → BuildM PUnit) (extraDepTrace : BuildM _ := pure BuildTrace.nil) : FileTarget := + Target.mk <| depTarget.bindSync fun depInfo depTrace => do + let depTrace := depTrace.mix (← extraDepTrace) + let trace ← buildFileUnlessUpToDate file depTrace <| build depInfo + return (file, trace) -def fileTargetWithDepList (file : FilePath) (depTargets : List (BuildTarget i)) -(build : List i → BuildM PUnit) (extraDepTrace : BuildM _ := pure BuildTrace.nil) : FileTarget := +def fileTargetWithDepList (file : FilePath) (depTargets : List (BuildTarget ι)) +(build : List ι → BuildM PUnit) (extraDepTrace : BuildM _ := pure BuildTrace.nil) : FileTarget := fileTargetWithDep file (Target.collectList depTargets) build extraDepTrace -def fileTargetWithDepArray (file : FilePath) (depTargets : Array (BuildTarget i)) -(build : Array i → BuildM PUnit) (extraDepTrace : BuildM _ := pure BuildTrace.nil) : FileTarget := +def fileTargetWithDepArray (file : FilePath) (depTargets : Array (BuildTarget ι)) +(build : Array ι → BuildM PUnit) (extraDepTrace : BuildM _ := pure BuildTrace.nil) : FileTarget := fileTargetWithDep file (Target.collectArray depTargets) build extraDepTrace /-! # Specific Targets -/ @@ -81,12 +83,26 @@ def leanExeTarget (binFile : FilePath) (extraDepTrace := getLeanTrace <&> (·.mix <| pureHash linkArgs)) fun links => do compileExe binFile links linkArgs (← getLeanc) -def staticToLeanDynlibTarget (staticLibTarget : FileTarget) : FileTarget := - let dynlib := staticLibTarget.info.withExtension sharedLibExt - fileTargetWithDep dynlib staticLibTarget fun lib => do - let args := - if System.Platform.isOSX then - #[s!"-Wl,-force_load,{lib}"] +def staticToLeanSharedLibTarget (staticLibTarget : FileTarget) : FileTarget := + .mk <| staticLibTarget.bindSync fun staticLib staticTrace => do + let dynlib := staticLib.withExtension sharedLibExt + let trace ← buildFileUnlessUpToDate dynlib staticTrace do + let args := + if System.Platform.isOSX then + #[s!"-Wl,-force_load,{staticLib}"] + else + #["-Wl,--whole-archive", staticLib.toString, "-Wl,--no-whole-archive"] + compileSharedLib dynlib args (← getLeanc) + return (dynlib, trace) + +def sharedToLeanDynlibTarget (sharedLibTarget : FileTarget) : DynlibTarget := + .mk <| sharedLibTarget.bindSync fun sharedLib trace => do + if let some stem := sharedLib.fileStem then + if Platform.isWindows then + return ((sharedLib.parent, stem), trace) + else if stem.startsWith "lib" then + return ((sharedLib.parent, stem.drop 3), trace) else - #["-Wl,--whole-archive", lib.toString, "-Wl,--no-whole-archive"] - compileSharedLib dynlib args (← getLeanc) + error s!"shared library `{sharedLib}` does not start with `lib`; this is not supported on Unix" + else + error s!"shared library `{sharedLib}` has no file name" diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean index c6744689ad..89350a35a3 100644 --- a/Lake/CLI/Build.lean +++ b/Lake/CLI/Build.lean @@ -17,7 +17,7 @@ structure BuildSpec where /-- Get the `Job` associated with some `ActiveBuildTarget` `BuildData`. -/ @[inline] def BuildData.toJob [FamilyDef BuildData k (ActiveBuildTarget α)] (data : BuildData k) : Job := - ofFamily data |>.task + ofFamily data |>.materializeAsync @[inline] def mkBuildSpec (info : BuildInfo) [FamilyDef BuildData info.key (ActiveBuildTarget α)] : BuildSpec :=