Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update hello example to use new MSBuild SDK #2513

Merged
merged 28 commits into from
Jun 3, 2022

Conversation

kant2002
Copy link
Contributor

@kant2002 kant2002 commented Mar 30, 2022

  • This simplify project files
  • This allow to target .NET for free

Notable changes:

  • Retarget Hello from net45 to support net462
  • Dependent project now netstandard2.0 in samples
  • Ulibfs is netstandard2.0 now

@kant2002
Copy link
Contributor Author

kant2002 commented Apr 1, 2022

And here the problem. I did take a look at options to install MSBuild on the Linux and according to these 2 StackOverflow links https://stackoverflow.com/questions/47992371/where-to-get-msbuild-for-linux and https://stackoverflow.com/questions/32546121/how-to-install-msbuild-on-os-x-and-linux there no official way to have msbuild as separate app. You have to install .NET SDK. There 2 LTS version .NET Core 3.1 and .NET 6

Mono itself is support same platforms right now. So I would go with Dotnet SDK since that's easier to setup and in general that's seems to be the way to .NET on the Mac and Linux nowadays. Mono is more and more dissimilated into .NET and I do not think this is safe choice as main target.

Dotnet platform support matrix is here. .NET 6.0 support more platforms and versions then .NET Core 3.1 so I link to that version, even if .NET Core 3.1 earlier in release cycle.

Mono 6 support summarized here.
OSX supported starting from 10.9
Ubuntu supported starting with Ubuntu 16.04
RHEL starting from RHEL 6

@kant2002
Copy link
Contributor Author

kant2002 commented Apr 1, 2022

/cc @mateuszbujalski probably you maybe interested in this one, and to drive discussion.

@kant2002
Copy link
Contributor Author

kant2002 commented Apr 6, 2022

@nikswamy can you take a look?

@@ -11,13 +11,12 @@ ifeq ($(OS),Windows_NT)
else
FSC = fsharpc
# If can't find msbuild, use xbuild, but throw a warning
MSBUILD = $(shell which msbuild || (echo '\n\n\033[0;31mWarning:\033[0m could not find "msbuild", trying (deprecated) "xbuild"\n\n'>&2; which xbuild))
MSBUILD = $(shell which msbuild || (echo "dotnet msbuild"))
#MSBUILD = dotnet msbuild
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you please say more about this change, the earlier code was looking for xbuild in case msbuild is not found, but now we are just printing the message dotnet msbuild, why?

Also what's up with the commented line?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

xbuild is not something which you would like to use for .NET development, even if you use mono. I'm not that familiar with old Mono (which is before dotnet and Mono begin consolidating) but Mono 6 for example use msbuild for the build.

commented line is junk.

mkdir -p packages
$(NUGET) restore UlibFS.sln
find packages -name '*.exe' -exec chmod +x '{}' ';'
$(MSBUILD) /t:Restore UlibFS.sln
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do we need this change? Is msbuild /t:Restore equivalent in that it runs nuget restore, and sets correct permissions on the .exe files?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

msbuild /t:Restore equivalent in that it runs nuget restore.

That's true.

and sets correct permissions on the .exe files?

That's me not finding what kind of "EXE" is affected by this line. I suspect that this is line maybe related to how old Mono was working. I cannot find any package which have EXE inside.

ulib/Makefile Outdated
@@ -50,6 +50,9 @@ ulib-in-fsharp:
+$(MAKE) -f Makefile.extract.fsharp all-fs
+$(MAKE) -C fs/VS

install-ulib-in-fsharp: ulib-in-fsharp
cp fs/bin/Release/netstandard2.0/ulibfs.* ../bin/

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you please say more, what changes in this PR prompted this new target to copy some files?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's to make example hello works. Maybe that's wrong location, but I cannot find who copy ulib.dll to bin folder, without that F# example hello does not work on clean machine.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, thanks for clarifying, let's wait for @mateuszbujalski to chime in.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See https://github.com/FStarLang/FStar/pull/2513/files#r848888382.
I wonder if it makes sense to try to copy pdb when you take a release build anyway.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I thought about having separate changes

  • mechanical changes (like this one where I just bump tooling)
  • some other changes to simplify improve infra.

