oleans not downloading

Stream: general

[Anne Baanen]

I'm trying to use leanproject to download oleans for branch#ericrbg/poly_diamond_int, but it just gets stuck on the "remotely..." line for over a minute. Anyone else having trouble getting oleans?

[Kevin Buzzard]

It's working fine for me on that branch

[Kevin Buzzard]

$ git checkout ericrbg/poly_diamond_int
Branch 'ericrbg/poly_diamond_int' set up to track remote branch 'ericrbg/poly_diamond_int' from 'origin'.
Switched to a new branch 'ericrbg/poly_diamond_int'
buzzard@bob:~/active-lean-projects/mathlib$ git pull
Already up-to-date.
buzzard@bob:~/active-lean-projects/mathlib$ leanproject get-c
Looking for mathlib oleans for a3ad7f49a7
  locally...
  remotely...
  Found remote mathlib oleans
Using matching cache
  a3ad7f49a7: 100%|████████████████████████████████████████████████████████████████████| 74.0M/74.0M [00:13<00:00, 5.67MB/s]
Applying cache
  files extracted: 2599 [00:06, 431.81/s]
buzzard@bob:~/active-lean-projects/mathlib$

[Anne Baanen]

Okay, the problem is probably on my end then.

[Anne Baanen]

Indeed, when doing a full system upgrade half of the downloads seem to be stuck too...