Default Behavior for Lemma File and Module Import in Kontrol
Nadie ha tomado este issue todavía.
Evaluación
- Dificultad
- 5/5
- Tiempo estimado
- Más de una semana
- Aptitud para principiantes
- 35/100
- Tipo de issue
- Nueva funcionalidad
- Claridad
- Bastante claro
- Estado de actividad
- Estancado
- Área
- cli
Línea de trabajo
Comienza con el comando de compilación kontrol build e inspecciona cómo se gestionan actualmente --require y --module-import. Usa el archivo propuesto project-lemmas.k y el comportamiento del módulo PROJECT-LEMMAS como criterios de aceptación: los valores predeterminados deberían funcionar sin repetir los flags, el archivo debería crearse cuando no exista y los módulos faltantes deberían producir una advertencia o un error.
Escrito por el modelo de indexación a partir del texto del issue.
Descripción
I propose a default setting enhancement for lemma files and module imports for the kontrol build command.
Current Requirement:
If a user wants to include project-specific lemmas, he must explicitly specify the lemmas file and module import on each build, like so:
kontrol build --require lemmas.k --module-import CronTwoTest:CRON-TWO-LEMMAS
Proposed Default Behavior:
The new behavior turns this configuration into a convention:
- We let
--requiredefault toproject-lemmas.k. - We let
--module-importdefault toPROJECT-LEMMAS. - We auto-create
project-lemmas.kwith an emptyPROJECT-LEMMASmodule if not present. (Maybe we could even add a simple lemma here, so users have a template to start from). - We emit a warning/error if
PROJECT-LEMMASmodule is missing (e.g. because a user deleted it).
This simplifies the process, benefiting users by reducing repetitive command-line specifications.
- Lenguaje dominante
- KCL
- Estrellas
- 592
- Forks
- 156
- Merge medio
- 2 h 19 min
- PR fusionados (30 d)
- 1
Preparar el entorno
Aún no hemos revisado los archivos de configuración de este proyecto. Empieza por su README y consulta nuestra guía para la primera contribución para los pasos generales.
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 runtimeverification/evm-semantics
-
Dificultad 1/5 Menos de una hora Aptitud para principiantes 78/100
runtimeverification/evm-semantics#1190 ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 45/100
runtimeverification/evm-semantics#2879 ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 35/100
runtimeverification/evm-semantics#2869 ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 35/100
runtimeverification/evm-semantics#2832 ·
-
Dificultad 4/5 3-5 días Aptitud para principiantes 30/100
runtimeverification/evm-semantics#2824 ·
Todos los issues de runtimeverification/evm-semantics
Issues similares
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 84/100
beehive-lab/TornadoVM#1151 ·
Los mantenedores suelen responder en 1 día
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 75/100
Los mantenedores suelen responder en 5 días
-
Failed to resolve logo sourceAbiertobug
Dificultad 2/5 1-3 horas Aptitud para principiantes 68/100
fastfetch-cli/fastfetch#2628 ·
Los mantenedores suelen responder en 1 día
-
bug os:Windows
Dificultad 2/5 1-3 horas Aptitud para principiantes 88/100
Los mantenedores suelen responder en 1 día
-
state:triage-needed
Dificultad 2/5 1-3 horas Aptitud para principiantes 72/100
Los mantenedores suelen responder en 1 día