Zulip Chat Archive

Stream: general

Topic: failed to fetch cached oleans


view this post on Zulip Kevin Buzzard (Dec 16 2020 at 16:45):

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?

view this post on Zulip Kevin Buzzard (Dec 16 2020 at 16:47):

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

view this post on Zulip Gabriel Ebner (Dec 16 2020 at 16:49):

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

view this post on Zulip Eric Wieser (Dec 16 2020 at 16:51):

I think that means tb65536 needs to verify their email

view this post on Zulip Gabriel Ebner (Dec 16 2020 at 16:53):

That's an unexpected requirement for a CI service.

view this post on Zulip Eric Wieser (Dec 16 2020 at 16:53):

@Thomas Browning

view this post on Zulip Eric Wieser (Dec 16 2020 at 16:53):

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

view this post on Zulip Kevin Buzzard (Dec 16 2020 at 16:54):

(deleted)

view this post on Zulip Bryan Gin-ge Chen (Dec 16 2020 at 17:25):

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.

view this post on Zulip Kevin Buzzard (Dec 16 2020 at 17:30):

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

view this post on Zulip Thomas Browning (Dec 16 2020 at 18:39):

Hopefully my email address should be verified now


Last updated: May 14 2021 at 22:15 UTC