fstar.exe is no longer buildable in F# as a .NET executable #2512
Conversation
…s files and handling that with a Makefile
…ts to make it work on Linux
…d windows, for use with fsharp.extraction.target
… in CallProc.fsproj to avoid pollution from build.sh setting of OTHERFLAGS
| FStar_Integers.fs \ | ||
| FStar_Ref.fs | ||
|
|
||
| all-fs: $(addprefix $(OUTPUT_DIRECTORY)/, $(FS_FILES)) |
There was a problem hiding this comment.
@mateuszbujalski , I now extract files from F* to fs with this Makefile
| @@ -87,7 +89,7 @@ | |||
|
|
|||
| <!-- Run extraction for .fst files --> | |||
| <!-- TODO: What about interfaces? Should we at least run verification for them? --> | |||
| <Exec ConsoleToMsBuild="true" Condition="'%(Compile.Extension)' == '.fst'" Command="$(FSTAR_EXE) $(FSTAR_WARN_ERROR) $(FSTAR_EXTRACTION_FLAGS) $(FSTAR_FLAGS) %(Compile.Identity) --extract "+%(Compile.Filename)"" IgnoreStandardErrorWarningFormat="true" /> | |||
| <Exec ConsoleToMsBuild="true" Condition="'%(Compile.Extension)' == '.fst'" Command="$(CALL_PROC_EXE) $(FSTAR_EXE) $(FSTAR_WARN_ERROR) $(FSTAR_EXTRACTION_FLAGS) $(FSTAR_FLAGS) %(Compile.Identity) --extract "+%(Compile.Filename)"" IgnoreStandardErrorWarningFormat="true" /> | |||
There was a problem hiding this comment.
I retained a version of fsharp.extraction.targets, but wrapped it with CallProc, a small .NET program I wrote to wrap the call to a native fstar.exe. This works on both Windows & Linux
There was a problem hiding this comment.
If there's a way to make this work on Linux without the CallProc wrapper that would be great ... happy to have a PR for that
| <OutputType>Exe</OutputType> | ||
| <RootNamespace>CallProc</RootNamespace> | ||
| <AssemblyName>CallProc</AssemblyName> | ||
| <OtherFlags>--nowarn:0086 --mlcompatibility --nologo</OtherFlags> |
There was a problem hiding this comment.
This is important! Otherwise, if the environment sets the OTHERFLAGS variable (which our build scripts routinely do) then the value of that variable is passed to fsc. So, you must set here. Crazy, but true.
|
|
||
| # -------------------------------------------------------------------- | ||
| nuget-restore: | ||
| $(RUNTIME) VS/.nuget/NuGet.exe restore VS/FStar.sln |
There was a problem hiding this comment.
F#-specific stuff is gone
| boot_dir: | ||
| mkdir -p boot | ||
|
|
||
| boot: $(ALL_BOOT) |
There was a problem hiding this comment.
patching files and copying them to boot is gone
For several years now, we have been using F* after bootstrapping it in OCaml. However, the sources of F* were also compilable in F# (since the sources were in a shared subset of F* and F#), but the F# version lacked many features of the official OCaml version of F*, including basic things checked files and native plugins, and besides had many other unpredictable discrepancies.
So, with this PR, we finally break the ability to compile F* as a .NET executable.
Note, this does not mean that we are de-prioritizing the use of F* in .NET scenarios. F* still very much supports the --codegen FSharp option, the standard library is built after extraction to F# as a .NET dll (ulibfs.dll), and sample solution files in examples/{algorithms, data_structures, hello} all illustrate how to use F* files within an F# project.
The main changes in this PR: