FStarLang/FStar

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

Open

#793 geöffnet am 23. Dez. 2016

Auf GitHub ansehen
 (8 Kommentare) (0 Reaktionen) (0 zugewiesene Personen)F* (258 Forks)auto 404
area/fsharp-vs-ocamlcomponent/buildcomponent/extractiongood first issuekind/bug

Repository-Metriken

Stars
 (3.068 Stars)
PR-Merge-Metriken
 (PR-Metriken ausstehend)

Beschreibung

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#.

Contributor Guide

Research-Richtung
Untersuchen Sie die F# Codegenerierung für Fließkommaliterale im F* Extraktionsmechanismus. Stellen Sie sicher, dass das Literal mit einem Dezimalpunkt und korrekter F# Syntax (z. B. '1.0' statt '1') ausgegeben wird.
Tech Stack
Keine
Domain
compilers
Issue Type
Fehler
SchwierigkeitGeschätzte Implementierungsschwierigkeit für neue Contributors, von 1 für sehr kleine Änderungen bis 5 für Expertenarbeit.
2
Geschätzte ZeitEin grober Zeitrahmen, um zu recherchieren, zu implementieren, zu testen und einen Pull Request vorzubereiten.
1-3 Stunden
AktivitätsstatusWie verfügbar das Issue gerade wirkt: frisch, aktiv, stale, blockiert oder wartet auf Maintainer-Input.
Aktiv
KlarheitWie klar das Issue die erwartete Änderung, Akzeptanzkriterien und den nächsten Schritt erklärt.
Klar
Voraussetzungen
F*
EinsteigerfreundlichkeitEin Score von 1 bis 100, der schätzt, wie zugänglich dieses Issue für First-Time Contributors ist.
40