Issues running kclaim style proofs
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 5/5
- Tempo stimato
- Più di una settimana
- Idoneità per principianti
- 20/100
- Tipo di issue
- Bug
- Chiarezza
- Da chiarire
- Stato di attività
- Ferma
- Ambito
- tooling
Direzione di ricerca
Inizia tracciando la gestione di --save-directory e --reinit, poi esamina come vengono accodate le dipendenze delle dimostrazioni e i batch paralleli. Il lavoro è completato quando le affermazioni o le dipendenze modificate vengono invalidate, le dimostrazioni idonee vengono accodate senza attese non necessarie dei batch e le dimostrazioni con dipendenze non scaricabili seguono la regola di ammissione indicata.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
- Re-executing a KClaim (with
--save-directory) where a proof changes or a dependency changes, does not trigger--reinitbehavior. We should be parsing the claims, and invalidating any claims where the claim itself or a dependency has changed. - Parallel proof discharge waits for each batch of proofs instead of adding to the queue of tasks asynchronously. This means that if there a few really long running proofs in one layer of proofs, we won't move on to the proofs in the next layer who's dependencies are already discharged.
- Proofs whos dependencies are not discharged should not be run unless the dependency is admitted or the user specifies to admit dependencies. Perhaps?
- Lingua principale
- KCL
- Stelle
- 592
- Fork
- 156
- Merge medio
- 2h 19m
- PR unite (30g)
- 1
Preparare l'ambiente
Non abbiamo ancora controllato i file di configurazione di questo progetto. 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
-
Marble Madness II is missingAperta
Difficoltà 2/5 1-3 ore Idoneità per principianti 68/100
-
[Request]: Snow ShotAperta
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
ScoopInstaller/Extras#18870 ·
I maintainer di solito rispondono entro 1 giorno
-
type:bug
Difficoltà 2/5 1-3 ore Idoneità per principianti 82/100
BHoM/MidasCivil_Toolkit#441 ·
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 82/100
autopkg/hjuutilainen-recipes#345 ·
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 86/100
I maintainer di solito rispondono entro 1 giorno