lake error on nightly-testing

Stream: nightly-testing

[Kim Morrison]

@Mac Malone, could I have some assistance with this:

% git checkout nightly-testing
Already on 'nightly-testing'
Your branch is up to date with 'nightly-testing/nightly-testing'.
% lake exe cache get
lake stdout:
✔ [0/2] Ran job computation
✖ [1/2] (Optional) Fetching proofwidgets:optRelease
error: target is out-of-date and needs to be rebuilt
✖ [2/2] Running proofwidgets:release
error: failed to fetch GitHub release (see 'proofwidgets:optRelease' for details)
Some required targets logged failures:
- proofwidgets:release
lake stderr:
error: build failed
uncaught exception: Failed to validate ProofWidgets cloud release: lake failed with error code 1

Actionable error messages would be really helpful here! :-)

[Mac Malone]

Unfortunately, this is a bug that it appears I accidentaly introduced in lean4#12086 while fixing another bug.

[Mac Malone]

Do you need the fix tonight? If so, I cna push out a quick untested hotfix. Otherwise, I can do a more testing a merge a change tomorrow.

[Kim Morrison]

NP. I will cancel v4.28.0-rc1 for now. Could you ping me when this is fixed on master?

[Kim Morrison]

Tomorrow is okay.

[Kim Morrison]

Or Monday, of course!

[Mac Malone]

Fixed in lean4#12142.

[Kim Morrison]

Great, thanks, I will turn nightly-2026-01-25 into v4.28.0-rc1 tonight!