leanprover/lean4

Lake fetches caches for unbuilt dependencies

Closed this issue · 0 comments

Description

Lake builds the package-level extraDep target for package and its dependencies even if no target in one of those dependencies is built. As a result, Lake will attempt to fetch the cache for such dependencies even though no build artifacts from those packages are used (or would be built without the cache). Since Lake will re-attempt to fetch the cache as long as the build directory for a package is missing, the lack of a local build on a fetch failure will cause Lake to re-attempt indefinitely. This breaks --no-build in this situation.

Context

Reported on Zulip (diagnosed at this point in the thread).

Versions

v4.13.0-rc1/v4.13.0-rc3

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.