FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

F# extraction rely on unsupported features of F# #3368

Open kant2002 opened 3 months ago

kant2002 commented 3 months ago

I did try to export F* source code to F# and was shown following error messages in .NET 6 and up

F* Code

let center : lens circle point = {
  get = (fun c -> c.center);
  put = (fun n c -> {c with center = n})
}

produce extraction error like this

error FS0062: This construct is deprecated. The use of multiple parenthesized type parameters before a generic type name such as '( 
int, int) Map' was deprecated in F# 2.0 and is no longer supported. You can enable this feature by using '--langversion:5.0' and '--mlcompatibility'.

Also export add #light “off” to the beginning of the file which is no longer supported and produces error.

There workarounds for this, but if extraction left as is, it would eventually stagnate and break one day or another.