Still show last compiled goal-state while `Processing file...`
Evaluación
- Dificultad
- 4/5
- Tiempo estimado
- 3-5 días
- Aptitud para principiantes
- 40/100
- Tipo de issue
- Nueva funcionalidad
- Claridad
- Bastante claro
- Estado de actividad
- Estancado
- Stack tecnológico
- lua, neovim
- Área
- developer-experience, tooling
Línea de trabajo
El issue no nombra archivos, pruebas ni puntos de entrada. Empieza rastreando cómo lean.nvim muestra el estado actual del objetivo mientras se procesa un archivo; determina si el estado compilado anteriormente puede permanecer visible con un indicador Processing file..., y verifica el comportamiento durante la edición de pruebas y la recompilación.
Escrito por el modelo de indexación a partir del texto del issue.
Descripción
When I'm writing a proof, I would love to be able to have a consistent point of reference of existing hypothesis in the scope. Currently on every justification step I have to stop, wait for the file to process, and then in 90% of cases look for a hypothesis that was already available to find its name and exact statement.
It would be so much faster to have an option (or have it be default) of seeing the previously compiled state with a small indicator of Processing file... at the bottom or to the side, which would allow to write proofs without needless interrupts.
- Lenguaje dominante
- Lua
- Estrellas
- 607
- Forks
- 63
- Merge medio
- 1 d 8 h
- PR fusionados (30 d)
- 8
Preparar el entorno
- Sin Dockerfile ni archivo de Docker Compose
- Sin plantilla de pull request
- Leer la 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 Julian/lean.nvim
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 70/100
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 88/100
-
Dificultad 3/5 1-2 días Aptitud para principiantes 56/100
-
Dificultad 4/5 3-5 días Aptitud para principiantes 48/100
-
Dificultad 3/5 1-2 días Aptitud para principiantes 58/100
Todos los issues de Julian/lean.nvim
Issues similares
-
P2: A timed rotation maneuver does nothing on a ship that had an earlier timed lateral maneuverAbierto
Dificultad 2/5 1-3 horas Aptitud para principiantes 78/100
scp-fs2open/fs2open.github.com#7914 ·
Los mantenedores suelen responder en 1 día
-
severity: low
Dificultad 1/5 1-3 horas Aptitud para principiantes 89/100
luainkernel/lunatik#1980 ·
Los mantenedores suelen responder en 1 día
-
LSP: inline_completion logs ServerCancelled as an errorPosiblemente ocupada @dobsontom la tomó hoy. Abiertolsp
Dificultad 2/5 1-3 horas Aptitud para principiantes 72/100
Los mantenedores suelen responder en 1 día
-
bug
Dificultad 2/5 1-3 horas Aptitud para principiantes 62/100
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 76/100