FStar icon indicating copy to clipboard operation
FStar copied to clipboard

F# extraction rely on unsupported features of F#

Open kant2002 opened this issue 1 year ago • 0 comments

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.

kant2002 avatar Aug 07 '24 04:08 kant2002