FStarLang/FStar

assert are never extracted even with `--mlish`

Open

#984 ouverte le 13 avr. 2017

Voir sur GitHub
 (0 commentaires) (0 réactions) (0 assignés)F* (258 forks)auto 404
area/error-messagescomponent/extractiongood first issue

Métriques du dépôt

Stars
 (3 068 stars)
Métriques de merge PR
 (Métriques PR en attente)

Description

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.

Guide contributeur

Direction de recherche
Enquêtez sur l'extraction des assertions dans le compilateur F* et identifiez pourquoi les assertions ne sont pas extraites vers OCaml lors de l'utilisation du drapeau mlish.
Stack technique
Aucun
Domaine
compilers
Type d'issue
Bug
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
3
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
Une demi journée
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
Récente
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Claire
Prérequis
GitF* basics
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
50