Extraction examples eg. examples/hello failing with F#

[A-Manning]

building examples/hello with make -C examples/hello fs is failing to build with F#, with the error

Cannot open assembly './out/hello.exe': No such file or directory.
Makefile:47: recipe for target 'fs' failed
make: *** [fs] Error 2

This is due to compilation being commented out in the makefile:

#$(FSC) --nowarn:0086 -o out/hello.exe $(LIB)/fs/prims.fs $(LIB)/fs/io.fs out/Hello.fs

uncommenting gives another error - seemingly related to the removal of Powerpack

error FS0078: Unable to find the file '../../bin/FSharp.PowerPack.dll' in any of
 /usr/lib/mono/4.5
 /FStar/examples/hello
 /usr/lib/cli/fsharp

Placing FSharp.PowerPack.dll in /bin/ then gives a different error:

/FStar/examples/hello/out/Hello.fs(4,12): error FS0039: The namespace 'Pervasives' is not defined

/FStar/examples/hello/out/Hello.fs(9,51): error FS0039: The type 'Pervasives' is not defined

/FStar/examples/hello/out/Hello.fs(9,140): error FS0039: The type 'Pervasives' is not defined

/FStar/examples/hello/out/Hello.fs(10,9): error FS0039: The constructor, module or namespace 'Pervasives' is not defined

[catalin-hritcu]

Problems confirmed. @mtzguido @darrenge Any thoughts?

[A-Manning]

I tracked down the issue with FSharp.Powerpack.dll dependency to prims.fs defining a type l_HashMultiMap which appears nowhere else, but depends on Powerpack.

I've provided a realized FStar.Pervasives.Native.fst in a PR #1092,
but this by itself is not sufficient to build the extracted FStar.Pervasives.fs.
examples/hello will however compile if one changes the dependency in the extracted Hello.fs from FStar.Pervasives to FStar.Pervasives.Native.

The issue in FStar.Pervasives.fs is that F# won't accept type abbreviations that don't use all of the declared type parameters in the type being abbreviated, whereas OCaml will, which gives several FS0035 errors when trying to compile FStar.Pervasives.fs. See https://stackoverflow.com/questions/9838098/getting-fs0035-construct-is-deprecated.
Since GTot functions are extracted to Prims.unit, this happens in st_wp_h, defined in FStar.Pervasives.fst :

let st_pre_h  (heap:Type)          = heap -> GTot Type0
let st_post_h (heap:Type) (a:Type) = a -> heap -> GTot Type0
let st_wp_h   (heap:Type) (a:Type) = st_post_h heap a -> Tot (st_pre_h heap)

Which gets extracted to the following, in FStar.Pervasives.fs:

type 'Aheap st_pre_h =
'Aheap  ->  obj
type ('Aheap, 'Aa) st_post_h =
'Aa  ->  'Aheap  ->  obj
type ('Aheap, 'Aa) st_wp_h =
Prims.unit  ->  'Aheap st_pre_h

Since 'Aa appears as a parameter of st_wp_h but not in the type abbreviation that it is defined by, the F# compiler throws FS0035.

This error is not restricted to instances where F* extracts GTot types to unit; It also occurs, for example, in this perfectly valid F* type definition:

type fs0035 (a:Type) (n:nat) = a

Which extracts to

type ('Aa, 'An) fs0035 = 'Aa

Which is not valid, since 'An does not appear in the type abbreviation.

[A-Manning]

Another issue with F# extraction is that only implicit arguments at the start of a function are erased, whereas the others are extracted to unit and obj:

val fail: #a:Type -> a -> #b:Type -> b -> #c:Type -> (a-> b -> c) -> c
let fail #a x #b y #c f = f x y

val pass: #a:Type -> #b:Type -> #c:Type -> a -> b -> (a-> b -> c) -> c
let pass #a #b #c x y f = f x y

Extracts to

