Skip to content

Sample how to perform export of F* to F# with Nuget

Notifications You must be signed in to change notification settings

kant2002/fstarsample

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

23 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

F* sample

This is sample how to use new Nuget package for Ulib. This repo is to test how things would work, and from that point move toward publishing process.

For now I place ulibfs package to the Myget, once things become stable and both me and F* team are happy, I would work on publishing process.

How to get started

Define environment variable FSTAR_HOME for root folder of FStar installation.

<?xml version="1.0" encoding="utf-8"?>
<configuration>
  <packageSources>
    <!--To inherit the global NuGet package sources remove the <clear/> line below -->
    <clear />
    <add key="fstar-experimental" value="https://codevision.pkgs.visualstudio.com/FStarLang/_packaging/fstarlang/nuget/v3/index.json" />
    <add key="nuget" value="https://api.nuget.org/v3/index.json" />
  </packageSources>
</configuration>

Create new global.json, or add msbuild-sdks values as shown below.

{
  "msbuild-sdks": {
    "FStarLang.Sdk": "0.1.0"
  }
}

then switch to project directory and run usual .NET commands.

dotnet restore
dotnet run

This sample working using MSBuild SDK from this repo: https://github.com/kant2002/FStarMSBuildSdk

Notes

printf sample does not working. It's hitting FStarLang/FStar#2650 and also require FStarLang/FStar#2656 (landed master, not released). So please wait.

gc sample is very much barebone. I would like to make closer to https://github.com/dotnet/runtime/blob/main/src/coreclr/gc/sample/GCSample.cpp in spirit. On the other side, this sample show how you can mix F* and F#

About

Sample how to perform export of F* to F# with Nuget

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published