i.e. this is just foundation for future work. I can make changes here if you like.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I restore functionality per your comment. Overlook and overthink things.

<CALL_PROC_EXE Condition="'$(FSTAR_HOME)' == ''">CallProc.exe</CALL_PROC_EXE>
<CALL_PROC_EXE Condition="'$(FSTAR_HOME)' != ''">$(FSTAR_HOME)\bin\CallProc.exe</CALL_PROC_EXE>
<CALL_PROC_EXE Condition="'$(FSTAR_HOME)' == '' and '$(OS)' != 'Windows_NT' ">CallProc.exe</CALL_PROC_EXE>
<CALL_PROC_EXE Condition="'$(FSTAR_HOME)' != '' and '$(OS)' != 'Windows_NT'">$(FSTAR_HOME)\bin\CallProc.exe</CALL_PROC_EXE>
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do we need this additional check, my understanding (from #2512) is that CallProc.exe works on both Windows and Linux.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I do have issues with CallProc.exe in one of my setups. Not sure why I have that, but I belive that there no need to have separate apps until nescessary. If that's again only for old Mono case, then probably it can be removed completely.

Because of long delay, I'm relatively forgot why specifically I remove that. What I wrote is relative hints which I have. I have to replicate work to provide better explanation.

Copy link
Contributor Author

@kant2002 kant2002 Apr 11, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay. I seems to be understand what issue I was hitting. right now I do not see how CallProc.exe is built in the repo, and I do see the case for complete removal of dependency on Msbuild or XBuild, since it seems the only available modern (>2017) toolchain is .NET SDK and that mean we can use simply dotnet build XXX.csproj and dotnet build YYY.csproj without too much thinking.

I'm still running errands on the internet to better understand that Mono ecosystem, but what I see is that Mono is runtime environment only, no dev support provided and .NET is the future.

There options to use MsBuild as separate executable, but on Ubuntu 20.04 this is on preview feed, and you know, default on Linux is not a Mono right now.

Please correct me if I'm wrong somewhere in my assumptions.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ignore, I otherthinking here about CallProc.exe. All things about Mono still holds. You can read #2513 (comment) about additional rationale for xbuild/msbuild drop

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I didn't really catch up with all of the discussions yet, but do we still need the CallProc.exe at all? If so, do we understand why?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I do not know right now. I just don't want to rock the boat, and remove it if needed in separate PR.

Personally I think think that file is not needed, but I do not know if team use that somehow for having uniform line endings in log (?) or whatever.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Afair, this was added by @nikswamy due to issues on CI as without it fstar.exe was called as mono fstar.exe, when called through msbuild targets.

Now that mono is getting removed it shouldn't be a problem anymore so it could be removed completely.

@nikswamy WDYT?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If it is possible to remove that CallProc, I'll be all for it!

.gitignore Outdated
extracted/
.vs/
.ionide/

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you please remove these editor setting, as discussed on #2508, they can be added locally if needed. Also extracted, I don't see F* generating this directory.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay. I will remove that.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Extracted is generated after you run make -C src ulib-in-fsharp and this is excluded ulib/fs/generated folder which is required to build ulib.fsproj . I would say extracted is generic pattern in this repository to produce extracted files so that's why I place it in the ignore folder.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you please move it to ulib/ (as is done with the ml/extracted)? Note that the directory name is not mandated by F*, it is a command line option and so each "user" of extraction, e.g. ulib, sets it. There are instances in examples where we use _output, and that is ignored locally in examples/.gitignore.

.gitignore Outdated
@@ -31,6 +31,9 @@ cache/
/bin/z3-x64.exe
/src/*/obj

# Generated by build
bin/fstar-compiler-lib

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

When I do git status, I don't see any files in bin in the output, why do we need this entry in .gitignore?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Honestly I forget on what exact configuration it was produced, maybe that's me fiddling, Do I need to provide you with repro steps on clear repo how I reach that state?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That would be great to know, thanks!

@aseemr
Copy link
Collaborator

aseemr commented Apr 11, 2022

Thanks for the PR (and your patience) @kant2002, I added few comments. Since F* usage in F# is not part of our regular setup, it is hard for me to appreciate the improvements.

@mateuszbujalski, could you please look at the changes and share your opinion?

@kant2002
Copy link
Contributor Author

@aseemr if you have capacity, can you also review #2526 since I want work with FStar in VSCode and that's require me to hack LSP support. That's first PR which introduce tests for LSP, so I the faster it lands, the faster I can make independent changes, since test infra would be in place.

.gitignore Outdated
@@ -64,6 +67,7 @@ dump
.depend
.depend.rsp
._depend
.depend.extract.fsharp
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please move it to ulib/.gitignore as well (as with .depend.extract).

@@ -11,13 +11,11 @@ ifeq ($(OS),Windows_NT)
else
FSC = fsharpc
# If can't find msbuild, use xbuild, but throw a warning
MSBUILD = $(shell which msbuild || (echo '\n\n\033[0;31mWarning:\033[0m could not find "msbuild", trying (deprecated) "xbuild"\n\n'>&2; which xbuild))
MSBUILD = $(shell which msbuild || (echo "dotnet msbuild"))
Copy link
Contributor

@mateuszbujalski mateuszbujalski Apr 12, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not just dotnet build?
If you're doing a full upgrade of a toolchain, then I think it makes sense to simplify this a bit more.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree. The only reason why I do not replace, is that I do not know about "all" scenarios which involve "modern Mono". I try to survey people in the wild and seems to be it's safe choice. If @aseemr is support that - I can simplify build even further, because we would not need msbuild.bat altogether which is a win! and whole make file is just dotnet build

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That would be the best scenario. If you do that, I can try testing it on both windows and linux over the weekend.
We would also need someone from F* team to try it out on CI setup as I don't have access there.

</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@kant2002 Previously this was responsible for installing ulibfs.dll into bin directory.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Aah. Then I resurrect parts of it.

@mateuszbujalski
Copy link
Contributor

Looks great, I think upgrading the toolchain is a step in a good direction.
I didn't really have the time to try it out yet, I can do that during the weekend.

@@ -2,6 +2,7 @@
<PropertyGroup>
<TargetFramework>netstandard2.0</TargetFramework>
<OtherFlags>--nowarn:0086 --mlcompatibility --nologo</OtherFlags>
<OutputPath>..\..\bin\</OutputPath>
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's double check if it doesn't produce some extra garbage in the bin directory now.

@kant2002
Copy link
Contributor Author

@mateuszbujalski hopefully you will have time to take a look at PR 😉

@mateuszbujalski
Copy link
Contributor

@kant2002 I've started playing with it. Just on windows for now.
One thing that feels missing is some instruction on how to set things up from sources to be able to use fstar in .net context.

Unless I'm missing something in the process, the CallProc.exe isn't being copied to bin directory after migrating to sdk projects. You should either restore this, and drop CallProc altogether (I'd prefer the latter if possible).

Also, it looks like default target for the hello example is net6.0, which is a bit confusing, as the rest of the codebase uses net462. I think it would be best to keep it consistent with 4.6.2.

@kant2002
Copy link
Contributor Author

One thing that feels missing is some instruction on how to set things up from sources to be able to use fstar in .net context.

Do you know place where steps should be documented?

Unless I'm missing something in the process, the CallProc.exe isn't being copied to bin directory after migrating to sdk projects. You should either restore this, and drop CallProc altogether (I'd prefer the latter if possible).

Remove CallProc.exe

Also, it looks like default target for the hello example is net6.0, which is a bit confusing, as the rest of the codebase uses net462. I think it would be best to keep it consistent with 4.6.2.

It is not clear for me what exactly was confusing for you. Can you clarify? Meanwhile I tell my view on the sample.
I assume we are talking about examples, since ulib is .NET Standard 2.0. I prefer to have .NET 6.0 as default, and supporting .NET Framework 4.6.2 apparently still needed, since I assume nobody would like to change. I did not change a lot of example projects to new format, not because I don't think that's needed, but because I want reduce changeset, so nobody would miss something in the large pile of mundane changes. I can continue port project files to new format in this PR if needed.

@kant2002
Copy link
Contributor Author

Build failure from missing dotnet on CI machines. If somebody can point to CI scripts in the repo, I can update them too.

@mateuszbujalski
Copy link
Contributor

Do you know place where steps should be documented?

I would probably add a separate README_DOTNET.txt or something similar on the top level. @nikswamy?

Unless I'm missing something in the process, the CallProc.exe isn't being copied to bin directory after migrating to sdk projects. You should either restore this, and drop CallProc altogether (I'd prefer the latter if possible).

Remove CallProc.exe

I'll retest :)

It is not clear for me what exactly was confusing for you. Can you clarify?

I didn't have .net6 installed on my machine and when trying to compile the example, I was getting some errors. It took me few minutes to realize what the problem was and that I either have to install some new stuff on my machine, or call dotnet build with extra -f net462 flag.

I think it's nice to support .net6, but if the rest of the repo is stuck at net462, requiring both adds complexity to the required initial setup. IMO, it should be either well documented, or simplified.

@kant2002
Copy link
Contributor Author

I think it's nice to support .net6, but if the rest of the repo is stuck at net462, requiring both adds complexity to the required initial setup.

@mateuszbujalski if you ask me, I would go with only net6.0. Probably that would be easier to setup on Linux/MacOS as well. I do not mind have just one target, or document both options how to run samples. Just capturing feedback from your guys.

IMO, it should be either well documented, or simplified.

Yes, obviously I would document. I have assumption that multitargeting is relatively common in .NET ecosystem, so it does not require additional wording. Seems to be I'm proved wrong.

Will wait for Nick opinion on docs, and proceed from that point.

@@ -63,9 +63,6 @@
<!-- If FSTAR_HOME is not defined then assume that fstar.exe is available on the path -->
<FSTAR_EXE Condition="'$(FSTAR_HOME)' == ''">fstar.exe</FSTAR_EXE>
<FSTAR_EXE Condition="'$(FSTAR_HOME)' != ''">$(FSTAR_HOME)\bin\fstar.exe</FSTAR_EXE>
<CALL_PROC_EXE Condition="'$(FSTAR_HOME)' == ''">CallProc.exe</CALL_PROC_EXE>
<CALL_PROC_EXE Condition="'$(FSTAR_HOME)' != ''">$(FSTAR_HOME)\bin\CallProc.exe</CALL_PROC_EXE>
</PropertyGroup>
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Restore PropertyGroup tag closing.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oops!

# If can't find msbuild, use xbuild, but throw a warning
MSBUILD = $(shell which msbuild || (echo '\n\n\033[0;31mWarning:\033[0m could not find "msbuild", trying (deprecated) "xbuild"\n\n'>&2; which xbuild))
UNAME = $(shell uname -s)
RUNTIME = mono
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@nikswamy Just fyi, the 'mono' was apprearing because RUNTIME was set

<Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
<SchemaVersion>2.0</SchemaVersion>
<ProjectGuid>4b0a4572-302e-4a58-b480-8b783c6bf520</ProjectGuid>
<TargetFrameworks>net462;net6.0</TargetFrameworks>
<OutputType>Exe</OutputType>
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One minor issue I've found is that +x is not set on the produced executable on linux.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I assume that you are talking only about net462 target. net6.0 set -x flag. Honestly I consider net462 as legacy target which I do not want promote. I can understand that FStar users specifically can be very conservative, so I do not want rock the boat too much.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's not a big deal, and indeed it only affects the net462.

@mateuszbujalski
Copy link
Contributor

I've tried this out on both windows and linux and apart from few minor comments it looks good to me.
It's nice how the commands to get up and running are the same no matter the OS.

As I said earlier, it would be good to document the commands needed to get some F# example working, and I guess it needs some setup on a CI machine as well before merging.

Thanks @kant2002 !

@kant2002
Copy link
Contributor Author

kant2002 commented May 7, 2022

I add CI configuraiton of .NET SDK on the build machine via GitHub action https://github.com/actions/setup-dotnet
Would like to know if something else is neeed.

- This simplify project files
- This allow to target .NET for free

Notable changes:
- Retarget Hello from net45 to support net462
- Dependent project now netstandard2.0 in samples
- Ulib is netstandard2.0 now
- Ulib referenced as project, and not as DLL, to simplify dev workflow

Relies on FStarLang#2506
@kant2002
Copy link
Contributor Author

Errors which we are seeing was due to missing reference assemblies. If you have Mono installed, they would be picked up. Unfortunately I have Mono installed on my Linux machine, so I overlook this.
@nikswamy can you try again? I expect clean build right now.

@nikswamy
Copy link
Collaborator

Thanks @kant2002 !

Building it

I tried building this again and the build worked out for me with the following steps:

  1. I ran dotnet msbuild in examples/hello. This failed with:
/usr/share/dotnet/sdk/6.0.300/Sdks/Microsoft.NET.Sdk/targets/Microsoft.PackageDependencyResolution.targets(267,5): error NETSDK1004: Assets file '/home/nswamy/clean/FStar/examples/hello/Hello/obj/project.assets.json' not found. Run a NuGet package restore to generate this file. [/home/nswamy/clean/FStar/examples/hello/Hello/Hello.fsproj]

I looked this up at https://docs.microsoft.com/en-us/nuget/Consume-Packages/Package-restore-troubleshooting#assets-file-projectassetsjson-not-found and based on it did

  1. dotnet msbuild -t:restore

  2. dotnet msbuild

This time the build completed successfully, with just some expected warnings:

/home/nswamy/clean/FStar/examples/hello/TestFSharp/extracted/TestFSharp.fs(1,1): warning FS0062: This construct is for ML compatibility. Consider using a file with extension '.ml' or '.mli' instead. You can disable this warning by using '--mlcompatibility' or '--nowarn:62'. [/home/nswamy/clean/FStar/examples/hello/TestFSharp/TestFSharp.fsproj]
/home/nswamy/clean/FStar/examples/hello/TestSeq/extracted/TestSeq.fs(1,1): warning FS0062: This construct is for ML compatibility. Consider using a file with extension '.ml' or '.mli' instead. You can disable this warning by using '--mlcompatibility' or '--nowarn:62'. [/home/nswamy/clean/FStar/examples/hello/TestSeq/TestSeq.fsproj]

It would be great to add these options to the .fsproj files to suppress these warnings.

Running the program

I'm afraid I'm not able to successfully run the Hello.exe that's produced from this sample. I tried the following and it failed as shown below:

nswamy@NikDev:~/clean/FStar/examples/hello$ ls ./Hello/bin/Debug/net462/Hello.exe
./Hello/bin/Debug/net462/Hello.exe
nswamy@NikDev:~/clean/FStar/examples/hello$ dotnet ./Hello/bin/Debug/net462/Hello.exe
Cannot use file stream for [/home/nswamy/clean/FStar/examples/hello/Hello/bin/Debug/net462/Hello.deps.json]: No such file or directory
A fatal error was encountered. The library 'libhostpolicy.so' required to execute the application was not found in '/home/nswamy/clean/FStar/examples/hello/Hello/bin/Debug/net462/'.
Failed to run as a self-contained app.
  - The application was run as a self-contained app because '/home/nswamy/clean/FStar/examples/hello/Hello/bin/Debug/net462/Hello.runtimeconfig.json' was not found.
  - If this should be a framework-dependent app, add the '/home/nswamy/clean/FStar/examples/hello/Hello/bin/Debug/net462/Hello.runtimeconfig.json' file and specify the appropriate framework.

Maybe something weird going on here, because this output from dotnet msbuild shows where the DLLs and exes are being placed:

 Hello -> /home/nswamy/clean/FStar/examples/hello/Hello/bin/Debug/net6.0/Hello.dll
  TestFSharp -> /home/nswamy/clean/FStar/examples/hello/TestFSharp/bin/Debug/netstandard2.0/TestFSharp.dll
  TestSeq -> /home/nswamy/clean/FStar/examples/hello/TestSeq/bin/Debug/netstandard2.0/TestSeq.dll
  Hello -> /home/nswamy/clean/FStar/examples/hello/Hello/bin/Debug/net462/Hello.exe

Some are in net6.0, some in netstandard2.0 and some in net462

Any idea what's going on here?

Thanks again for all your work on this! Looks like we're really close to the finish line.

@kant2002
Copy link
Contributor Author

I would try use dotnet build and not dotnet msbuild. Technically there should not be any difference.
Also net462 is for Windows only, at least I do not expect that this setup would work on Linux without some hassle. You should try to run using net6.0.
I envision process

dotnet restore
dotnet build
dotnet run -f net6.0

This way to run should works too. At least this is my expectations.

dotnet /home/nswamy/clean/FStar/examples/hello/Hello/bin/Debug/net6.0/Hello.dll

@nikswamy
Copy link
Collaborator

I managed to get things to work on Windows and Linux with net6.0, by running dotnet ..../net6.0/Hello.dll

As far as I see, the steps remaining to complete this PR:

  • I was confused by the presence of net462. I don't think it is necessary to retain this backwards compatibility. Can we please remove it?

  • A top-level README-DOTNET.txt in examples/hello

  • Addressing @tahina-pro's comments on the Dockerfile and yaml files

Thank you!

#light "off"
module Hello
open Prims
open FStar_Pervasives
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@kant2002 I think these extracted files were added by mistake?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes. I already remove them and start ignoring.

@kant2002
Copy link
Contributor Author

@nikswamy and @tahina-pro what else should I do?

@tahina-pro
Copy link
Member

Thanks Andrii for all your work so far! I'm going to test the Dockerfile with the latest Ubuntu version and, if I manage to make it work, I'll submit a PR to your fork, to merge it back here.

@kant2002
Copy link
Contributor Author

@tahina-pro i have no problem with merge, but if that’s only issue so far, can you merge as is, since I have other plans how improve .Net experience and this is foundational PR, so it would be risky work until this truly lands. You guys often busy, so I fear this can be dragged. I know that’s not intentional, but still, delays demotivates sometimes.

I can promise update to latest Ubuntu immidiately after this lands :)

@nikswamy
Copy link
Collaborator

nikswamy commented Jun 1, 2022

hi Andrey, I realize that this has been a lot of work and the conversation here is very long. Thanks for all your work and patience.

However, from Tahina's investigations yesterday, changing the container to use dotnet breaks a part of our CI, where another project using F* was relying on mono, a dependence that we had forgotten about. So, the infrastructure change is quite subtle and it's good, in a way, that we're proceeding slowly.

We clearly want to merge this ASAP, but we have to sort out a few things first with projects that depend on F*. I realize that the delay is frustrating ... but thanks in advance for your patience!

@kant2002
Copy link
Contributor Author

kant2002 commented Jun 1, 2022

I did not know about build failures in the other project. Apologize if I'm being too pushy.
If other project is public, I can try to fix it, or maybe I can try to make this PR works in such way, it would work with Mono. Just asking about options how I can help move forward this PR without breaking anything!

@nikswamy
Copy link
Collaborator

nikswamy commented Jun 1, 2022

If you have other improvements planned that depend on this PR, I think it's safe to assume that this PR will be merged either in its current form, or something very close to it. So, you can continue working on top of this PR.

tahina-pro added a commit to project-everest/everest that referenced this pull request Jun 2, 2022
@tahina-pro tahina-pro self-assigned this Jun 3, 2022
@tahina-pro tahina-pro merged commit cbfa0be into FStarLang:master Jun 3, 2022
@kant2002
Copy link
Contributor Author

kant2002 commented Jun 3, 2022

Thank you!

@kant2002 kant2002 deleted the kant/newmsbuildsdk branch June 3, 2022 18:17
@nikswamy
Copy link
Collaborator

nikswamy commented Jun 3, 2022

Thank you all for the long thread of work on this PR! It's great to have it merged : )

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

5 participants