let fail = (fun ( x  :  'Aa ) ( b  :  Prims.unit ) ( y  :  obj ) ( c  :  Prims.unit ) ( f1  :  'Aa  ->  obj  ->  obj ) -> (f1 x y))
let pass = (fun ( x  :  'Aa ) ( y  :  'Ab ) ( f1  :  'Aa  ->  'Ab  ->  'Ac ) -> (f1 x y))

These both compile just fine, but if one tries to actually use them :

let main = fail () () () () (fun x y -> x = y)

fails to compile with error

error FS0001: This expression was expected to have type
    obj    
but here has type
    bool

whereas let main = pass () () (fun x y -> x = y) compiles just fine.

[catalin-hritcu]

@A-Manning Thanks a lot for looking into these problems. This is starting to look like an F# extraction pinhada than a bug report though. How about keeping this report for issues related to extracting the hello world example, and filing more issues for the other problems?

[A-Manning]

Ok, should I make seperate issues for each problem, or one issue for F# extraction issues?

[catalin-hritcu]

Your call. We do allow for "meta issues", just that they tend to stick around forever.

[drvink]

Besides the issue raised in fsharp/fslang-suggestions#597 (F# requiring the use of all declared type parameters in type abbreviations), parts of FStar.Pervasives are extracted incorrectly (?) to F#, resulting in errors involving undefined tags in DUs, e.g.:

fstar/examples/hello/out/FStar.Pervasives.fs(63,3): error FS0039: The pattern discriminator 'U__V' is not defined.

[A-Manning]

@drvink Which version of F* are you using? I can't reproduce this error.

[drvink]

@A-Manning

arch-vm[1003]:~% fstar.exe --version
F* 0.9.5.0
platform=Linux_x86_64
compiler=OCaml 4.04.2
date=2017-09-11T23:54:07+09:00
commit=9c3cc3626

I was trying to compile the extracted source by hand, since the Makefile doesn't seem to do it, so I did:

arch-vm[1015]:~/.opam/4.04.2+flambda/packages.dev/fstar/examples/hello% make FSTAR=`which fstar.exe` fs
/home/mdl/.opam/4.04.2+flambda/bin/fstar.exe   --odir out --codegen FSharp hello.fst
./hello.fst(5,0-5,37): (Warning) Top-level let-bindings must be total; this term may have effects
Extracted module Native
Extracted module Pervasives
Extracted module Exn
Extracted module Classical
Extracted module FunctionalExtensionality
Extracted module Set
Extracted module Preorder
Extracted module StrongExcludedMiddle
Extracted module PropositionalExtensionality
Extracted module PredicateExtensionality
Extracted module TSet
Extracted module Heap
Extracted module ST
Extracted module All
Extracted module Hello
Verified module: Hello (405 milliseconds)
All verification conditions discharged successfully
mono ./out/hello.exe
Cannot open assembly './out/hello.exe': No such file or directory.
make: *** [Makefile:52: fs] Error 2

...and then I built the stuff in ulib/fs, since the extracted source required it:

arch-vm[1020]:~/.opam/4.04.2+flambda/packages.dev/fstar/ulib/fs% make
fsharpc --mlcompatibility --nologo  --nowarn:0086 -a prims.fs st.fs all.fs io.fs

...then you should be able to see these errors if you try running something like:

arch-vm[1024]:~/.opam/4.04.2+flambda/packages.dev/fstar/examples/hello/out% fsharpc --mlcompatibility '--lib:../../../ulib/fs' -r:io.dll FStar.Pervasives.fs Hello.fs

[A-Manning]

This is probably due to the makefile for examples/hello being out of date, and/or the F# realizations in ulib being out of date. I'll investigate further when I have some time.

[nikswamy]

Especially given #1096 ... it seems that extraction to F# is far from complete. So, fixing hello.exe on its own is really just a small first step.

[catalin-hritcu]

Was there any progress on this since Sept 2017?

I run over it again recently: https://fstar.zulipchat.com/#narrow/stream/184683-questions-and.20help/topic/Compiling.20to.20F.23

[catalin-hritcu]

It seems that F# extraction regressed further at least on this Hello example. Now we're getting an empty fs file whose name is .fs: https://fstar.zulipchat.com/#narrow/stream/184683-questions-and.20help/topic/Extracting.20Hello.20to.20F.23

[DejanMilicic]

F# extraction works again in the version 0.9.6.001

[catalin-hritcu]

version 0.9.6 is very old, so no

[mateuszbujalski]

Hi,

@Nik Swamy, I was playing a little bit with your branch (nik_fsharp_extraction). I can say that the most basic hello example works fine now :). I have a few questions/concerns before moving forward.

1. It looks like testing any more complicated examples will require building out the ulib/fs first. Is my understanding correct that ulib/fs should be composed of the files extracted from ulib/*.fst (excluding the modules that have 'manual' implementation provided in ulib/fs) + files provided within ulib/fs?

2. Extracted F# code always opens the "FStar.Pervasives", whereas ocaml code doesn't seem to do that. The extracted code doesn't depend on it though, just "FStar.Pervasives.Native". Should FStar.Pervasives not be automatically added to extracted F# code?

3. F# usually complains about having FStar.Pervasives and FStar.Pervasives.Native in the same assembly (error FS0247: A namespace and a module named 'FStar.Pervasives' both occur in two parts of this assembly). It doesn't look like FStar.Pervasives is actually used by the extracted code, but I suppose there will be other modules that cause similar issues in ulib? Any ideas how to work around that?

4. Does it make sense to put examples as part of the VS solution and make them depend on the ulibfs project that I've added recently? I'm still wondering if it's better to have a single 'examples' project that would generate executables for all examples, or a project per example.

[nikswamy]

Hi Mateusz,

Thanks for digging into this!

1. Yes. For ulib/fs we should follow the structure of ulib/ml. Several modules have hand-rolled implementation, but most come from ulib/ml/extracted which are extracted from the .fst files in ulib. Porting each ulib/ml file to ulib/fs is probably tedious, but I hope it is relatively straightforward also.

2 & 3. As we try more examples, we will certainly have code that depends on FStar.Pervasives. On the OCaml side, this module appears as ulib/ml/extracted/FStar_Pervasives.ml. I agree that we should probably not have an open FStar.Pervasives in an F# generated code, and instead treat it like any other module and reference its symbols with fully qualified names. As for namespace/module conventions, I think we should follow the same approach as we do for OCaml, i.e., F* module names A.B.C are rewritten to just an atomic module identifier "A_B_C".

4. I'd be more in favor of having a .sln for each example. And this can reference the ulib/fs project. Hopefully that also establishes a template/style guide for others trying to build F# projects from F* code. Do you buy it?

Thanks again!
-Nik

[mateuszbujalski]

Thanks!

Re 4. Would changing the directory structure in examples like below be ok?

examples/
    example1/
        Example1.sln  -- allows to build all examples within example1 (e.g. hello)
        makefile         -- would work as today, just the paths inside would change to reflect new directory structure
        Example1_A/
            Example1_A.fst
            Example1_A.fsproj -- generates Example1_A.fs file in fsout directory with an msbuild target and the generated file(s) are added to compilation. depends on ulibfs library. Would also need a 'test' target to actually run the example if needed
        Example1_B/
            Example1_B.fst
            Example1_B.fsproj

One thing I'm not sure about yet is how to deal with examples that consist of multiple fst files. In particular how to make the fsproj include the generated files in the right order for F# compilation to work.

[nikswamy]

Hi Mateusz, Sorry for the slow reply!

That directory structure sounds fine to me.

Regarding the order of dependences: F* has a dependence analysis which currently emits dependences in makefile format for F*, OCaml and Kremlin. See the output of fstar --dep full A.fst and its use in building .depend files in many of our makefiles. We could rig that to add an option, e.g., fstar --dep full --codegen FSharp A.fst could also emit the list of .fs files in the order needed for an fsproj.

[mateuszbujalski]

@nikswamy

I have few more questions about ulib extraction :)

1. Looking at how it works for ocaml, it seems that extraction is invoked for each module separately. Is this on purpose? Would it make sense to call fstar to extract all modules at once? Or it's not a good idea for some reason?
2. Is the order in which those modules are extracted important (i.e. order of invocations)? If we switched to a single invocation for all modules, would the order of files passed to fstar be important? Or would fstar handle the ordering of fst(i) files internally?
3. My current understanding is that fsti files are only used for typechecking of other modules, but they are not being extracted themselves. Is that correct? It seems they are all lax checked during the dependency analysis run that happens before extraction, and the lax.cache is later used to typecheck other modules?

[nikswamy]

Hi Mateusz,

All three of your questions are intertwined in some way. The short answer is that F* is heavily biased towards verifying and extracting one module at a time. In some cases, it is possible to verify and extract multiple modules in a single invocation. However, this is not a common usage in all but the simplest projects.

Now, a more elaborate response.

.fsti files: Interface files are an essential mechanism in F* for enforcing abstraction. Consider the following example:

A.fsti: An interface for module A that says that A provides some boolean a

module A
val a : bool

A.fst: An implementation of the interface providing concretely the value true

module A
let a = true

B.fst: A client module of A. It can only "see" A's interface. In particular, it cannot rely on A.a being true (the expect_failure [19] attribute states that that definition is expected to fail with Error 19).

module B
[@@expect_failure [19]]
let test = assert (A.a == true)

Now, if you try to invoke F* on all these files together

$ fstar A.fsti A.fst B.fst
(Error 117) You may have a cyclic dependence on module a: use --dep full t
o confirm. Alternatively, invoking fstar with A.fst on the command line breaks th
e abstraction imposed by its interface A.fsti; if you really want this behavior a
dd the option '--expose_interfaces'
1 error was reported (see above)

That's because in this single invocation, F* cannot guarantee to hide the implementation details of A.fst from B.fst. You have to verify those files separately. (The --expose_interfaces option is not really recommended ... it breaks abstraction).

So, coming to your questions

1. Looking at how it works for ocaml, it seems that extraction is invoked for each module separately. Is this on purpose? Would it make sense to call fstar to extract all modules at once? Or it's not a good idea for some reason?

We at least have to verify modules one at a time with separate invocations of F*. We could, conceivably, after verifying all modules and producing .checked files, extract them all to .fs or .ml in a single additional invocation. But, I'm not sure if that adds much value.

2. Is the order in which those modules are extracted important (i.e. order of invocations)? If we switched to a single invocation for all modules, would the order of files passed to fstar be important? Or would fstar handle the ordering of fst(i) files internally?

Not really applicable, since single invocation for all modules doesn't fly.

3. My current understanding is that fsti files are only used for typechecking of other modules, but they are not being extracted themselves. Is that correct? It seems they are all lax checked during the dependency analysis run that happens before extraction, and the lax.cache is later used to typecheck other modules?

First, about lax: Lax checking and lax.cache are a bit peculiar. Basically, running F* with --lax disables the verifier. One shouldn't really be using --lax in a project where verification is intended. We currenly use --lax primarily for bootstrapping the compiler sources (which are not verified). There is also a remnant use of lax for the extraction of fstarlib ... but this should probably be removed, since those files are also verified properly (without --lax) as part of make uib.

Then interfaces: These are definitely typechecked and extracted. An interface in F* can include both type signatures, definitions of inductive types, as well as let bindings. All of this is verified and extracted along with the implementation files. See https://github.com/FStarLang/FStar/wiki/F%E2%98%85-Interfaces-(simple-version)

I shouldn't be too hard to get fstar --dep full to also emit F# dependency information. I could easily add that. But, one implicit assumption here is that in order to run multiple invocations of F* to build your entire project, that one is willing to use make to schedule the build properly and incrementally. Are you able to use cygwin/make in your setup?

[mateuszbujalski]

Thanks, that's really helpful! It looks like I've misunderstood how some things work :)

I shouldn't be too hard to get fstar --dep full to also emit F# dependency information. I could easily add that. But, one implicit assumption here is that in order to run multiple invocations of F* to build your entire project, that one is willing to use make to schedule the build properly and incrementally. Are you able to use cygwin/make in your setup?

I might be able to use it now, but I most likely won't be able to do that in my work environment, so I would prefer to avoid adding a dependency on make for windows build.

I was planning to look into generating the right order with fstar later, once I make sure that the extraction works for ulib and examples (at least some non-trivial examples). For now, I'm ordering the extraction manually with fsproj - the current code invokes fstar per FStarSourceFile item in the order those items are defined in the project file.

My idea was that I could add "--dep msbuild" option that would simply generate an ordered list of modules to extract, plus perhaps a separate list of fs files to compile if we can't assume those are the same (up to a small name transformation like FStar.Module.fst -> FStar_Module.fs).

Then interfaces: These are definitely typechecked and extracted. An interface in F* can include both type signatures, definitions of inductive types, as well as let bindings. All of this is verified and extracted along with the implementation files. See https://github.com/FStarLang/FStar/wiki/F%E2%98%85-Interfaces-(simple-version)

I didn't see any codegen commands that would be running on an fsti file when building ocaml version of ulib, so can I assume that ulib always uses 'realised modules' for interfaces? Or should we also allow https://github.com/FStarLang/FStar/wiki/F★-interfaces-%28split-file%2C-more-complicated-version%29?

[nikswamy]

No, it actually uses the complicated version quite extensively.

For example, take FStar.BigOps.fsti and FStar.BigOps.fst. The extracted code FStar_BigOps.ml contains elements of both the .fst and the .fsti files.