FStarLang/FStar

assert are never extracted even with `--mlish`

Open

#984 aperta il 13 apr 2017

Vedi su GitHub
 (0 commenti) (0 reazioni) (0 assegnatari)F* (258 fork)auto 404
area/error-messagescomponent/extractiongood first issue

Metriche repository

Star
 (3068 star)
Metriche merge PR
 (Metriche PR in attesa)

Descrizione

The function assert is never extracted to OCaml. This is not very nice when using the ocaml-based F* compiler and getting a Failure("Impossible") because an invariant was broken.

It would be nice to extract the assertions when they do correspond to runtime checks as they are in the compiler.

Guida contributor

Direzione di ricerca
Investiga l'estrazione delle asserzioni nel compilatore F* e identifica perché le asserzioni non vengono estratte in OCaml quando si usa il flag mlish.
Tech stack
Nessuno
Dominio
compilers
Tipo issue
Bug
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
Mezza giornata
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Nuova
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
GitF* basics
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
50