Discussion of `glean`

Stream: general

[Junyan Xu]

Does it mirror oleans? Not sure how fast currently it is to download oleans in China. I think Azure does operate in China, though the current server seems to be located at lakecache.blob.core.windows.net rather than mathlib3's https://oleanstorage.azureedge.net/mathlib/.

[Alissa Tung]

@Junyan Xu No, we have not complete the work of cache library build artifacts yet. My plan is to use a S3 compatible storage server, and rewrite the Mathlib4 cache and other cloud-releases.

[Alissa Tung]

Junyan Xu 发言道：

Does it mirror oleans? Not sure how fast currently it is to download oleans in China. I think Azure does operate in China, though the current server seems to be located at lakecache.blob.core.windows.net rather than mathlib3's https://oleanstorage.azureedge.net/mathlib/.

The cache from azure is unusable in China, we can not access those sites directly. And since Mathlib4 just drop out the retry support of downloading files, the cache functionality is totally unusable even under a proxy.

[Notification Bot]

3 messages were moved here from #announce > Release of glean: all-in-one tool for Lean mirror by Johan Commelin.