Zulip Chat Archive

Stream: general

Topic: oleans not downloading

Anne Baanen (Aug 01 2022 at 08:59):

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 (Aug 01 2022 at 09:01):

It's working fine for me on that branch

Kevin Buzzard (Aug 01 2022 at 09:02):

$ 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
  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]

Anne Baanen (Aug 01 2022 at 09:03):

Okay, the problem is probably on my end then.

Anne Baanen (Aug 01 2022 at 09:08):

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

Last updated: Aug 03 2023 at 10:10 UTC