diff --git a/Lake/Build/Actions.lean b/Lake/Build/Actions.lean index 32b9967076..b650517f82 100644 --- a/Lake/Build/Actions.lean +++ b/Lake/Build/Actions.lean @@ -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 diff --git a/Lake/Build/Context.lean b/Lake/Build/Context.lean index c6e6e424d0..80b6925ebc 100644 --- a/Lake/Build/Context.lean +++ b/Lake/Build/Context.lean @@ -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 diff --git a/Lake/Build/Executable.lean b/Lake/Build/Executable.lean index 28ce94af97..97d11cdd3a 100644 --- a/Lake/Build/Executable.lean +++ b/Lake/Build/Executable.lean @@ -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 diff --git a/Lake/Build/Facets.lean b/Lake/Build/Facets.lean index 574e25bac6..d39a009e61 100644 --- a/Lake/Build/Facets.lean +++ b/Lake/Build/Facets.lean @@ -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 diff --git a/Lake/Build/Imports.lean b/Lake/Build/Imports.lean index c8676a8c8b..686a107c6c 100644 --- a/Lake/Build/Imports.lean +++ b/Lake/Build/Imports.lean @@ -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 diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean index 975219e990..0dcc0e06ab 100644 --- a/Lake/Build/Index.lean +++ b/Lake/Build/Index.lean @@ -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 diff --git a/Lake/Build/Job.lean b/Lake/Build/Job.lean new file mode 100644 index 0000000000..c4bed59cbc --- /dev/null +++ b/Lake/Build/Job.lean @@ -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 #[]) diff --git a/Lake/Build/Library.lean b/Lake/Build/Library.lean index e097178c68..9f55a05b71 100644 --- a/Lake/Build/Library.lean +++ b/Lake/Build/Library.lean @@ -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 := diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean index cc6814e56b..abcb0141c9 100644 --- a/Lake/Build/Module.lean +++ b/Lake/Build/Module.lean @@ -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 := diff --git a/Lake/Build/Package.lean b/Lake/Build/Package.lean index 48ca4d51dd..2b5db86a94 100644 --- a/Lake/Build/Package.lean +++ b/Lake/Build/Package.lean @@ -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 := diff --git a/Lake/Build/Target.lean b/Lake/Build/Target.lean index 5fb0c26b34..42904a94f3 100644 --- a/Lake/Build/Target.lean +++ b/Lake/Build/Target.lean @@ -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 diff --git a/Lake/Build/TargetTypes.lean b/Lake/Build/TargetTypes.lean index 1731e1a275..2951ce8a0d 100644 --- a/Lake/Build/TargetTypes.lean +++ b/Lake/Build/TargetTypes.lean @@ -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 diff --git a/Lake/Build/Targets.lean b/Lake/Build/Targets.lean index 48d0deb480..948e6f2d26 100644 --- a/Lake/Build/Targets.lean +++ b/Lake/Build/Targets.lean @@ -5,6 +5,7 @@ Authors: Mac Malone -/ import Lake.Build.Actions import Lake.Build.TargetTypes +import Lake.Build.Monad open System namespace Lake diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean index 31ecf74c33..d3ffbefd8e 100644 --- a/Lake/CLI/Build.lean +++ b/Lake/CLI/Build.lean @@ -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 diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean index 4516b517ce..8b787337d3 100644 --- a/Lake/CLI/Main.lean +++ b/Lake/CLI/Main.lean @@ -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}`" diff --git a/Lake/Config/FacetConfig.lean b/Lake/Config/FacetConfig.lean index 60efcdd161..688024f170 100644 --- a/Lake/Config/FacetConfig.lean +++ b/Lake/Config/FacetConfig.lean @@ -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 diff --git a/Lake/Config/LeanLib.lean b/Lake/Config/LeanLib.lean index 903405588a..a318b79a84 100644 --- a/Lake/Config/LeanLib.lean +++ b/Lake/Config/LeanLib.lean @@ -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 /-- diff --git a/Lake/Config/LeanLibConfig.lean b/Lake/Config/LeanLibConfig.lean index c9ad055c3e..0288c0ff33 100644 --- a/Lake/Config/LeanLibConfig.lean +++ b/Lake/Config/LeanLibConfig.lean @@ -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 diff --git a/Lake/Config/Module.lean b/Lake/Config/Module.lean index 2e8325a9f6..45897f6a9e 100644 --- a/Lake/Config/Module.lean +++ b/Lake/Config/Module.lean @@ -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 := diff --git a/Lake/Config/TargetConfig.lean b/Lake/Config/TargetConfig.lean index 4fad3abafe..d97c2a6e37 100644 --- a/Lake/Config/TargetConfig.lean +++ b/Lake/Config/TargetConfig.lean @@ -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 . -/ diff --git a/Lake/DSL/Facets.lean b/Lake/DSL/Facets.lean index 71b9a9f099..e647148def 100644 --- a/Lake/DSL/Facets.lean +++ b/Lake/DSL/Facets.lean @@ -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 diff --git a/examples/targets/lakefile.lean b/examples/targets/lakefile.lean index 41ecdd0361..6aa718e227 100644 --- a/examples/targets/lakefile.lean +++ b/examples/targets/lakefile.lean @@ -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