Default Behavior for Lemma File and Module Import in Kontrol
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 5/5
- Tempo stimato
- Più di una settimana
- Idoneità per principianti
- 35/100
- Tipo di issue
- Funzionalità
- Chiarezza
- Abbastanza chiara
- Stato di attività
- Ferma
- Ambito
- cli
Direzione di ricerca
Inizia dal comando di build kontrol build e verifica come vengono gestiti attualmente --require e --module-import. Usa il file proposto project-lemmas.k e il comportamento del modulo PROJECT-LEMMAS come criteri di accettazione: i valori predefiniti dovrebbero funzionare senza flag ripetuti, il file dovrebbe essere creato quando è assente e i moduli mancanti dovrebbero produrre un avviso o un errore.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
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.
- Lingua principale
- KCL
- Stelle
- 594
- Fork
- 157
- Merge medio
- 2h 19m
- PR unite (30g)
- 1
Preparare l'ambiente
Questo progetto non fornisce container di sviluppo, Dockerfile né guida per i contributori, quindi l'ambiente è a tuo carico: parti dal suo README e consulta la nostra guida al primo contributo per i passaggi generali.
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di runtimeverification/evm-semantics
-
Difficoltà 1/5 Meno di un'ora Idoneità per principianti 78/100
runtimeverification/evm-semantics#1190 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100
runtimeverification/evm-semantics#2879 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100
runtimeverification/evm-semantics#2869 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100
runtimeverification/evm-semantics#2832 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 30/100
runtimeverification/evm-semantics#2824 ·
Tutte le issue di runtimeverification/evm-semantics
Issue simili
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 84/100
mvanhorn/printing-press-library#2120 ·
I maintainer di solito rispondono entro 1 giorno
-
touch: "setting times of" instead of "cannot touch" for an existing file the user cannot writeAperta
Difficoltà 2/5 1-3 ore Idoneità per principianti 75/100
I maintainer di solito rispondono entro 1 giorno
-
bug
Difficoltà 2/5 1-3 ore Idoneità per principianti 88/100
pyrite-wiki/pyrite#574 ·
I maintainer di solito rispondono entro 1 giorno
-
category/ui priority/P3 scope/keybindings scope/web-shell type/feature-request
Difficoltà 2/5 1-3 ore Idoneità per principianti 84/100
QwenLM/qwen-code#13175 · 3 commenti ·
I maintainer di solito rispondono entro 1 giorno