The lean-toolchain file contains master. elan has no master release channel, so a fresh elan/lake setup fails with:
error: no such release: 'master'
This blocks CI — with the workflow placed correctly (#8 / #9), the job runs but fails at the Elan install step with exactly that error — and also any clean checkout that does not already have a locally linked toolchain named master.
Suggested fix: pin to an elan-resolvable channel. leanprover/lean4:nightly keeps the "track latest Lean" intent; a concrete leanprover/lean4:nightly-YYYY-MM-DD or a stable leanprover/lean4:vX.Y.Z are alternatives if reproducible CI is preferred.
The
lean-toolchainfile containsmaster. elan has nomasterrelease channel, so a fresh elan/lake setup fails with:This blocks CI — with the workflow placed correctly (#8 / #9), the job runs but fails at the Elan install step with exactly that error — and also any clean checkout that does not already have a locally linked toolchain named
master.Suggested fix: pin to an elan-resolvable channel.
leanprover/lean4:nightlykeeps the "track latest Lean" intent; a concreteleanprover/lean4:nightly-YYYY-MM-DDor a stableleanprover/lean4:vX.Y.Zare alternatives if reproducible CI is preferred.