diff --git a/src/lake/Lake/Build/Basic.lean b/src/lake/Lake/Build/Basic.lean index a7e62e838ca1..f8ec65e00eeb 100644 --- a/src/lake/Lake/Build/Basic.lean +++ b/src/lake/Lake/Build/Basic.lean @@ -39,11 +39,12 @@ abbrev JobTask α := BaseIOTask (JobResult α) /-- A Lake job. -/ structure Job (α : Type u) where task : JobTask α + caption : String /-- A Lake context with a build configuration and additional build data. -/ structure BuildContext extends BuildConfig, Context where leanTrace : BuildTrace - registeredJobs : IO.Ref (Array (String × Job Unit)) + registeredJobs : IO.Ref (Array (Job Unit)) /-- A transformer to equip a monad with a `BuildContext`. -/ abbrev BuildT := ReaderT BuildContext @@ -81,7 +82,7 @@ instance [Pure m] : MonadLift LakeM (BuildT m) where /-- The internal core monad of Lake builds. Not intended for user use. -/ abbrev CoreBuildM := BuildT LogIO -/-- The monad of asynchronous Lake jobs. -/ +/-- The monad of asynchronous Lake jobs. Lifts into `FetchM`. -/ abbrev JobM := CoreBuildM /-- The monad used to spawn asynchronous Lake build jobs. Lifts into `FetchM`. -/ @@ -89,3 +90,13 @@ abbrev SpawnM := BuildT BaseIO /-- The monad used to spawn asynchronous Lake build jobs. **Replaced by `SpawnM`.** -/ @[deprecated SpawnM] abbrev SchedulerM := SpawnM + +/-- +Logs a build step with `message`. + +**Deprecated:** Build steps are now managed by a top-level build monitor. +As a result, this no longer functions the way it used to. It now just logs the +`message` via `logVerbose`. +-/ +@[deprecated] def logStep (message : String) : JobM Unit := do + logVerbose message diff --git a/src/lake/Lake/Build/Facets.lean b/src/lake/Lake/Build/Facets.lean index 95013cbc8264..44c8efd3c3ad 100644 --- a/src/lake/Lake/Build/Facets.lean +++ b/src/lake/Lake/Build/Facets.lean @@ -116,6 +116,13 @@ module_data o.noexport : BuildJob FilePath /-! ## Package Facets -/ +/-- +A package's *optional* cloud build release. +Does not fail if the release cannot be fetched. +-/ +abbrev Package.optReleaseFacet := `optRelease +package_data optRelease : BuildJob Bool + /-- A package's cloud build release. -/ abbrev Package.releaseFacet := `release package_data release : BuildJob Unit diff --git a/src/lake/Lake/Build/Fetch.lean b/src/lake/Lake/Build/Fetch.lean index b0129718cf64..cc6e389cc14c 100644 --- a/src/lake/Lake/Build/Fetch.lean +++ b/src/lake/Lake/Build/Fetch.lean @@ -72,19 +72,46 @@ abbrev FetchM := IndexT RecBuildM export BuildInfo (fetch) -/-- Register the produced job for the CLI progress UI. -/ -def withRegisterJob - (caption : String) (x : FetchM (Job α)) +/-- Wraps stray I/O, logs, and errors in `x` into the produced job. -/ +def ensureJob (x : FetchM (Job α)) : FetchM (Job α) := fun fetch stack ctx log store => do let iniPos := log.endPos match (← (withLoggedIO x) fetch stack ctx log store) with | (.ok job log, store) => let (log, jobLog) := log.split iniPos - let regJob := job.mapResult (discard <| ·.modifyState (jobLog ++ ·)) - ctx.registeredJobs.modify (·.push (caption, regJob)) - return (.ok job.clearLog log, store) + let job := if jobLog.isEmpty then job else + job.mapResult (sync := true) (·.modifyState (jobLog ++ ·)) + return (.ok job log, store) | (.error _ log, store) => let (log, jobLog) := log.split iniPos - let regJob := ⟨Task.pure <| .error 0 jobLog⟩ - ctx.registeredJobs.modify (·.push (caption, regJob)) - return (.ok .error log, store) + return (.ok (.error jobLog) log, store) + +/-- +Registers the produced job for the top-level build monitor +(e.g., the Lake CLI progress UI), assigning it `caption`. + +Stray I/O, logs, and errors produced by `x` will be wrapped into the job. +-/ +@[inline] def withRegisterJob + (caption : String) (x : FetchM (Job α)) +: FetchM (Job α) := do + let job ← ensureJob x + let job := job.setCaption caption + let regJob := job.mapResult (sync := true) discard + (← readThe BuildContext).registeredJobs.modify (·.push regJob) + return job.clearLog + +/-- +Registers the produced job for the top-level build monitor +if it is not already (i.e., it has an empty caption). +-/ +@[inline] def maybeRegisterJob + (fallbackCaption : String) (job : Job α) +: FetchM (Job α) := do + if job.caption.isEmpty then + let job := job.setCaption fallbackCaption + let regJob := job.mapResult (sync := true) discard + (← readThe BuildContext).registeredJobs.modify (·.push regJob) + return job.clearLog + else + return job diff --git a/src/lake/Lake/Build/Info.lean b/src/lake/Lake/Build/Info.lean index cb2aa08e616f..9427e367b1e2 100644 --- a/src/lake/Lake/Build/Info.lean +++ b/src/lake/Lake/Build/Info.lean @@ -220,6 +220,10 @@ abbrev Package.facet (facet : Name) (self : Package) : BuildInfo := abbrev Package.release (self : Package) : BuildInfo := self.facet releaseFacet +@[inherit_doc optReleaseFacet] +abbrev Package.optRelease (self : Package) : BuildInfo := + self.facet optReleaseFacet + @[inherit_doc extraDepFacet] abbrev Package.extraDep (self : Package) : BuildInfo := self.facet extraDepFacet diff --git a/src/lake/Lake/Build/Job.lean b/src/lake/Lake/Build/Job.lean index 3e5a5c7d216c..f54a1b9ef8c6 100644 --- a/src/lake/Lake/Build/Job.lean +++ b/src/lake/Lake/Build/Job.lean @@ -12,23 +12,39 @@ namespace Lake namespace Job -@[inline] protected def pure (a : α) : Job α := - {task := Task.pure (.ok a {})} +@[inline] def ofTask (task : JobTask α) (caption := "") : Job α := + {task, caption} + +@[inline] protected def error (l : Log := {}) (caption := "") : Job α := + {task := Task.pure (.error 0 l), caption} + +@[inline] protected def pure (a : α) (l : Log := {}) (caption := "") : Job α := + {task := Task.pure (.ok a l), caption} instance : Pure Job := ⟨Job.pure⟩ instance [Inhabited α] : Inhabited (Job α) := ⟨pure default⟩ -@[inline] protected def nop : Job Unit := - pure () +@[inline] protected def nop (l : Log := {}) (caption := "") : Job Unit := + .pure () l caption -@[inline] protected def error (l : Log := {}) : Job α := - {task := Task.pure (.error 0 l)} +/-- Sets the job's caption. -/ +@[inline] def setCaption (caption : String) (job : Job α) : Job α := + {job with caption} + +/-- Sets the job's caption if the job's current caption is empty. -/ +@[inline] def setCaption? (caption : String) (job : Job α) : Job α := + if job.caption.isEmpty then {job with caption} else job @[inline] def mapResult (f : JobResult α → JobResult β) (self : Job α) (prio := Task.Priority.default) (sync := false) : Job β := - {task := self.task.map f prio sync} + {self with task := self.task.map f prio sync} + +@[inline] def bindTask [Monad m] + (f : JobTask α → m (JobTask β)) (self : Job α) +: m (Job β) := + return {self with task := ← f self.task} @[inline] protected def map (f : α → β) (self : Job α) @@ -56,7 +72,7 @@ instance : Functor Job where map := Job.map /-- Spawn a job that asynchronously performs `act`. -/ @[inline] protected def async (act : JobM α) (prio := Task.Priority.default) -: SpawnM (Job α) := fun ctx => Job.mk <$> do +: SpawnM (Job α) := fun ctx => .ofTask <$> do BaseIO.asTask (prio := prio) do (withLoggedIO act) ctx {} /-- Wait a the job to complete and return the result. -/ @@ -86,8 +102,8 @@ after the job `a` completes. @[inline] protected def bindSync (self : Job α) (f : α → JobM β) (prio := Task.Priority.default) (sync := false) -: SpawnM (Job β) := fun ctx => Job.mk <$> do - BaseIO.mapTask (t := self.task) (prio := prio) (sync := sync) fun +: SpawnM (Job β) := fun ctx => self.bindTask fun task => do + BaseIO.mapTask (t := task) (prio := prio) (sync := sync) fun | EResult.ok a l => (withLoggedIO (f a)) ctx l | EResult.error n l => return .error n l @@ -98,8 +114,8 @@ after the job `a` completes and then merges into the job produced by `b`. @[inline] protected def bindAsync (self : Job α) (f : α → SpawnM (Job β)) (prio := Task.Priority.default) (sync := false) -: SpawnM (Job β) := fun ctx => Job.mk <$> do - BaseIO.bindTask self.task (prio := prio) (sync := sync) fun +: SpawnM (Job β) := fun ctx => self.bindTask fun task => do + BaseIO.bindTask task (prio := prio) (sync := sync) fun | .ok a l => do let job ← f a ctx if l.isEmpty then return job.task else @@ -115,7 +131,7 @@ results of `a` and `b`. The job `c` errors if either `a` or `b` error. @[inline] def zipWith (f : α → β → γ) (x : Job α) (y : Job β) (prio := Task.Priority.default) (sync := false) -: BaseIO (Job γ) := Job.mk <$> do +: BaseIO (Job γ) := Job.ofTask <$> do BaseIO.bindTask x.task (prio := prio) (sync := true) fun rx => BaseIO.mapTask (t := y.task) (prio := prio) (sync := sync) fun ry => match rx, ry with @@ -147,14 +163,14 @@ namespace BuildJob instance : Pure BuildJob := ⟨BuildJob.pure⟩ @[inline] def attempt (self : BuildJob α) : BuildJob Bool := - {task := self.toJob.task.map fun + self.mapResult fun | .error _ l => .ok (false, nilTrace) l - | .ok (_, t) l => .ok (true, t) l} + | .ok (_, t) l => .ok (true, t) l @[inline] def attempt? (self : BuildJob α) : BuildJob (Option α) := - {task := self.toJob.task.map fun + self.mapResult fun | .error _ l => .ok (none, nilTrace) l - | .ok (a, t) l => .ok (some a, t) l} + | .ok (a, t) l => .ok (some a, t) l @[inline] protected def map (f : α → β) (self : BuildJob α) : BuildJob β := mk <| (fun (a,t) => (f a,t)) <$> self.toJob diff --git a/src/lake/Lake/Build/Key.lean b/src/lake/Lake/Build/Key.lean index 6b1ebd9377ef..c3b540d01cfe 100644 --- a/src/lake/Lake/Build/Key.lean +++ b/src/lake/Lake/Build/Key.lean @@ -23,6 +23,18 @@ def toString : (self : BuildKey) → String | targetFacet p t f => s!"{p}/{t}:{f}" | customTarget p t => s!"{p}/{t}" +/-- Like the default `toString`, but without disambiguation markers. -/ +def toSimpleString : (self : BuildKey) → String +| moduleFacet m f => s!"{m}:{f}" +| packageFacet p f => s!"{p}:{f}" +| targetFacet p t f => s!"{p}/{t}:{eraseHead f}" +| customTarget p t => s!"{p}/{t}" +where + eraseHead : Name → Name + | .anonymous | .str .anonymous _ | .num .anonymous _ => .anonymous + | .str p s => .str (eraseHead p) s + | .num p s => .num (eraseHead p) s + instance : ToString BuildKey := ⟨(·.toString)⟩ def quickCmp (k k' : BuildKey) : Ordering := diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean index 6652e291a79e..4a8a3519741c 100644 --- a/src/lake/Lake/Build/Package.lean +++ b/src/lake/Lake/Build/Package.lean @@ -35,9 +35,9 @@ def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) := job ← job.mix <| ← dep.extraDep.fetch -- Fetch pre-built release if desired and this package is a dependency if self.name ≠ (← getWorkspace).root.name ∧ self.preferReleaseBuild then - job ← job.add <| ← (← self.release.fetch).attempt.bindSync fun success t => do + job ← job.add <| ← (← self.optRelease.fetch).bindSync fun success t => do unless success do - logWarning "fetching cloud release failed; falling back to local build" + logWarning "failed to fetch cloud release; falling back to local build" return ((), t) -- Build this package's extra dep targets for target in self.extraDepTargets do @@ -49,16 +49,17 @@ def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet := mkFacetJobConfig Package.recBuildExtraDepTargets /-- Download and unpack the package's prebuilt release archive (from GitHub). -/ -def Package.fetchRelease (self : Package) : FetchM (BuildJob Unit) := - withRegisterJob s!"Fetching {self.name} cloud release" <| Job.async do +def Package.fetchOptRelease (self : Package) : FetchM (BuildJob Bool) := Job.async do let repo := GitRepo.mk self.dir let repoUrl? := self.releaseRepo? <|> self.remoteUrl? let some repoUrl := repoUrl? <|> (← repo.getFilteredRemoteUrl?) - | error <| s!"{self.name}: wanted prebuilt release, " ++ - "but package's repository URL was not known; it may need to set `releaseRepo?`" + | logInfo s!"{self.name}: wanted prebuilt release, \ + but package's repository URL was not known; it may need to set 'releaseRepo'" + return (false, .nil) let some tag ← repo.findTag? - | error <| s!"{self.name}: wanted prebuilt release, " ++ - "but could not find an associated tag for the package's revision" + | logInfo s!"{self.name}: wanted prebuilt release, \ + but could not find an associated tag for the package's revision" + return (false, .nil) let url := s!"{repoUrl}/releases/download/{tag}/{self.buildArchive}" let logName := s!"{self.name}/{tag}/{self.buildArchive}" let depTrace := Hash.ofString url @@ -69,11 +70,20 @@ def Package.fetchRelease (self : Package) : FetchM (BuildJob Unit) := unless upToDate && (← self.buildDir.pathExists) do logVerbose s!"unpacking {logName}" untar self.buildArchiveFile self.buildDir - return ((), .nil) + return (true, .nil) + +/-- The `PackageFacetConfig` for the builtin `optReleaseFacet`. -/ +def Package.optReleaseFacetConfig : PackageFacetConfig optReleaseFacet := + mkFacetJobConfig (·.fetchOptRelease) /-- The `PackageFacetConfig` for the builtin `releaseFacet`. -/ def Package.releaseFacetConfig : PackageFacetConfig releaseFacet := - mkFacetJobConfig (·.fetchRelease) + mkFacetJobConfig fun pkg => + withRegisterJob s!"Fetching {pkg.name} cloud release" do + (← pkg.optRelease.fetch).bindSync fun success t => do + unless success do + error "failed to fetch cloud release" + return ((), t) /-- Perform a build job after first checking for a cloud release for the package. -/ def Package.afterReleaseAsync (self : Package) (build : SpawnM (Job α)) : FetchM (Job α) := do @@ -98,4 +108,5 @@ def initPackageFacetConfigs : DNameMap PackageFacetConfig := DNameMap.empty |>.insert depsFacet depsFacetConfig |>.insert extraDepFacet extraDepFacetConfig + |>.insert optReleaseFacet optReleaseFacetConfig |>.insert releaseFacet releaseFacetConfig diff --git a/src/lake/Lake/Build/Run.lean b/src/lake/Lake/Build/Run.lean index bcb6d75b05b1..b2d7f58a74d7 100644 --- a/src/lake/Lake/Build/Run.lean +++ b/src/lake/Lake/Build/Run.lean @@ -27,7 +27,7 @@ def mkBuildContext (ws : Workspace) (config : BuildConfig) : BaseIO BuildContext /-- The job monitor function. An auxiliary definition for `runFetchM`. -/ partial def monitorJobs - (jobs : Array (String × Job Unit)) + (jobs : Array (Job Unit)) (out : IO.FS.Stream) (failLv outLv : LogLevel) (showANSIProgress : Bool) @@ -42,25 +42,25 @@ where let mut unfinishedJobs := #[] let mut failures := initFailures let mut resetCtrl := resetCtrl - for jobEntry@(caption, job) in jobs do + for job in jobs do if (← IO.hasFinished job.task) then let log := job.task.get.state let failed := log.hasEntriesGe failLv if failed then - failures := failures.push caption + failures := failures.push job.caption if log.hasEntriesGe outLv then let jobsDone := totalJobs - jobs.size + unfinishedJobs.size + 1 - out.putStr s!"{resetCtrl}[{jobsDone}/{totalJobs}] {caption}\n" + out.putStr s!"{resetCtrl}[{jobsDone}/{totalJobs}] {job.caption}\n" resetCtrl := "" let outLv := if failed then .trace else outLv log.replay (logger := MonadLog.stream out outLv) out.flush else - unfinishedJobs := unfinishedJobs.push jobEntry + unfinishedJobs := unfinishedJobs.push job if h : 0 < unfinishedJobs.size then if showANSIProgress then let jobsDone := totalJobs - jobs.size - let (caption, _) := unfinishedJobs[0]'h + let caption := unfinishedJobs[0]'h |>.caption out.putStr s!"{resetCtrl}[{jobsDone}/{totalJobs}] {caption}" resetCtrl := "\x1B[2K\r" out.flush @@ -74,6 +74,15 @@ where out.putStr resetCtrl return failures +/-- +Whether the build should show progress information. + +`Verbosity.quiet` hides progress and, for a `noBuild`, +`Verbosity.verbose` shows progress. +-/ +def BuildConfig.showProgress (cfg : BuildConfig) : Bool := + (cfg.noBuild ∧ cfg.verbosity == .verbose) ∨ cfg.verbosity != .quiet + /-- Run a build function in the Workspace's context using the provided configuration. Reports incremental build progress and build logs. In quiet mode, only reports @@ -86,12 +95,9 @@ def Workspace.runFetchM let ctx ← mkBuildContext ws cfg let out ← if cfg.useStdout then IO.getStdout else IO.getStderr let useANSI ← out.isTty - let verbosity := cfg.verbosity - let outLv := verbosity.minLogLevel - let failLv : LogLevel := if ctx.failIfWarnings then .warning else .error - let showProgress := - (cfg.noBuild ∧ verbosity == .verbose) ∨ - verbosity != .quiet + let outLv := cfg.verbosity.minLogLevel + let failLv : LogLevel := if cfg.failIfWarnings then .warning else .error + let showProgress := cfg.showProgress let showANSIProgress := showProgress ∧ useANSI -- Job Computation let caption := "Computing build jobs" @@ -104,7 +110,7 @@ def Workspace.runFetchM if log.hasEntriesGe outLv then unless showANSIProgress do out.putStr header - out.putStr "\n" + out.putStr "\n" let outLv := if failed then .trace else outLv log.replay (logger := MonadLog.stream out outLv) out.flush diff --git a/src/lake/Lake/CLI/Build.lean b/src/lake/Lake/CLI/Build.lean index f3dcac127cca..29a5c7cd5642 100644 --- a/src/lake/Lake/CLI/Build.lean +++ b/src/lake/Lake/CLI/Build.lean @@ -29,8 +29,9 @@ structure BuildSpec where | throw <| CliError.nonCliFacet facetType facet return {info, getBuildJob := h ▸ getJob} -@[inline] protected def BuildSpec.fetch (self : BuildSpec) : FetchM (BuildJob Unit) := - self.getBuildJob <$> self.info.fetch +@[inline] protected def BuildSpec.fetch (self : BuildSpec) : FetchM (BuildJob Unit) := do + maybeRegisterJob s!"Building {self.info.key.toSimpleString}" <| ← do + self.getBuildJob <$> self.info.fetch def buildSpecs (specs : Array BuildSpec) : FetchM (BuildJob Unit) := do BuildJob.mixArray (← specs.mapM (·.fetch)) diff --git a/src/lake/Lake/DSL/Targets.lean b/src/lake/Lake/DSL/Targets.lean index f1f68d418253..308f5640a334 100644 --- a/src/lake/Lake/DSL/Targets.lean +++ b/src/lake/Lake/DSL/Targets.lean @@ -20,10 +20,13 @@ syntax buildDeclSig := /-! ## Facet Declarations -/ -------------------------------------------------------------------------------- -@[inline] def mkModuleFacetJob - (mod : Module) (facet : Name) (f : Module → FetchM (BuildJob α)) -: FetchM (BuildJob α) := do - withRegisterJob s!"Building {mod.name}:{facet}" (f mod) +abbrev mkModuleFacetDecl + (α) (facet : Name) + [FamilyDef ModuleData facet (BuildJob α)] + (f : Module → FetchM (BuildJob α)) +: ModuleFacetDecl := .mk facet <| mkFacetJobConfig fun mod => do + withRegisterJob s!"Building {mod.facet facet |>.key.toSimpleString}" + (f mod) /-- Define a new module facet. Has one form: @@ -42,21 +45,22 @@ kw:"module_facet " sig:buildDeclSig : command => do | `(buildDeclSig| $id:ident $[$mod?]? : $ty := $defn $[$wds?:whereDecls]?) => let attr ← withRef kw `(Term.attrInstance| module_facet) let attrs := #[attr] ++ expandAttrs attrs? - let name := Name.quoteFrom id id.getId - let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_modFacet") + let facet := Name.quoteFrom id id.getId + let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_modFacet") let mod ← expandOptSimpleBinder mod? `(module_data $id : BuildJob $ty - $[$doc?:docComment]? @[$attrs,*] abbrev $facetId : ModuleFacetDecl := { - name := $name - config := Lake.mkFacetJobConfig fun mod => - Lake.DSL.mkModuleFacetJob (α := $ty) mod $name (fun $mod => $defn) - } $[$wds?:whereDecls]?) + $[$doc?:docComment]? @[$attrs,*] abbrev $declId := + Lake.DSL.mkModuleFacetDecl $ty $facet (fun $mod => $defn) + $[$wds?:whereDecls]?) | stx => Macro.throwErrorAt stx "ill-formed module facet declaration" -@[inline] def mkPackageFacetJob - (pkg : Package) (facet : Name) (f : Package → FetchM (BuildJob α)) -: FetchM (BuildJob α) := do - withRegisterJob s!"Building {pkg.name}:{facet}" (f pkg) +abbrev mkPackageFacetDecl + (α) (facet : Name) + [FamilyDef PackageData facet (BuildJob α)] + (f : Package → FetchM (BuildJob α)) +: PackageFacetDecl := .mk facet <| mkFacetJobConfig fun pkg => do + withRegisterJob s!"Building {pkg.facet facet |>.key.toSimpleString}" + (f pkg) /-- Define a new package facet. Has one form: @@ -75,21 +79,22 @@ kw:"package_facet " sig:buildDeclSig : command => do | `(buildDeclSig| $id:ident $[$pkg?]? : $ty := $defn $[$wds?:whereDecls]?) => let attr ← withRef kw `(Term.attrInstance| package_facet) let attrs := #[attr] ++ expandAttrs attrs? - let name := Name.quoteFrom id id.getId - let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_pkgFacet") + let facet := Name.quoteFrom id id.getId + let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_pkgFacet") let pkg ← expandOptSimpleBinder pkg? `(package_data $id : BuildJob $ty - $[$doc?]? @[$attrs,*] abbrev $facetId : PackageFacetDecl := { - name := $name - config := Lake.mkFacetJobConfig fun pkg => - Lake.DSL.mkPackageFacetJob (α := $ty) pkg $name (fun $pkg => $defn) - } $[$wds?:whereDecls]?) + $[$doc?]? @[$attrs,*] abbrev $declId := + Lake.DSL.mkPackageFacetDecl $ty $facet (fun $pkg => $defn) + $[$wds?:whereDecls]?) | stx => Macro.throwErrorAt stx "ill-formed package facet declaration" -@[inline] def mkLibraryFacetJob - (lib : LeanLib) (facet : Name) (f : LeanLib → FetchM (BuildJob α)) -: FetchM (BuildJob α) := do - withRegisterJob s!"Building {lib.name}:{facet}" (f lib) +abbrev mkLibraryFacetDecl + (α) (facet : Name) + [FamilyDef LibraryData facet (BuildJob α)] + (f : LeanLib → FetchM (BuildJob α)) +: LibraryFacetDecl := .mk facet <| mkFacetJobConfig fun lib => do + withRegisterJob s!"Building {lib.facet facet |>.key.toSimpleString}" + (f lib) /-- Define a new library facet. Has one form: @@ -108,25 +113,26 @@ kw:"library_facet " sig:buildDeclSig : command => do | `(buildDeclSig| $id:ident $[$lib?]? : $ty := $defn $[$wds?:whereDecls]?) => let attr ← withRef kw `(Term.attrInstance| library_facet) let attrs := #[attr] ++ expandAttrs attrs? - let name := Name.quoteFrom id id.getId - let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_libFacet") + let facet := Name.quoteFrom id id.getId + let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_libFacet") let lib ← expandOptSimpleBinder lib? `(library_data $id : BuildJob $ty - $[$doc?]? @[$attrs,*] abbrev $facetId : LibraryFacetDecl := { - name := $name - config := Lake.mkFacetJobConfig fun lib => - Lake.DSL.mkLibraryFacetJob (α := $ty) lib $name (fun $lib => $defn) - } $[$wds?:whereDecls]?) + $[$doc?]? @[$attrs,*] abbrev $declId : LibraryFacetDecl := + Lake.DSL.mkLibraryFacetDecl $ty $facet (fun $lib => $defn) + $[$wds?:whereDecls]?) | stx => Macro.throwErrorAt stx "ill-formed library facet declaration" -------------------------------------------------------------------------------- /-! ## Custom Target Declaration -/ -------------------------------------------------------------------------------- -@[inline] def mkTargetJob - (pkg : NPackage n) (target : Name) (f : NPackage n → FetchM (BuildJob α)) -: FetchM (BuildJob α) := do - withRegisterJob s!"Building {n}/{target}" (f pkg) +abbrev mkTargetDecl + (α) (pkgName target : Name) + [FamilyDef CustomData (pkgName, target) (BuildJob α)] + (f : NPackage pkgName → FetchM (BuildJob α)) +: TargetDecl := .mk pkgName target <| mkTargetJobConfig fun pkg => do + withRegisterJob s!"Building {pkg.target target |>.key.toSimpleString}" + (f pkg) /-- Define a new custom target for the package. Has one form: @@ -151,12 +157,9 @@ kw:"target " sig:buildDeclSig : command => do let pkgName := mkIdentFrom id `_package.name let pkg ← expandOptSimpleBinder pkg? `(family_def $id : CustomData ($pkgName, $name) := BuildJob $ty - $[$doc?]? @[$attrs,*] abbrev $id : TargetDecl := { - pkg := $pkgName - name := $name - config := Lake.mkTargetJobConfig fun pkg => - Lake.DSL.mkTargetJob (α := $ty) pkg $name (fun $pkg => $defn) - } $[$wds?:whereDecls]?) + $[$doc?]? @[$attrs,*] abbrev $id := + Lake.DSL.mkTargetDecl $ty $pkgName $name (fun $pkg => $defn) + $[$wds?:whereDecls]?) | stx => Macro.throwErrorAt stx "ill-formed target declaration" diff --git a/src/lake/examples/targets/test.sh b/src/lake/examples/targets/test.sh index 55fc1f3de412..db6c8208aa86 100755 --- a/src/lake/examples/targets/test.sh +++ b/src/lake/examples/targets/test.sh @@ -28,20 +28,20 @@ $LAKE build bark | awk '/Building/,/Bark!/' | diff -u --strip-trailing-cr <(cat info: Bark! EOF ) - -$LAKE build targets/bark_bark | awk '/Building/,/bark_bark/' | diff -u --strip-trailing-cr <(cat << 'EOF' +$LAKE build targets/bark_bark | awk '/Building/,0' | diff -u --strip-trailing-cr <(cat << 'EOF' [1/2] Building targets/bark info: Bark! -[2/2] Building targets/bark_bark +All builds jobs completed successfully. EOF ) - -$LAKE build targets:print_name | awk '/Building/,0' | diff -u --strip-trailing-cr <(cat << 'EOF' +$LAKE build targets:print_name | awk '/Building/,/^targets/' | diff -u --strip-trailing-cr <(cat << 'EOF' [1/1] Building targets:print_name info: stdout/stderr: targets EOF ) - -$LAKE build Foo:print_name | awk '/Building/,0' | diff -u --strip-trailing-cr <(cat << 'EOF' -[1/1] Building Foo:print_name +$LAKE build Foo:print_name | awk '/Building/,/^Foo/' | diff -u --strip-trailing-cr <(cat << 'EOF' +[1/1] Building targets/Foo:print_name info: stdout/stderr: Foo EOF diff --git a/src/lake/tests/noRelease/clean.sh b/src/lake/tests/noRelease/clean.sh new file mode 100755 index 000000000000..b6e54c681e54 --- /dev/null +++ b/src/lake/tests/noRelease/clean.sh @@ -0,0 +1 @@ +rm -rf .lake lake-manifest.json diff --git a/src/lake/tests/noRelease/dep/lakefile.lean b/src/lake/tests/noRelease/dep/lakefile.lean new file mode 100644 index 000000000000..ce123925d29c --- /dev/null +++ b/src/lake/tests/noRelease/dep/lakefile.lean @@ -0,0 +1,6 @@ +import Lake +open Lake DSL + +package dep where + preferReleaseBuild := true + releaseRepo := "https://example.com" diff --git a/src/lake/tests/noRelease/lakefile.lean b/src/lake/tests/noRelease/lakefile.lean new file mode 100644 index 000000000000..8a0940dfdc52 --- /dev/null +++ b/src/lake/tests/noRelease/lakefile.lean @@ -0,0 +1,5 @@ +import Lake +open Lake DSL + +package test +require dep from "dep" diff --git a/src/lake/tests/noRelease/test.sh b/src/lake/tests/noRelease/test.sh new file mode 100755 index 000000000000..7a13c118a10f --- /dev/null +++ b/src/lake/tests/noRelease/test.sh @@ -0,0 +1,29 @@ +#!/usr/bin/env bash +set -euxo pipefail + +LAKE=${LAKE:-../../.lake/build/bin/lake} + +./clean.sh + +# --- +# Test Lake's behavior when failing to fetch a cloud release +# --- + +# Test that a direct invocation fo `lake build *:release` fails +($LAKE build dep:release && exit 1 || true) | diff -u --strip-trailing-cr <(cat << 'EOF' +[1/1] Fetching dep cloud release +info: dep: wanted prebuilt release, but could not find an associated tag for the package's revision +error: failed to fetch cloud release +Some build steps logged failures: +- Fetching dep cloud release +EOF +) - + +# Test that an indirect fetch on the release does not cause the build to fail +$LAKE build -v test:extraDep | diff -u --strip-trailing-cr <(cat << 'EOF' +[1/1] Building test:extraDep +info: dep: wanted prebuilt release, but could not find an associated tag for the package's revision +warning: failed to fetch cloud release; falling back to local build +All builds jobs completed successfully. +EOF +) -