refactor: separate proof/spec files into a dedicated LckSpec lake target
Nadie ha tomado este issue todavía.
Evaluación
- Dificultad
- 4/5
- Tiempo estimado
- 3-5 días
- Aptitud para principiantes
- 48/100
- Tipo de issue
- Refactorización
- Claridad
- Bastante claro
- Estado de actividad
- Estancado
- Área
- build-system, compilers
Línea de trabajo
Inspecciona la definición actual del objetivo de Lake y los archivos spec/proof enumerados, incluidos RegexSpec.lean, DesugarSpec.lean y ParserSpec.lean. Confirma qué archivos se incluyen en el objetivo principal Lck y sepáralos en un objetivo LckSpec compilado explícitamente, manteniendo el código relevante para el tiempo de ejecución en Lck. Se considera completado cuando las compilaciones posteriores de Lck ya no compilan la infraestructura de proof, mientras que LckSpec sigue disponible para la verificación o CI.
Escrito por el modelo de indexación a partir del texto del issue.
Descripción
Problem
Spec and proof files (RegexSpec.lean, DesugarSpec.lean, ParserSpec.lean, etc.) are included in the main Lck library target. This means every downstream user of the library also compiles the proof infrastructure, which is heavyweight (imports Mathlib, long compile times).
Expected fix
Move spec/proof files into a separate LckSpec Lake target (or library) that is only built when explicitly requested (e.g., for verification or CI). The main Lck target should contain only the runtime-relevant code.
References
- Suggested by AI code review on PR #9
- Lenguaje dominante
- Lean
- Estrellas
- 2
- Forks
- 1
- Métricas de merge de PR
- Sin PR fusionados en 30 d
Guía de contribución
No hay ninguna guía de contribución indexada para este repositorio
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 lambdaclass/lambda_compiler_kit
-
Dificultad 1/5 Menos de una hora Aptitud para principiantes 72/100
-
Dificultad 1/5 Menos de una hora Aptitud para principiantes 68/100
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 68/100
-
enhancement
Dificultad 4/5 3-5 días Aptitud para principiantes 48/100
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 50/100
Todos los issues de lambdaclass/lambda_compiler_kit
Issues similares
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 75/100
freedomofpress/dangerzone#1562 ·
-
Mend: dependency security vulnerability status: needs triage 🕵️♀️
Dificultad 2/5 1-3 horas Aptitud para principiantes 70/100
carbon-design-system/ibm-products#9907 ·
-
intake mcp-intake needs-ac needs-human-review priority:medium type:feature
Dificultad 2/5 1-3 horas Aptitud para principiantes 75/100
Ikalus1988/MisakaNet#2102 · 2 comentarios ·
-
onnx-ir re-exports ModelProto and GraphProto but not NodeProto, AttributeProto and AttributeType Abierto
Dificultad 2/5 1-3 horas Aptitud para principiantes 75/100
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 65/100
llvm/lighthouse#283 ·