Request and RFC for add Lean4 mirrors
Nadie ha tomado este issue todavía.
Evaluación
- Dificultad
- 5/5
- Tiempo estimado
- Más de una semana
- Aptitud para principiantes
- 20/100
- Tipo de issue
- Nueva funcionalidad
- Claridad
- Necesita aclaración
- Estado de actividad
- Estancado
- Área
- build-system, cloud, devops, infrastructure
Línea de trabajo
Comienza con elan-init.sh, elan-init.ps1 y los archivos Rust de Elan manifestation.rs, dist.rs y config.rs para entender la configuración de mirrors solicitada. Después, revisa Mathlib4's Cache/Requests.lean y la documentación enlazada de la biblioteca, la documentación web y la caché. Se considerará terminado cuando las cinco áreas de mirrors enumeradas y sus cambios de configuración estén implementados y sean verificables.
Escrito por el modelo de indexación a partir del texto del issue.
Descripción
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
- 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
elanread 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.
- make Mathlib4
cacheread 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...
- Lenguaje dominante
- Python
- Estrellas
- 496
- Forks
- 179
- Merge medio
- 2 min
- PR fusionados (30 d)
- 1
Preparar el entorno
- Incluye un Dockerfile o un archivo de Docker Compose
- Sin plantilla de pull request
- Sin guía de contribución
Primeros pasos
- Lee el issue completo y luego la guía de contribución del proyecto.
- Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
- Haz un fork del repositorio y trabaja en una rama.
- Abre un pull request que haga referencia al número del issue.
Más de tuna/tunasync-scripts
-
Dificultad 4/5 3-5 días Aptitud para principiantes 55/100
tuna/tunasync-scripts#207 ·
-
git-recursive脚本同步git仓库时，工作不正常Posiblemente ocupada @marvil6 la tomó hace 26 días. Abierto
Dificultad 3/5 1-2 días Aptitud para principiantes 35/100
tuna/tunasync-scripts#161 · 5 comentarios ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 35/100
tuna/tunasync-scripts#122 ·
-
S3 sync missing filesAbierto
Dificultad 3/5 1-2 días Aptitud para principiantes 30/100
tuna/tunasync-scripts#88 · 3 comentarios ·
Todos los issues de tuna/tunasync-scripts
Issues similares
-
Project submission:Abierto
Dificultad 1/5 Menos de una hora Aptitud para principiantes 72/100
slavakurilyak/awesome-ai-agents#845 ·
Los mantenedores suelen responder en 1 día
-
tests: pin that the atomic writers in utils/paths.py stage the temporary file in the target's directoryPosiblemente ocupada Un pull request vinculado a esta issue está abierto o ya se fusionó. Abiertodifficulty:2 enhancement good first issue
Dificultad 1/5 1-3 horas Aptitud para principiantes 92/100
MakazhanAlpamys/Soup#2178 ·
Los mantenedores suelen responder en 1 día
-
[BUG] dcg.waggr permutation p-values are folded twice, so near-zero scores get the smallest p-valuesAbierto
Dificultad 2/5 1-3 horas Aptitud para principiantes 75/100
scverse/rapids-singlecell#854 ·
Los mantenedores suelen responder en 1 día
-
Slang input: int8_t4_packed and uint8_t4_packed are copied into CrossGLPosiblemente ocupada @ninglinLiu la tomó hoy. Abiertoarea:frontend backend:slang bug direction:input
Dificultad 2/5 1-3 horas Aptitud para principiantes 70/100
Los mantenedores suelen responder en 1 día
-
random_elements(unique=True) on an OrderedDict: ZeroDivisionError once only zero weights remain, AssertionError with use_weighting=FalsePosiblemente ocupada Un pull request vinculado a esta issue está abierto o ya se fusionó. Abierto
Dificultad 2/5 1-3 horas Aptitud para principiantes 85/100
Los mantenedores suelen responder en 13 días