Zulip Chat Archive

Stream: general

Topic: Azure failures

Anne Baanen (Sep 05 2022 at 11:39):

Anyone else having problems with downloading oleans from Azure? I'm getting:

HTTPSConnectionPool(host='oleanstorage.azureedge.net', port=443): Max retries exceeded with url: /mathlib/44c90247a7438134e994c1d26ba8691e205b02e7.tar.xz (Caused by SSLError(SSLEOFError(8, 'EOF occurred in violation of protocol (_ssl.c:997)')))

Anne Baanen (Sep 05 2022 at 11:41):

After 10 or so retries it now managed to download 63% of the file before disconnecting...

Kevin Buzzard (Sep 05 2022 at 11:42):

I just updated mathlib and tried leanproject get-c and it worked fine for me (it downloaded remote oleans no problem)

Riccardo Brasca (Sep 05 2022 at 11:44):

It just worked for me too.

Anne Baanen (Sep 05 2022 at 11:45):

It finally resolved itself for me too.

Last updated: Dec 20 2023 at 11:08 UTC