Request and RFC for add Lean4 mirrors

To mirror Lean4 the task is split into:

1. The Elan installer itself and its init scripts
2. The Lean4 toolchains binary
3. The Mathlib4 library and its recursive dependencies
4. The Mathlib4 web docs
5. The Mathlib4 cache

The Elan installer itself and its init scripts

init scripts: elan-init.sh, elan-init.ps1

• mirror init scripts

The mirror can change variable ELAN_UPDATE_ROOT or ElanRoot to the mirrored one. The request URL structure is exactly what GitHub release like.

• mirror Elan binary releases

The Lean4 toolchains binary

In the Elan repo, src/elan-dist/src/manifestation.rs and src/elan-dist/src/dist.rs should take config custom URL like what rustup had done. (See src/config.rs)

• make elan read env vars
• mirror Lean4 binary releases

The Mathlib4 library and its recursive dependencies

It would be better to direct require from tuna mirror. There should have some recursive modification automatically.

• mirror Mathlib4 library and its recursive dependencies git repo

The Mathlib4 web docs

See https://github.com/leanprover-community/mathlib4#building-html-documentation

• mirror the web docs

The Mathlib4 cache

The Mathlib4 cache is stored in Azure blob storage. It can be replace by an Azure compatible server.

See https://github.com/leanprover-community/mathlib4/blob/0469f845e132ccd0e56c40aafd34bd9084c104bb/Cache/Requests.lean#L14

• make Mathlib4 cache read env var
• set up Azure compatible server
• mirror Mathlib4 cache

---

I have draft some checkboxes above to make a initial plan for mirror Lean4 ecosystem. If Tuna is willing for mirroring the Lean4 ecosystem which would be a great help!

It would be better if there is some people more familiar with Tuna mirror system. If someone is not available to approach them I can do most of above job, once I learned how to debug and test the Tuna mirror system. I have basic skill for Lean4 and general programming and I think I can do the programming task at both side, Tuna and the Lean4 ecosystem...

Start with elan-init.sh, elan-init.ps1, and the Elan Rust files manifestation.rs, dist.rs, and config.rs to understand the requested mirror configuration. Then review Mathlib4's Cache/Requests.lean and the linked documentation for the library, web docs, and cache. Done means the five listed mirror areas and their configuration changes are implemented and verifiable.