diff --git a/src/lake/Lake/Build/Basic.lean b/src/lake/Lake/Build/Basic.lean
index 183b897a43..d658c7da76 100644
--- a/src/lake/Lake/Build/Basic.lean
+++ b/src/lake/Lake/Build/Basic.lean
@@ -51,8 +51,24 @@ Whether the build should show progress information.
def BuildConfig.showProgress (cfg : BuildConfig) : Bool :=
(cfg.noBuild ∧ cfg.verbosity == .verbose) ∨ cfg.verbosity != .quiet
+/-- The core structure of a Lake job. -/
+structure JobCore (α : Type u) where
+ /-- The Lean `Task` object for the job. -/
+ task : α
+ /--
+ A caption for the job in Lake's build monitor.
+ Will be formatted like `✔ [3/5] Ran
`.
+ -/
+ caption : String
+ /-- Whether this job failing should cause the build to fail. -/
+ optional : Bool := false
+ deriving Inhabited
+
+/-- A Lake job task with an opaque value type in `Type`. -/
+declare_opaque_type OpaqueJobTask
+
/-- A Lake job with an opaque value type in `Type`. -/
-declare_opaque_type OpaqueJob
+abbrev OpaqueJob := JobCore OpaqueJobTask
/-- A Lake context with a build configuration and additional build data. -/
structure BuildContext extends BuildConfig, Context where
diff --git a/src/lake/Lake/Build/Facets.lean b/src/lake/Lake/Build/Facets.lean
index 44c8efd3c3..67c32462bb 100644
--- a/src/lake/Lake/Build/Facets.lean
+++ b/src/lake/Lake/Build/Facets.lean
@@ -118,12 +118,15 @@ module_data o.noexport : BuildJob FilePath
/--
A package's *optional* cloud build release.
-Does not fail if the release cannot be fetched.
+Will not cause the whole build to fail if the release cannot be fetched.
-/
abbrev Package.optReleaseFacet := `optRelease
package_data optRelease : BuildJob Bool
-/-- A package's cloud build release. -/
+/--
+A package's cloud build release.
+Will cause the whole build to fail if the release cannot be fetched.
+-/
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 8bf894d56c..4359122c41 100644
--- a/src/lake/Lake/Build/Fetch.lean
+++ b/src/lake/Lake/Build/Fetch.lean
@@ -104,8 +104,8 @@ def ensureJob (x : FetchM (Job α))
Registers the job for the top-level build monitor,
(e.g., the Lake CLI progress UI), assigning it `caption`.
-/
-def registerJob (caption : String) (job : Job α) : FetchM (Job α) := do
- let job := job.setCaption caption
+def registerJob (caption : String) (job : Job α) (optional := false) : FetchM (Job α) := do
+ let job : Job α := {job with caption, optional}
(← getBuildContext).registeredJobs.modify (·.push job)
return job.renew
@@ -116,10 +116,10 @@ Registers the produced job for the top-level build monitor
Stray I/O, logs, and errors produced by `x` will be wrapped into the job.
-/
def withRegisterJob
- (caption : String) (x : FetchM (Job α))
+ (caption : String) (x : FetchM (Job α)) (optional := false)
: FetchM (Job α) := do
let job ← ensureJob x
- registerJob caption job
+ registerJob caption job optional
/--
Registers the produced job for the top-level build monitor
diff --git a/src/lake/Lake/Build/Job.lean b/src/lake/Lake/Build/Job.lean
index 7418c46175..6c909644b8 100644
--- a/src/lake/Lake/Build/Job.lean
+++ b/src/lake/Lake/Build/Job.lean
@@ -101,33 +101,32 @@ abbrev SpawnM := BuildT BaseIO
@[deprecated SpawnM (since := "2024-05-21")] abbrev SchedulerM := SpawnM
/-- A Lake job. -/
-structure Job (α : Type u) where
- task : JobTask α
- caption : String
+abbrev Job (α : Type u) := JobCore (JobTask α)
+
+structure BundledJobTask where
+ {Result : Type u}
+ task : JobTask Result
deriving Inhabited
-structure BundledJob where
- {type : Type u}
- job : Job type
- deriving Inhabited
+instance : CoeOut (JobTask α) BundledJobTask := ⟨.mk⟩
-instance : CoeOut (Job α) BundledJob := ⟨.mk⟩
+hydrate_opaque_type OpaqueJobTask BundledJobTask
-hydrate_opaque_type OpaqueJob BundledJob
+abbrev OpaqueJob.Result (job : OpaqueJob) : Type :=
+ job.task.get.Result
-abbrev OpaqueJob.type (job : OpaqueJob) : Type :=
- job.get.type
+nonrec abbrev OpaqueJob.task (job : OpaqueJob) : JobTask job.Result :=
+ job.task.get.task
-abbrev OpaqueJob.toJob (job : OpaqueJob) : Job job.type :=
- job.get.job
+abbrev OpaqueJob.ofJob (job : Job α) : OpaqueJob :=
+ {job with task := job.task}
-abbrev OpaqueJob.task (job : OpaqueJob) : JobTask job.type :=
- job.toJob.task
+instance : CoeOut (Job α) OpaqueJob := ⟨.ofJob⟩
-abbrev OpaqueJob.caption (job : OpaqueJob) : String :=
- job.toJob.caption
+abbrev OpaqueJob.toJob (job : OpaqueJob) : Job job.Result :=
+ {job with task := job.task}
-instance : CoeDep OpaqueJob job (Job job.type) := ⟨job.toJob⟩
+instance : CoeDep OpaqueJob job (Job job.Result) := ⟨job.toJob⟩
namespace Job
diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean
index 34bb232dd6..03bdb30895 100644
--- a/src/lake/Lake/Build/Package.lean
+++ b/src/lake/Lake/Build/Package.lean
@@ -24,23 +24,27 @@ def Package.recComputeDeps (self : Package) : FetchM (Array Package) := do
def Package.depsFacetConfig : PackageFacetConfig depsFacet :=
mkFacetConfig Package.recComputeDeps
+/-- Tries to download and unpack the package's prebuilt release archive (from GitHub). -/
+def Package.fetchOptRelease (self : Package) : FetchM (BuildJob Unit) := do
+ (← self.optRelease.fetch).bindSync fun success t => do
+ unless success do
+ logWarning s!"building from source; \
+ failed to fetch cloud release (see '{self.name}:optRelease' for details)"
+ return ((), t)
+
/--
Build the `extraDepTargets` for the package and its transitive dependencies.
Also fetch pre-built releases for the package's' dependencies.
-/
-def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) := do
+def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) :=
+ withRegisterJob s!"{self.name}:extraDep" do
let mut job := BuildJob.nil
-- Build dependencies' extra dep targets
for dep in self.deps do
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 <| ←
- withRegisterJob s!"{self.name}:optRelease" do
- (← self.optRelease.fetch).bindSync fun success t => do
- unless success do
- logWarning "failed to fetch cloud release; falling back to local build"
- return ((), t)
+ job := job.add <| ← self.fetchOptRelease
-- Build this package's extra dep targets
for target in self.extraDepTargets do
job := job.mix <| ← self.fetchTargetJob target
@@ -50,17 +54,19 @@ def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) :=
def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
mkFacetJobConfig Package.recBuildExtraDepTargets
-/-- Download and unpack the package's prebuilt release archive (from GitHub). -/
-def Package.fetchOptRelease (self : Package) : FetchM (BuildJob Bool) := Job.async do
+/-- Tries to download and unpack the package's prebuilt release archive (from GitHub). -/
+def Package.fetchOptReleaseCore (self : Package) : FetchM (BuildJob Bool) :=
+ withRegisterJob s!"{self.name}:optRelease" (optional := true) <| Job.async do
let repo := GitRepo.mk self.dir
let repoUrl? := self.releaseRepo? <|> self.remoteUrl?
let some repoUrl := repoUrl? <|> (← repo.getFilteredRemoteUrl?)
- | logInfo s!"{self.name}: wanted prebuilt release, \
- but repository URL not known; the package may need to set 'releaseRepo'"
+ | logError s!"release repository URL not known; \
+ the package may need to set 'releaseRepo'"
updateAction .fetch
return (false, .nil)
let some tag ← repo.findTag?
- | logInfo s!"{self.name}: wanted prebuilt release, but no tag found for revision"
+ | let rev ← if let some rev ← repo.getHeadRevision? then pure s!" '{rev}'" else pure ""
+ logError s!"no release tag found for revision{rev}"
updateAction .fetch
return (false, .nil)
let url := s!"{repoUrl}/releases/download/{tag}/{self.buildArchive}"
@@ -77,7 +83,7 @@ def Package.fetchOptRelease (self : Package) : FetchM (BuildJob Bool) := Job.asy
/-- The `PackageFacetConfig` for the builtin `optReleaseFacet`. -/
def Package.optReleaseFacetConfig : PackageFacetConfig optReleaseFacet :=
- mkFacetJobConfig (·.fetchOptRelease)
+ mkFacetJobConfig (·.fetchOptReleaseCore)
/-- The `PackageFacetConfig` for the builtin `releaseFacet`. -/
def Package.releaseFacetConfig : PackageFacetConfig releaseFacet :=
@@ -85,20 +91,20 @@ def Package.releaseFacetConfig : PackageFacetConfig releaseFacet :=
withRegisterJob s!"{pkg.name}:release" do
(← pkg.optRelease.fetch).bindSync fun success t => do
unless success do
- error "failed to fetch cloud release"
+ error s!"failed to fetch cloud release (see '{pkg.name}:optRelease' for details)"
return ((), t)
-/-- Perform a build job after first checking for a cloud release for the package. -/
+/-- Perform a build job after first checking for an (optional) cloud release for the package. -/
def Package.afterReleaseAsync (self : Package) (build : SpawnM (Job α)) : FetchM (Job α) := do
if self.preferReleaseBuild ∧ self.name ≠ (← getRootPackage).name then
- (← self.release.fetch).bindAsync fun _ _ => build
+ (← self.optRelease.fetch).bindAsync fun _ _ => build
else
build
-/-- Perform a build after first checking for a cloud release for the package. -/
+/-- Perform a build after first checking for an (optional) cloud release for the package. -/
def Package.afterReleaseSync (self : Package) (build : JobM α) : FetchM (Job α) := do
if self.preferReleaseBuild ∧ self.name ≠ (← getRootPackage).name then
- (← self.release.fetch).bindSync fun _ _ => build
+ (← self.optRelease.fetch).bindSync fun _ _ => build
else
Job.async build
diff --git a/src/lake/Lake/Build/Run.lean b/src/lake/Lake/Build/Run.lean
index f89f721def..2f7e0e63ca 100644
--- a/src/lake/Lake/Build/Run.lean
+++ b/src/lake/Lake/Build/Run.lean
@@ -99,17 +99,18 @@ def renderProgress (running unfinished : Array OpaqueJob) (h : 0 < unfinished.si
def reportJob (job : OpaqueJob) : MonitorM PUnit := do
let {jobNo, ..} ← get
let {totalJobs, failLv, outLv, out, useAnsi, showProgress, minAction, ..} ← read
- let {task, caption} := job.toJob
+ let {task, caption, optional} := job.toJob
let {log, action, ..} := task.get.state
let maxLv := log.maxLv
let failed := log.hasEntries ∧ maxLv ≥ failLv
- if failed then
+ if failed ∧ ¬optional then
modify fun s => {s with failures := s.failures.push caption}
let hasOutput := failed ∨ (log.hasEntries ∧ maxLv ≥ outLv)
if hasOutput ∨ (showProgress ∧ ¬ useAnsi ∧ action ≥ minAction) then
let verb := action.verb failed
let icon := if hasOutput then maxLv.icon else '✔'
- let caption := s!"{icon} [{jobNo}/{totalJobs}] {verb} {caption}"
+ let opt := if optional then " (Optional)" else ""
+ let caption := s!"{icon} [{jobNo}/{totalJobs}]{opt} {verb} {caption}"
let caption :=
if useAnsi then
let color := if hasOutput then maxLv.ansiColor else "32"
@@ -235,7 +236,7 @@ def Workspace.runFetchM
| error "top-level build failed"
return a
else
- print! out "Some builds logged failures:\n"
+ print! out "Some required builds logged failures:\n"
failures.forM (print! out s!"- {·}\n")
flush out
error "build failed"
diff --git a/src/lake/Lake/Util/Git.lean b/src/lake/Lake/Util/Git.lean
index ef8333b0f0..33675b6e2f 100644
--- a/src/lake/Lake/Util/Git.lean
+++ b/src/lake/Lake/Util/Git.lean
@@ -47,9 +47,6 @@ def cwd : GitRepo := ⟨"."⟩
@[inline] def dirExists (repo : GitRepo) : BaseIO Bool :=
repo.dir.isDir
-@[inline] def captureGit (args : Array String) (repo : GitRepo) : LogIO String :=
- captureProc {cmd := "git", args, cwd := repo.dir}
-
@[inline] def captureGit? (args : Array String) (repo : GitRepo) : BaseIO (Option String) :=
captureProc? {cmd := "git", args, cwd := repo.dir}
@@ -66,31 +63,30 @@ def cwd : GitRepo := ⟨"."⟩
repo.execGit #["init", "-q"]
@[inline] def fetch (repo : GitRepo) (remote := Git.defaultRemote) : LogIO PUnit :=
- repo.execGit #["fetch", remote]
+ repo.execGit #["fetch", "--tags", "--force", remote]
@[inline] def checkoutBranch (branch : String) (repo : GitRepo) : LogIO PUnit :=
repo.execGit #["checkout", "-B", branch]
@[inline] def checkoutDetach (hash : String) (repo : GitRepo) : LogIO PUnit :=
- repo.execGit #["checkout", "--detach", hash]
+ repo.execGit #["checkout", "--detach", hash, "--"]
@[inline] def resolveRevision? (rev : String) (repo : GitRepo) : BaseIO (Option String) := do
- repo.captureGit? #["rev-parse", "--verify", rev]
-
-@[inline] def resolveRevision (rev : String) (repo : GitRepo) : LogIO String := do
- repo.captureGit #["rev-parse", "--verify", rev]
-
-@[inline] def getHeadRevision (repo : GitRepo) : LogIO String :=
- repo.resolveRevision "HEAD"
+ repo.captureGit? #["rev-parse", "--verify", "--end-of-options", rev]
@[inline] def getHeadRevision? (repo : GitRepo) : BaseIO (Option String) :=
repo.resolveRevision? "HEAD"
+def getHeadRevision (repo : GitRepo) : LogIO String := do
+ if let some rev ← repo.getHeadRevision? then return rev
+ error s!"{repo}: could not resolve 'HEAD' to a commit; \
+ the repository may be corrupt, so you may need to remove it and try again"
+
def resolveRemoteRevision (rev : String) (remote := Git.defaultRemote) (repo : GitRepo) : LogIO String := do
if Git.isFullObjectName rev then return rev
if let some rev ← repo.resolveRevision? s!"{remote}/{rev}" then return rev
if let some rev ← repo.resolveRevision? rev then return rev
- error s!"cannot find revision {rev} in repository {repo}"
+ error s!"{repo}: revision not found '{rev}'"
def findRemoteRevision (repo : GitRepo) (rev? : Option String := none) (remote := Git.defaultRemote) : LogIO String := do
repo.fetch remote; repo.resolveRemoteRevision (rev?.getD Git.upstreamBranch) remote
diff --git a/src/lake/Lake/Util/MainM.lean b/src/lake/Lake/Util/MainM.lean
index a6345aa1d5..72cb37b602 100644
--- a/src/lake/Lake/Util/MainM.lean
+++ b/src/lake/Lake/Util/MainM.lean
@@ -79,10 +79,9 @@ instance : MonadLift IO MainM := ⟨MonadError.runIO⟩
@[inline] def runLogIO (x : LogIO α)
(minLv := LogLevel.info) (ansiMode := AnsiMode.auto) (out := OutStream.stderr)
: MainM α := do
- let logger ← out.getLogger minLv ansiMode
match (← x {}) with
- | .ok a log => replay log logger; return a
- | .error _ log => replay log logger; exit 1
+ | .ok a log => replay log (← out.getLogger minLv ansiMode); return a
+ | .error _ log => replay log (← out.getLogger .trace ansiMode); exit 1
where
-- avoid specialization of this call at each call site
replay (log : Log) (logger : MonadLog BaseIO) : BaseIO Unit :=
diff --git a/src/lake/tests/noRelease/lakefile.lean b/src/lake/tests/noRelease/lakefile.lean
index 09395425bb..1d8a762897 100644
--- a/src/lake/tests/noRelease/lakefile.lean
+++ b/src/lake/tests/noRelease/lakefile.lean
@@ -2,6 +2,7 @@ import Lake
open Lake DSL
package test
-require dep from "dep"
+
+require dep from git "dep" @ "release"
lean_lib Test
diff --git a/src/lake/tests/noRelease/test.sh b/src/lake/tests/noRelease/test.sh
index 1190a5d380..ccb5aa1bf8 100755
--- a/src/lake/tests/noRelease/test.sh
+++ b/src/lake/tests/noRelease/test.sh
@@ -19,40 +19,51 @@ git config user.name test
git config user.email test@example.com
git add --all
git commit -m "initial commit"
+git tag release
+INIT_REV=`git rev-parse release`
+git commit --allow-empty -m "second commit"
popd
+# Clone dependency
+$LAKE update
+# Remove the release tag from the local copy
+git -C .lake/packages/dep tag -d 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:release
-info: dep: wanted prebuilt release, but no tag found for revision
-error: failed to fetch cloud release
-Some builds logged failures:
+REV_STR="'${INIT_REV}'"
+($LAKE build dep:release && exit 1 || true) | diff -u --strip-trailing-cr <(cat << EOF
+✖ [1/2] (Optional) Fetching dep:optRelease
+error: no release tag found for revision ${REV_STR}
+✖ [2/2] Running dep:release
+error: failed to fetch cloud release (see 'dep:optRelease' for details)
+Some required builds logged failures:
- dep:release
EOF
) -
# Test that an indirect fetch on the release does not cause the build to fail
-$LAKE build Test | diff -u --strip-trailing-cr <(cat << 'EOF'
-⚠ [1/3] Fetched dep:optRelease
-info: dep: wanted prebuilt release, but no tag found for revision
-warning: failed to fetch cloud release; falling back to local build
-✔ [2/3] Built Test
+$LAKE build Test | diff -u --strip-trailing-cr <(cat << EOF
+✖ [1/5] (Optional) Fetching dep:optRelease
+error: no release tag found for revision ${REV_STR}
+⚠ [2/5] Ran dep:extraDep
+warning: building from source; failed to fetch cloud release (see 'dep:optRelease' for details)
+✔ [4/5] Built Test
Build completed successfully.
EOF
) -
# Test download failure
-git -C dep tag release
+$LAKE update # re-fetch release tag
($LAKE build dep:release && exit 1 || true) | grep --color "downloading"
# Test automatic cloud release unpacking
-mkdir -p dep/.lake/build
-$LAKE -d dep pack 2>&1 | grep --color "packing"
-test -f dep/.lake/release.tgz
-echo 4225503363911572621 > dep/.lake/release.tgz.trace
-rmdir dep/.lake/build
+mkdir -p .lake/packages/dep/.lake/build
+$LAKE -d .lake/packages/dep pack 2>&1 | grep --color "packing"
+test -f .lake/packages/dep/.lake/release.tgz
+echo 4225503363911572621 > .lake/packages/dep/.lake/release.tgz.trace
+rmdir .lake/packages/dep/.lake/build
$LAKE build dep:release -v | grep --color "unpacking"
-test -d dep/.lake/build
+test -d .lake/packages/dep/.lake/build
# Test that the job prints nothing if the archive is already fetched and unpacked
$LAKE build dep:release | diff -u --strip-trailing-cr <(cat << 'EOF'
@@ -66,5 +77,15 @@ Build completed successfully.
EOF
) -
+# Test retagging
+git -C dep tag -d release
+git -C dep tag release
+NEW_REV=`git -C dep rev-parse release`
+test ! "$INIT_REV" = "$NEW_REV"
+test `git -C .lake/packages/dep rev-parse HEAD` = "$INIT_REV"
+$LAKE update
+test `git -C .lake/packages/dep rev-parse HEAD` = "$NEW_REV"
+$LAKE build dep:release
+
# Cleanup git repo
rm -rf dep/.git