To mirror Lean4 the task is split into:
- The Elan installer itself and its init scripts
- The Lean4 toolchains binary
- The Mathlib4 library and its recursive dependencies
- The Mathlib4 web docs
- The Mathlib4 cache
The Elan installer itself and its init scripts
init scripts: elan-init.sh, elan-init.ps1
The mirror can change variable ELAN_UPDATE_ROOT or ElanRoot to the mirrored one. The request URL structure is exactly what GitHub release like.
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)
The Mathlib4 library and its recursive dependencies
It would be better to direct require from tuna mirror. There should have some recursive modification automatically.
The Mathlib4 web docs
See https://github.com/leanprover-community/mathlib4#building-html-documentation
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
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...
To mirror Lean4 the task is split into:
The Elan installer itself and its init scripts
init scripts: elan-init.sh, elan-init.ps1
The mirror can change variable
ELAN_UPDATE_ROOTorElanRootto the mirrored one. The request URL structure is exactly what GitHub release like.The Lean4 toolchains binary
In the Elan repo,
src/elan-dist/src/manifestation.rsandsrc/elan-dist/src/dist.rsshould take config custom URL like whatrustuphad done. (Seesrc/config.rs)elanread env varsThe Mathlib4 library and its recursive dependencies
It would be better to direct
requirefrom tuna mirror. There should have some recursive modification automatically.The Mathlib4 web docs
See https://github.com/leanprover-community/mathlib4#building-html-documentation
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
cacheread env varI 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...