leanproject get-cache slow?

Stream: general

[Scott Morrison]

As of a day or two ago, whenever I switch branches and run leanproject get-cache, the step of unzipping the archive has become super slow. It seems quite reproducible, and I'm stumped why it could be happening. It now takes >2 minutes to unzip the archive, and it's making switching branches very painful. Is anyone else seeing this, perchance?

[Eric Wieser]

Is unzipping older archives noticeably faster? Is it possible the regression is in an update to your unzipping tool?

[Scott Morrison]

Hmm, yes, it seems to still happen on older zips. Sadness. Thanks for the diagnostic suggestion, nevertheless.

[Eric Wieser]

I've found the speed to be quite painful on my windows system, so have switched to using gitpod exclusively where it takes only about 5s

[Eric Wieser]

Oh, I now remember that the unzipping tool is just python

[Scott Morrison]

I can reproduce the slow unzipping with xz on the command line, so I'm pretty confused.

[Eric Wieser]

Maybe you have an IO problem of some kind

[Eric Wieser]

Do you have a different hard disk you can put it on and compare with?

[Patrick Massot]

What is clear is that nothing changed on our side recently.

[Bolton Bailey]

I am trying to run leanproject get-c, but it hangs after the following output:

Looking for mathlib oleans for 10902535d1
  locally...
  remotely...

Any reason why it seems to be searching forever for the cache?

[Bolton Bailey]

Is it that a cache isn't created when there's a linter error?

[Mauricio Collares]

"Works" here:

$ leanproject get-c
Looking for mathlib oleans for 10902535d12
  locally...
  remotely...
No cache available for revision 10902535d12
Looking for mathlib oleans for 15c8fddadfb
  locally...
  remotely...
  Found remote mathlib oleans
Looking for mathlib oleans for 5118011fec0
  locally...
  remotely...
  Found remote mathlib oleans
No cache was available for 10902535d12.
There are multiple viable caches from parent commits:
 * 15c8fddadfb
 * 5118011fec0
To see the commits in question, run:
  git log --graph 10902535d12 15c8fddadfb^! 5118011fec0^!
Run `leanproject get-cache --rev` on one of the available commits above.
Failed to fetch cached oleans

[Bolton Bailey]

Unfortunately, even running leanproject get-c --rev origin/master for me results in it hanging

[Mauricio Collares]

Does https://oleanstorage.azureedge.net/mathlib/15c8fddadfb214a58fc40e60b42606bf17f23b87.tar.xz work? What if you add 13.107.246.34 oleanstorage.azureedge.netto /etc/hosts?

[Bolton Bailey]

I can download the link you gave, but I don't know where to put it. Adding that line to /etc/hosts doesn't change the output of leanproject get-c

[Bolton Bailey]

(I'm on Mac M1 if that's relevant)

[Mauricio Collares]

If you want manually apply the cache, you can go to the mathlib project root (the directory that contains archive, test and src subdirs, among others) and extract it with tar xvf /your/download/dir/15c8fddadfb214a58fc40e60b42606bf17f23b87.tar.xz.

[Mauricio Collares]

The reason I suggested the /etc/hosts change was because I sometimes see IPv6 causing hangs on some providers

[Bolton Bailey]

This works, thanks Mauricio for unblocking me. Still, it's a bit concerning that leanproject stopped working for some reason.