Style lint job fails

Stream: mathlib4

[Michael Rothgang]

Over at #23909, the lint-style job fails now --- both for CI-related reasons. (The error message says lake not found; that PR doesn't touch any .yml files.) CC @Anne Baanen since you modified that job recently.

[Michael Stoll]

Compare #mathlib4 > Is there a problem with Lake at the moment? @ 💬

[Anne Baanen]

This seems to be curl failing in lean-action but not actually causing the workflow to fail:

curl: (22) The requested URL returned error: 404

elan: command failed: curl -sSfL https://github.com/leanprover/elan/releases/latest/download/elan-x86_64-unknown-linux-gnu.tar.gz

/home/runner/work/_actions/leanprover/lean-action/f807b338d95de7813c5c50d018f1c23c9b93b4ec/scripts/install_elan.sh: line 12: /home/runner/.elan/bin/lean: No such file or directory

/home/runner/work/_actions/leanprover/lean-action/f807b338d95de7813c5c50d018f1c23c9b93b4ec/scripts/install_elan.sh: line 13: /home/runner/.elan/bin/lake: No such file or directory

[Anne Baanen]

(Shall we merge the two threads?)

[Anne Baanen]

The CI issue seems to be related to having a new Lake release that is only compiled for Apple: https://github.com/leanprover/elan/releases/tag/v4.1.2

[Michael Rothgang]

The other thread has two issues, IIUC - let's use this for the style-lint issue?

[Yaël Dillies]

Same over at #24149

[Michael Rothgang]

So all "important" mathlib CI jobs are borked right now, correct? Wow, that's bad.

[Michael Rothgang]

CC @Sebastian Ullrich since you just released a new elan version

[Damiano Testa]

It looks like lake build is still running, but all PRs will fail CI anyway.

[Michael Rothgang]

Does the cache generation and upload still work?

[Damiano Testa]

I don't know, the PR that I am running through CI right now needs to rebuild all of mathlib.

[Anne Baanen]

So as far as I can tell, what seems to have happened is the ongoing GitHub issues caused the Elan release to fail for all but one build, and that build ended up creating the release anyway.

[Damiano Testa]

I have been able to download the cache for #25203, so I think that the "Build" CI is working correctly.

[Robin Carlier]

in #24809 (which I updated recently) the cache generation upload worked correctly (despite the lint-style failure)

[Anne Baanen]

So now everyone trying to install the latest Elan on Linux or Windows is going to run into errors. I assume the Hoskinson runners still have Elan in their cache so they are still up.

[Anne Baanen]

One solution is to rerun the build jobs until the ongoing GitHub issues let them through by random chance...

[Robin Carlier]

Elan linux builds were released a few minutes ago, and lint-style seems to work now.