Publishing F* as nuget

[mateuszbujalski]

IDEA

With weekly binary packages fixed (https://github.com/FStarLang/FStar/pull/2275), it should be quite simple to extend the build process to also publish a nuget package. I have some bespoke powershell script that does the packaging and it makes using F* with F# extraction really easy (particularly in environments where setting up the OCaml setup to build master is impossible). The usage looks as below:

1. Take any F# project (new or existing one)
2. Add a reference to the F* nuget
3. Add fst(i) file to your project (the same way you would normally add a new F# file) - make sure the action is set to 'Compile'

With this, all your fst files are extracted into fs files, and then those fs files are added to the list of compiled sources in the F# project. There's no problem with mixing F* and F# sources as extraction target makes sure to keep the order of files in the project unchanged. The same targets are used to build ulib library for F# currently.

If you feel like this would be good to have, I'd be happy to contribute. Let me know what you think.

Building the nuget

We need the build process to provide an F* executable and an ulib extracted to F# and compiled. Then, we need create a certain directory structure and put files in there as described below:

• tools/bin
  • fstar.exe
  • . from z3-4.8.5-x64-win/bin
  • mingw dlls
• tools/ulib
  • fstar/ulib contents - whatever is needed for verification
• lib
  • ulibfs.[dll|pdb|xml]
• build
  • nuget_name.targets (see fsharp.extraction.targets.txt attached)
  • nuget_name.props (attached)
• nuget_name.nuspec (attached)

One you have this, you need to set the version inside nuget_name.nuspec (can probably reuse the datestamp from weekly build), and run nuget.exe: nuget.exe pack nuget_name.nuspec -OutputDirectory out

It's also possible to upload to either github packages or nuget.org for easy consumption (requires providing apikey to the script).

How the integration works

The nuget_name.props and nuget_name.targets inside build directory of a nuget are automatically referenced by the F# project (it's a nuget convention). A props file sets a FSTAR_HOME path (and some default F* flags) used later with the msbuild targets defined in targets file. The targets are using fstar from tools directory (it contains bin and ulib) to extract F* code in the project into F# sources that are later compiled together with the rest of F# code in the project. The lib directory contains an ulibfs.dll, which is used by F# for compilation and at runtime (F# project is automatically referencing libraries from lib due to how nugets work).

fsharp.extraction.targets.txt FStar.Windows.Ocaml.Unofficial.nuspec.txt FStar.Windows.Ocaml.Unofficial.props.txt

[WhiteBlackGoose]

Hey. I've seen your package, but I'm not sure it's the way. Cannot we pack all fs files into a F# library instead of packing source files?

[mateuszbujalski]

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 what is described here or implemented in the related PR. It also uses a fairly old version of F*.

For a nuget to be fully usable when writing code in F* and compiling it inside a F# codebase you need more than just extracted and compiled ulib. You also need fst(i) files from ulib available to be able to verify your F* projects against during build.

Having said that, the script in the PR can certainly be improved by pruning the contens of ulib more. AFAIR it also needs a small fix to support both framework and sdk style projects (I'm not sure if I published that change or only did it locally at the time).

Moreover, F# extraction still doesn't work for a big part of ulib so it won't be possible to use everything from a .net codebase (although what works is already usable). The main issue here is that .net doesn't allow implementing equivalent of Obj.magic so dependently typed code will fail at runtime when extracted to F#.

The PR has been open for almost a year and didn't receive a lot of attention, so there's probably not that many people that would be interested in using F* from .net codebase. And merging it would add some maintanence burden to the F* team. Still, even if it's not merged, if it's needed it should be easy enough to grab the scripts from the PR and build a nuget package locally.

Cheers, Mateusz.

[WhiteBlackGoose]

For a nuget to be fully usable when writing code in F* and compiling it inside a F# codebase you need more than just extracted and compiled ulib. You also need fst(i) files from ulib available to be able to verify your F* projects against during build.

Oh... I didn't think about it. Fair.

Alright, I see, thank you

[WhiteBlackGoose]

Actually no, I don't understand. When I use F* modules, I use them primarily from my F* files, e. g.

open FStar.Mul

let a = b * c

So it does the verification. Now, once the verification is finished, we don't care about how type safe the F# codegen is, right?

[mateuszbujalski]

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 during runtime
3. You want the two to come from the same version of F* codebase

I'm only guessing, but your misunderstanding might be about the fact that F# ulib is not just the contents of ulib/fs, but rather all the F* code that should get extracted and compiled. Files inside ulib/fs are a special case (hack?) where we want to use a hand-written F# code rather than the extracted version of a relevant module.

Hope it helps :)

[WhiteBlackGoose]

Hmmm, I probably don't understand 100%, but isn't it that the actual ulib gets code-generated by fstar --codegen FSharp for F#? The only things shipped in this nuget package would be the things which are missing, that is, not generated by fstar. For example in my case it generated everything but FStar_Pervasives, so I had to take the relevant FStar.Pervasivs.fst and ran fstar on it to get the F# file, which I included in the package.

(and btw, sorry if my questions/statements sound silly, I'm very new to F*, as you already probably noticed)

[mateuszbujalski]

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 force anyone to install F* machine-wide, but rather pin F* version used for a particular codebase. I guess it's a matter of what you need and a tradeoff between the package size and being able to support various usage scenarios.

[WhiteBlackGoose]

Ohhhh, so the idea is that fst are pre-generated and shipped with nuget in fs forms, while fsti are shipped as sources to verify the types? If so, it makes perfect sense to me.

I also wouldn't want to force anyone to install F* machine-wide, but rather pin F* version used for a particular codebase.

Hmm...

[mateuszbujalski]

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

[WhiteBlackGoose]

What's the point to ship sources of fst? Don't we only need fsti?

fs ulib is pre-generated and shipped with nuget in dll form

Right, there's no point to ship fs files as sources...

[mateuszbujalski]

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 corresponding interface file (e.g. it might be possible to query for a definition with Meta-F*?). However, if that's something we can assume safely, then it's possible to prune the contents of ulib in a nuget even more.

[lucasteles]

The PR has been open for almost a year and didn't receive a lot of attention, so there's probably not that many people that would be interested in using F* from .net codebase. And merging it would add some maintanence burden to the F* team. Still, even if it's not merged, if it's needed it should be easy enough to grab the scripts from the PR and build a nuget package locally.

I would love to use it in .net 😢

[lucasteles]

This 2 PRs maybe cold help to achieve this

https://github.com/FStarLang/FStar/pull/2607 https://github.com/FStarLang/FStar/pull/2608

[kant2002]

It seems issue about to be resolved. I have create MSBuild SDK and package scripts which can using of F* from F# much easier. Almost the same as existing dotnet build and dotnet run model. I already announce that on Slack, but here it would be visible.

• MSBuild SDK https://github.com/kant2002/fstarmsbuildsdk
• Repo with samples https://github.com/kant2002/fstarsample

Samples are work in progress. You technically don't need install F* locally, since dotnet restore will download latest version of F* and run extraction process for you.

Would like to receive more feedback on usage of this approach.

[lucasteles]

It seems issue about to be resolved. I have create MSBuild SDK and package scripts which can using of F* from F# much easier. Almost the same as existing dotnet build and dotnet run model. I already announce that on Slack, but here it would be visible.

• MSBuild SDK https://github.com/kant2002/fstarmsbuildsdk
• Repo with samples https://github.com/kant2002/fstarsample

Samples are work in progress. You technically don't need install F* locally, since dotnet restore will download latest version of F* and run extraction process for you.

Would like to receive more feedback on usage of this approach.

Thats amazing

Would be great to have a dotnet-tool for it, dotnet-fstar, maybe some templates, which give kinda of a first-class dev experience

[kant2002]

Yeah. At this point creation of templates is something which I can do on weekends. Where I need help is to have tutorials in F*. Right now I would like to have literally anything which can showcase F* and F#, but would be good if content would be enterprise oriented and not super academic.

I also would applaud not only code contribution, but idea contributions. For example payment gateway interaction, or maybe toy hardware, or synchronization processes for offline data.

Пн, 15 авг. 2022 г. в 21:05, Lucas Teles @.***>:

It seems issue about to be resolved. I have create MSBuild SDK and package scripts which can using of F* from F# much easier. Almost the same as existing dotnet build and dotnet run model. I already announce that on Slack, but here it would be visible.

• MSBuild SDK https://github.com/kant2002/fstarmsbuildsdk
• Repo with samples https://github.com/kant2002/fstarsample

Samples are work in progress. You technically don't need install F* locally, since dotnet restore will download latest version of F* and run extraction process for you.

Would like to receive more feedback on usage of this approach.

Thats amazing

Would be great to have a dotnet-tool for it, dotnet-fstar, maybe some templates, which give kinda of a first-class dev experience

— Reply to this email directly, view it on GitHub https://github.com/FStarLang/FStar/issues/2278#issuecomment-1215129871, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABAPKNZ5R5FGVP625QK6343VZJMDJANCNFSM43RWTBZQ . You are receiving this because you commented.Message ID: @.***>

[kant2002]

@lucasteles as I said earlier, I have now templates

Install templates

dotnet new install FStarLang.DotNet.Common.ProjectTemplates.1.0::0.0.9 --nuget-source https://codevision.pkgs.visualstudio.com/FStarLang/_packaging/fstarlang/nuget/v3/index.json

and now you can

dotnet new fstarconsole -o helloworld

Now left most complicated part, have interesting samples so all that tooling would not be for nothing.