Hacktoberfest 2026: los issues que los mantenedores marcaron para octubre, abiertos y aptos para principiantes. Explorar issues de Hacktoberfest

perf/safety: convert parseStr from recursive to iterative to prevent stack overflow

Abierto
#21 0 comentarios 0 reacciones 0 asignados Ver en GitHub

Nadie ha tomado este issue todavía.

Evaluación

Dificultad
4/5
Tiempo estimado
3-5 días
Aptitud para principiantes
45/100
Tipo de issue
Refactorización
Claridad
Bien especificado
Estado de actividad
Estancado
Área
compilers, performance

Línea de trabajo

Comienza en Lck/Json/Tokenizer.lean, en la implementación CPS recursiva de parseStr, y luego inspecciona cómo dependen los llamadores de su interfaz CPS. Reescribe el análisis de cadenas como un acumulador iterativo conservando esa interfaz, adapta la demostración en torno a un invariante inductivo del bucle y verifica que los literales de cadena grandes ya no corren el riesgo de provocar un desbordamiento de pila.

Escrito por el modelo de indexación a partir del texto del issue.

Descripción

Problem

parseStr in Lck/Json/Tokenizer.lean is written as a recursive CPS function. While the continuation wrapping is proven zero-cost at runtime (proofs are erased), the recursion itself is structural on the input — meaning for a string literal of length n, the Lean runtime creates n stack frames.

For pathologically large string values this can overflow the stack.

Expected fix

Rewrite parseStr as an iterative (tail-recursive or explicit loop) accumulator, maintaining the same CPS interface for callers. The proof structure can be adapted to use an inductive invariant on the loop state.

References

  • Flagged by AI code review on PR #8
Lenguaje dominante
Lean
Estrellas
2
Forks
1
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

  1. Lee el issue completo y luego la guía de contribución del proyecto.
  2. Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
  3. Haz un fork del repositorio y trabaja en una rama.
  4. Abre un pull request que haga referencia al número del issue.

Más de lambdaclass/lambda_compiler_kit

Todos los issues de lambdaclass/lambda_compiler_kit

Issues similares

Más issues de Compilers

Recibe los nuevos issues en tu correo

Un resumen breve de issues de GitHub para principiantes.