diff --git a/Lake/Build/Imports.lean b/Lake/Build/Imports.lean index a7f0a2cf24..fcbeabf572 100644 --- a/Lake/Build/Imports.lean +++ b/Lake/Build/Imports.lean @@ -40,12 +40,11 @@ def Package.buildImportsAndDeps (imports : List String) (self : Package) : Build else -- build local imports from list let mods := (← getWorkspace).processImportList imports - let (res, bStore) ← EStateT.run BuildStore.empty <| mods.mapM fun mod => + let (importTargets, bStore) ← RecBuildM.runIn {} <| mods.mapM fun mod => if mod.shouldPrecompile then buildIndexTop mod.dynlib <&> (·.withoutInfo) else buildIndexTop mod.leanBin - let importTargets ← failOnBuildCycle res let dynlibTargets := bStore.collectModuleFacetArray Module.dynlibFacet let externLibTargets := bStore.collectSharedExternLibs importTargets.forM (·.buildOpaque) diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean index 623e456a4a..e397860bf2 100644 --- a/Lake/Build/Index.lean +++ b/Lake/Build/Index.lean @@ -5,7 +5,6 @@ Authors: Mac Malone -/ import Lake.Build.Roots import Lake.Build.Topological -import Lake.Util.EStateT /-! # The Lake Build Index @@ -82,17 +81,12 @@ and a topological / suspending scheduler and return the dynamic result. [FamilyDef BuildData info.key α] : RecBuildM α := do cast (by simp) <| buildIndexTop' info -/-- Build the given Lake target using the given Lake build store. -/ -@[inline] def BuildInfo.buildIn -(store : BuildStore) (self : BuildInfo) [FamilyDef BuildData self.key α] : BuildM α := do - failOnBuildCycle <| ← EStateT.run' store <| buildIndexTop self - /-- Build the given Lake target in a fresh build store. -/ -@[macroInline] def BuildInfo.build +@[inline] def BuildInfo.build (self : BuildInfo) [FamilyDef BuildData self.key α] : BuildM α := - buildIn BuildStore.empty self + buildIndexTop self |>.run -export BuildInfo (build buildIn) +export BuildInfo (build) /-! ## Targets Using the Build Index -/ @@ -105,10 +99,7 @@ export BuildInfo (build buildIn) @[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 - toTarget? := fun info key_eq_type => - have : FamilyDef BuildData info.key (ActiveBuildTarget α) := - ⟨h.family_key_eq_type ▸ key_eq_type⟩ - info.target + getJob? := some (fun data => let_fun target := ofFamily data; target.task) /-! ### Module Facet Targets -/ diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean index 40817e2e39..dcd9244757 100644 --- a/Lake/Build/Info.lean +++ b/Lake/Build/Info.lean @@ -131,7 +131,7 @@ abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m abbrev IndexBuildM := IndexT RecBuildM /-- Build the given info using the Lake build index. -/ -@[inline] def BuildInfo.recBuild (self : BuildInfo) [FamilyDef BuildData self.key α] : IndexT m α := +@[inline] def BuildInfo.recBuild (self : BuildInfo) [FamilyDef BuildData self.key α] : IndexBuildM α := fun build => cast (by simp) <| build self export BuildInfo (recBuild) diff --git a/Lake/Build/Monad.lean b/Lake/Build/Monad.lean index d31b119739..8545bdc0c3 100644 --- a/Lake/Build/Monad.lean +++ b/Lake/Build/Monad.lean @@ -5,6 +5,7 @@ Authors: Mac Malone -/ import Lake.Config.Monad import Lake.Build.Context +import Lake.Util.EStateT open System @@ -29,3 +30,18 @@ def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α | Except.error cycle => do let cycle := cycle.map (s!" {·}") error s!"build cycle detected:\n{"\n".intercalate cycle}" + +/-- +Run the recursive build in the given build store. +If a cycle is encountered, log it and then fail. +-/ +@[inline] def RecBuildM.runIn (store : BuildStore) (build : RecBuildM α) : BuildM (α × BuildStore) := do + let (res, store) ← EStateT.run store build + return (← failOnBuildCycle res, store) + +/-- +Run the recursive build in a fresh build store. +If a cycle is encountered, log it and then fail. +-/ +@[inline] def RecBuildM.run (build : RecBuildM α) : BuildM α := do + (·.1) <$> build.runIn {} diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean index 8563d7114b..00a10fb0ba 100644 --- a/Lake/CLI/Build.lean +++ b/Lake/CLI/Build.lean @@ -8,6 +8,37 @@ import Lake.CLI.Error namespace Lake +/-! ## Build Target Specifiers -/ + +structure BuildSpec where + info : BuildInfo + getJob : BuildData info.key → Job + +/-- Get the `Job` associated with some `ActiveBuildTarget` `BuildData`. -/ +@[inline] def BuildData.toJob +[FamilyDef BuildData k (ActiveBuildTarget α)] (data : BuildData k) : Job := + ofFamily data |>.task + +@[inline] def mkBuildSpec (info : BuildInfo) +[FamilyDef BuildData info.key (ActiveBuildTarget α)] : BuildSpec := + {info, getJob := BuildData.toJob} + +@[inline] def mkConfigBuildSpec (facetType : String) +(info : BuildInfo) (config : FacetConfig Fam ι facet) (h : BuildData info.key = Fam facet) +: Except CliError BuildSpec := do + let some getJob := config.getJob? + | throw <| CliError.nonTargetFacet facetType facet + return {info, getJob := h ▸ getJob} + +def BuildSpec.build (self : BuildSpec) : RecBuildM Job := do + return self.getJob <| ← buildIndexTop' self.info + +def buildSpecs (specs : Array BuildSpec) : BuildM PUnit := do + let jobs ← RecBuildM.run do specs.mapM (·.build) + jobs.forM (discard <| liftM <| await ·) + +/-! ## Parsing CLI Build Target Specifiers -/ + def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package := if spec.isEmpty then return ws.root @@ -17,49 +48,57 @@ def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package | none => throw <| CliError.unknownPackage spec open Module in -def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : Name) : Except CliError OpaqueTarget := +def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : Name) : Except CliError BuildSpec := if facet.isAnonymous then - return mod.facetTarget leanBinFacet + return mkBuildSpec <| mod.facet leanBinFacet else if let some config := ws.findModuleFacetConfig? facet then do - let some target := config.toTarget? (mod.facet facet) rfl - | throw <| CliError.nonTargetFacet "module" facet - return target + mkConfigBuildSpec "module" (mod.facet facet) config rfl else throw <| CliError.unknownFacet "module" facet -def resolveLibTarget (lib : LeanLib) (facet : Name) : Except CliError OpaqueTarget := - if facet.isAnonymous || facet == `lean then - return lib.leanTarget - else if facet == `static then - return lib.staticLibTarget |>.withoutInfo - else if facet == `shared then - return lib.sharedLibTarget |>.withoutInfo +def resolveLibTarget (lib : LeanLib) (facet : Name) : Except CliError BuildSpec := + if facet.isAnonymous || facet = `lean then + return mkBuildSpec lib.lean + else if facet = `static then + return mkBuildSpec lib.static + else if facet = `shared then + return mkBuildSpec lib.shared else throw <| CliError.unknownFacet "library" facet -def resolveExeTarget (exe : LeanExe) (facet : Name) : Except CliError OpaqueTarget := +def resolveExeTarget (exe : LeanExe) (facet : Name) : Except CliError BuildSpec := if facet.isAnonymous || facet == `exe then - return exe.target |>.withoutInfo + return mkBuildSpec exe.exe else throw <| CliError.unknownFacet "executable" facet -def resolveTargetInPackage (ws : Workspace) (pkg : Package) (target : Name) (facet : Name) : Except CliError OpaqueTarget := +def resolveExternLibTarget (lib : ExternLib) (facet : Name) : Except CliError BuildSpec := + if facet.isAnonymous || facet = `static then + return mkBuildSpec lib.static + else if facet = `shared then + return mkBuildSpec lib.shared + else + throw <| CliError.unknownFacet "external library" facet + +def resolveCustomTarget (pkg : Package) +(target facet : Name) (config : TargetConfig) : Except CliError BuildSpec := + 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) := + ⟨by simp [h]⟩ + return mkBuildSpec <| pkg.customTarget config.name + else + throw <| CliError.badTarget pkg.name target config.package config.name + +def resolveTargetInPackage (ws : Workspace) +(pkg : Package) (target facet : Name) : Except CliError BuildSpec := if let some config := pkg.findTargetConfig? target then - 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) := - ⟨by simp [h]⟩ - return pkg.customTarget config.name |>.target - else - throw <| CliError.badTarget pkg.name target config.package config.name + resolveCustomTarget pkg target facet config else if let some exe := pkg.findLeanExe? target then resolveExeTarget exe facet else if let some lib := pkg.findExternLib? target then - if facet.isAnonymous then - return lib.target.withoutInfo - else - throw <| CliError.invalidFacet target facet + resolveExternLibTarget lib facet else if let some lib := pkg.findLeanLib? target then resolveLibTarget lib facet else if let some mod := pkg.findModule? target then @@ -67,47 +106,36 @@ def resolveTargetInPackage (ws : Workspace) (pkg : Package) (target : Name) (fac else throw <| CliError.missingTarget pkg.name (target.toString false) -def resolveDefaultPackageTarget (ws : Workspace) (pkg : Package) : Except CliError OpaqueTarget := - return Target.collectOpaqueArray <| ← - pkg.defaultTargets.mapM (resolveTargetInPackage ws pkg · .anonymous) +def resolveDefaultPackageTarget (ws : Workspace) (pkg : Package) : Except CliError (Array BuildSpec) := + pkg.defaultTargets.mapM (resolveTargetInPackage ws pkg · .anonymous) -def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : Name) : Except CliError OpaqueTarget := +def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : Name) : Except CliError (Array BuildSpec) := if facet.isAnonymous then resolveDefaultPackageTarget ws pkg else if let some config := ws.findPackageFacetConfig? facet then do - let some target := config.toTarget? (pkg.facet facet) rfl - | throw <| CliError.nonTargetFacet "package" facet - return target + Array.singleton <$> mkConfigBuildSpec "package" (pkg.facet facet) config rfl else throw <| CliError.unknownFacet "package" facet -def resolveTargetInWorkspace (ws : Workspace) (target : Name) (facet : Name) : Except CliError OpaqueTarget := +def resolveTargetInWorkspace (ws : Workspace) +(target : Name) (facet : Name) : Except CliError (Array BuildSpec) := if let some (pkg, config) := ws.findTargetConfig? target then - if !facet.isAnonymous then - throw <| CliError.invalidFacet config.name facet - else if h : pkg.name = config.package then - have : FamilyDef CustomData (pkg.name, config.name) (ActiveBuildTarget config.resultType) := - ⟨by simp [h]⟩ - return pkg.customTarget config.name |>.target - else - throw <| CliError.badTarget pkg.name target config.package config.name + Array.singleton <$> resolveCustomTarget pkg target facet config else if let some exe := ws.findLeanExe? target then - resolveExeTarget exe facet + Array.singleton <$> resolveExeTarget exe facet else if let some lib := ws.findExternLib? target then - if facet.isAnonymous then - return lib.target.withoutInfo - else - throw <| CliError.invalidFacet target facet + Array.singleton <$> resolveExternLibTarget lib facet else if let some lib := ws.findLeanLib? target then - resolveLibTarget lib facet + Array.singleton <$> resolveLibTarget lib facet else if let some pkg := ws.findPackage? target then resolvePackageTarget ws pkg facet else if let some mod := ws.findModule? target then - resolveModuleTarget ws mod facet + Array.singleton <$> resolveModuleTarget ws mod facet else throw <| CliError.unknownTarget target -def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet : Name) : Except CliError OpaqueTarget := do +def resolveTargetBaseSpec +(ws : Workspace) (spec : String) (facet : Name) : Except CliError (Array BuildSpec) := do match spec.splitOn "/" with | [spec] => if spec.isEmpty then @@ -118,7 +146,7 @@ def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet : Name) : Exce else if spec.startsWith "+" then let mod := spec.drop 1 |>.toName if let some mod := ws.findModule? mod then - resolveModuleTarget ws mod facet + Array.singleton <$> resolveModuleTarget ws mod facet else throw <| CliError.unknownModule mod else @@ -131,19 +159,27 @@ def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet : Name) : Exce else if targetSpec.startsWith "+" then let mod := targetSpec.drop 1 |>.toName if let some mod := pkg.findModule? mod then - resolveModuleTarget ws mod facet + Array.singleton <$> resolveModuleTarget ws mod facet else throw <| CliError.unknownModule mod else - resolveTargetInPackage ws pkg targetSpec facet + Array.singleton <$> resolveTargetInPackage ws pkg targetSpec facet | _ => throw <| CliError.invalidTargetSpec spec '/' -def parseTargetSpec (ws : Workspace) (spec : String) : Except CliError OpaqueTarget := do +def parseTargetSpec (ws : Workspace) (spec : String) : Except CliError (Array BuildSpec) := do match spec.splitOn ":" with | [spec] => resolveTargetBaseSpec ws spec .anonymous | [rootSpec, facet] => - resolveTargetBaseSpec ws rootSpec (Name.ofString facet) + resolveTargetBaseSpec ws rootSpec facet.toName | _ => throw <| CliError.invalidTargetSpec spec ':' + +def parseTargetSpecs (ws : Workspace) (specs : List String) : Except CliError (Array BuildSpec) := do + let mut results := #[] + for spec in specs do + results := results ++ (← parseTargetSpec ws spec) + if results.isEmpty then + results ← resolveDefaultPackageTarget ws ws.root + return results diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean index 63a6bffff5..132a2a9c85 100644 --- a/Lake/CLI/Main.lean +++ b/Lake/CLI/Main.lean @@ -300,14 +300,9 @@ protected def build : CliM PUnit := do let config ← mkLoadConfig opts let ws ← loadWorkspace config let targetSpecs ← takeArgs - let target ← show Except _ _ from do - let targets ← targetSpecs.mapM <| parseTargetSpec ws - if targets.isEmpty then - resolveDefaultPackageTarget ws ws.root - else - return Target.collectOpaqueList targets + let specs ← parseTargetSpecs ws targetSpecs let ctx ← mkBuildContext ws - BuildM.run MonadLog.io ctx target.build + BuildM.run MonadLog.io ctx <| buildSpecs specs protected def update : CliM PUnit := do processOptions lakeOption diff --git a/Lake/Config/FacetConfig.lean b/Lake/Config/FacetConfig.lean index 752a8ee0b2..568bcaaca8 100644 --- a/Lake/Config/FacetConfig.lean +++ b/Lake/Config/FacetConfig.lean @@ -12,8 +12,8 @@ namespace Lake structure FacetConfig (DataFam : Name → Type) (ι : Type) (name : Name) : Type where /-- The facet's build (function). -/ build : ι → IndexBuildM (DataFam name) - /-- Is this facet a buildable target? -/ - toTarget? : (info : BuildInfo) → BuildData info.key = DataFam name → Option OpaqueTarget + /-- Does this facet produce an associated asynchronous job? -/ + getJob? : Option (DataFam name → Job) deriving Inhabited protected abbrev FacetConfig.name (_ : FacetConfig DataFam ι name) := name @@ -22,7 +22,7 @@ protected abbrev FacetConfig.name (_ : FacetConfig DataFam ι name) := name @[inline] def mkFacetConfig (build : ι → IndexBuildM α) [h : FamilyDef Fam facet α] : FacetConfig Fam ι facet where build := cast (by rw [← h.family_key_eq_type]) build - toTarget? := fun _ _ => none + getJob? := none /-- A dependently typed configuration based on its registered name. -/ structure NamedConfigDecl (β : Name → Type u) where diff --git a/Lake/Config/Glob.lean b/Lake/Config/Glob.lean index 227d10ac8b..ceb503d17d 100644 --- a/Lake/Config/Glob.lean +++ b/Lake/Config/Glob.lean @@ -27,10 +27,10 @@ partial def forEachModuleIn [Monad m] [MonadLiftT IO m] (dir : FilePath) (f : Name → m PUnit) : m PUnit := do for entry in (← dir.readDir) do if (← liftM (m := IO) <| entry.path.isDir) then - let n := Name.ofString <| entry.fileName + let n := entry.fileName.toName f n *> forEachModuleIn entry.path (f <| n ++ ·) else if entry.path.extension == some "lean" then - f <| Name.ofString <| FilePath.withExtension entry.fileName "" |>.toString + f <| FilePath.withExtension entry.fileName "" |>.toString.toName namespace Glob diff --git a/Lake/Util/Name.lean b/Lake/Util/Name.lean index 2afa4d9627..7c2b397a9c 100644 --- a/Lake/Util/Name.lean +++ b/Lake/Util/Name.lean @@ -17,9 +17,6 @@ export Lean (Name NameMap) namespace Name open Lean.Name -def ofString (str : String) : Name := - str.splitOn "." |>.foldl (fun n p => .str n p.trim) .anonymous - @[simp] protected theorem beq_false (m n : Name) : (m == n) = false ↔ ¬ (m = n) := by rw [← beq_iff_eq m n]; cases m == n <;> simp