CLI fails silently on v4.30.0+ when using module system
Nadie ha tomado este issue todavía.
Evaluación
- Dificultad
- 3/5
- Tiempo estimado
- 1-2 días
- Aptitud para principiantes
- 52/100
Línea de trabajo
Comienza con el repositorio MWE enlazado de dos commits y compara su comportamiento con v4.29.1 y v4.30.0, centrándote en Main.lean y su declaración de módulo. Sigue cómo lean4-cli descubre e invoca el punto de entrada main meta público. La tarea estará terminada cuando un Main.lean basado en módulos se ejecute normalmente en lugar de convertirse silenciosamente en un no-op, mientras el caso existente de archivo simple siga funcionando.
Escrito por el modelo de indexación a partir del texto del issue.
Descripción
Up to v4.29.1, it was possible to use the module system for the entry point of an executabl (Main.lean in the template lake projects). In v4.30.0 this will cause lean4-cli to fail silently resulting in a no-op when the executable is called.
Reproduction
I've created an MWE-repo with 2 commits, one working in v4.29.1 and one failing in v4.30.0:
https://github.com/joneugster/lean-cli-bug-demo/commits/main/
The key is that Main.lean contains
module
...
public meta def main (args : List String) : IO UInt32 :=
i18n.validate args
If module is removed from Main.lean turning it into a plain Lean file, it works again.
- Lenguaje dominante
- Lean
- Estrellas
- 120
- Forks
- 30
- Merge medio
- 5 min
- PR fusionados (30 d)
- 4
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 leanprover/lean4-cli
-
enhancement
Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100
leanprover/lean4-cli#2 ·
Todos los issues de leanprover/lean4-cli
Issues similares
-
[Bug] reef-hermes tells me to resume with hermes --resume, which does not work from my shell Abiertoarea: harness bug status: needs-triage
Dificultad 2/5 1-3 horas Aptitud para principiantes 75/100
Human-Agent-Society/reef#625 ·
-
module: core
Dificultad 2/5 1-3 horas Aptitud para principiantes 75/100
bigbluebutton/bigbluebutton#25849 ·
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 75/100
vercel-labs/just-bash#464 ·
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 75/100
-
area:sandbox documentation enhancement platform:linux
Dificultad 1/5 Menos de una hora Aptitud para principiantes 85/100
anthropics/claude-code#96664 ·