Mateusz Bujalski

Hi, First of all, the package that is currently uploaded to nuget is a hacky version I did for my own purposes and it doesn't have much to do with...

When you use FStar.Mul module: 1. you use the FStar.Mul.fst during verification 2. you use the extracted FStar_Mul.fs compiled into ulib.dll during the build of your F# extracted code and...

It is generated, but in my view it should happen once, when building the nuget, as it's quite costly to verify and extract entire ulib. I also wouldn't want to...

Almost, fs ulib is pre-generated and shipped with nuget in **dll** form, while fst&fsti are shipped as sources for verification :)

You don't always have an fsti for a module in ulib. Besides, I'm not 100% sure F* won't be looking at fst file during verification even if there is a...

@nikswamy I think that packaging F* as a nuget for easy consumption is important for the .net part of the community. My work is still an open PR. I believe...

@nikswamy AFAIR we've discussed in the past reworking the --dep option in fstar to add a mode where it would produce a dependency graph consumable by msbuild (I couldn't find...