Request approve for Elan CI

Stream: general

[Alissa Tung]

In this merge request https://github.com/leanprover/elan/pull/103, I had purposed some changes on resource URLs and environment variables. If those changes are acceptable, I hope someone can approve it so that the CI can do some checks. We are going to build mirrors for the Lean4 ecosystem, advices on this topic are welcome!

[Sebastian Ullrich]

Could you say a bit more about the use case?

[Alissa Tung]

The motivation is that in some areas, people must use proxy to access GitHub releases. We are going to provide a service which allowed user to download {init script, elan itself and updates, lean toolchains} from any custom mirror site. We already had some progress at https://mirror.sjtu.edu.cn, which has mirrors for Lean and Elan binaries and most package repo we need.

[Alissa Tung]

The implementation details is not decided yet. Let me have some tests on this and write some explanations.

[Alissa Tung]

I can not working on this recently, and I have developed a tool glean which is a workaround to those problems...