failed to fetch cached oleans

Stream: general

[Kevin Buzzard]

I was going to take a look at #5345 but then this happened:

buzzard@bob:~/lean-projects/mathlib$ git pull
Already up-to-date.
buzzard@bob:~/lean-projects/mathlib$ git status
On branch alg_hom_tower
Your branch is up-to-date with 'origin/alg_hom_tower'.

nothing to commit, working tree clean
buzzard@bob:~/lean-projects/mathlib$ leanproject get-cache
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/24fcd6155cc6cddf911d58b081fb308d0d588f15.tar.xz to /home/buzzard/.mathlib/24fcd6155cc6cddf911d58b081fb308d0d588f15.tar.xz
Failed to fetch cached oleans
buzzard@bob:~/lean-projects/mathlib$

The commit seems to have a green tick according to https://github.com/leanprover-community/mathlib/pull/5345 . What am I doing wrong?

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/runs/1562126842 says "This check was skipped"

[Gabriel Ebner]

That's just the label action. If you click on the CI action, you get this wonderful error:

Please verify your email address to run GitHub Actions workflows. https://github.com/settings/emails

[Eric Wieser]

I think that means tb65536 needs to verify their email

[Gabriel Ebner]

That's an unexpected requirement for a CI service.

[Eric Wieser]

@Thomas Browning

[Eric Wieser]

Probably a first line of defense to avoid using github's CI machines for a DoS attack against something else

[Kevin Buzzard]

(deleted)

[Bryan Gin-ge Chen]

It should be possible for other users with mathlib write permissions to re-run the jobs via the "Re-run jobs" button. I haven't done so in case Thomas wants to re-run them.

[Kevin Buzzard]

in the mean time I just got the oleans from where the branch came off master and it worked fine

[Thomas Browning]

Hopefully my email address should be verified now