FStarLang/FStar

Floating point literals are badly handled by the F# extraction mechanism

Open

#793 ouverte le 23 déc. 2016

Voir sur GitHub
 (8 commentaires) (0 réactions) (0 assignés)F* (258 forks)auto 404
area/fsharp-vs-ocamlcomponent/buildcomponent/extractiongood first issuekind/bug

Métriques du dépôt

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

Description

Using literal floating point in some meant-to-be-extracted file like the F* compiler can produce bad results when extracting with the F# version of the F* compiler (seems to be fine with the ocaml version). For example 1.0 is extracted to 1 and 0.99 to 0,99 which are no longer of the same type. A temporary solution is to use float_of_string "1.0" but I would be rather surprised if there is no better way to do that in F#.

Guide contributeur

Direction de recherche
Examinez la génération de code F# pour les littéraux à virgule flottante dans le mécanisme d'extraction F*. Assurez vous que le littéral est émis avec un point décimal et une syntaxe F# correcte (par exemple, '1.0' au lieu de '1').
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.
2
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
1-3 heures
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
Active
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Claire
Prérequis
F*
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
40