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

Migrate to .NET Core #778

Closed
wants to merge 62 commits into from

Conversation

keyboardDrummer
Copy link
Member

@keyboardDrummer keyboardDrummer commented Aug 7, 2020

This PR builds on top of #773 to allow referencing the .NET Core boogie dependencies more easily.

Changes

  • Remove reference to Mono.Cecil since it is no longer needed.
  • Make some method calls in Dafny more explicit to resolve ambiguous references caused by changes in the standard library.
  • Remove Source/Dafny/cce.cs in favor of this Boogie version which seems slightly better. This solves ambiguous references that occurred in the .NET Core build. It's not clear why didn't occur before.
  • The ModelViewer package from Boogie, which is used by DafnyServer has not been ported to .NET Core, and I assume it can not be because it uses .NET framework libraries. It's unclear whether the ModelViewer package has a future in Boogie, since they want to get rid of their .NET framework support altogether. The files used from ModelViewer have been copied into DafnyServer to resolve the issue.
  • Rewrite the CompileTargetProgram method in Compiler-CSharp.cs so it uses Roslyn's Microsoft.CodeAnalysis.CSharp to Compile C#, because the existing method of compiling with System.CodeDom throws a platform not supported exception for Ubuntu in .NET Core. See this thread for more information.
  • Update the lit configuration so it uses dotnet run to get a platform independent way to run, instead of using Mono to run Dafny.exe.

Caveats

No more .NET Framework support

This PR adds support for the .NET Core framework but removes it for the .NET framework. Supporting both platforms at the same time would be difficult, since this PR contains source level changes. To support both platforms at the same time we'd have to duplicate some files and customize each platform to use the right file, but in that case I would suggest considering a fork for .NET Framework support.

Building Boogie

Building Boogie Core 2.4.21 is a pain! The following problems occur, all because of GitVersionTask:

  • An environment variable has to be set before the Boogie dependencies are built, due to a bug in Boogie's GitVersionTask dependency. The problem is described here: .NET Core SDK 3.1.200 breaks build which is using GitVersionTask dotnet/sdk#10878. Note that Boogie dependencies only need to be built once.
  • GitVersionTask requires a nonshallow git clone, while git submodules by default seem to be cloned shallow.
  • GitVersionTask requires the git repository to be on a branch for the project to build, while checking out the Boogie tag v.2.4.21 results in a headless repository.

The above problems can all be solved with some small manual actions, but it's not great asking Dafny devs to perform those steps as part of setting up their Dafny dev environment.

My recommendation is that we can create a Boogie fork that does not have GitVersionTask, so Boogie can be built without manual steps. I would create the boogie fork in the dafny-lang org but I don't have the permissions for that. It would only be a temporary fork until we start consuming Boogie from NuGet.

Alternatively, we can add a script to Dafny to perform these actions.

TestAttribute

The dafny\Test\DafnyTests\TestAttribute.dfy test has been turned off because it calls the NuGet package dafny.msbuild which doesn't work with .NET Core. I'm not sure what that NuGet package is for, where it's built from, and what this test is trying to test, so I'm not sure how to proceed.

Testing

  • Builds and runs on Windows using Visual studio and the dotnet CLI tool
  • Builds and runs on MacOS using the dotnet CLI tool
  • On MacOS using JetBrains rider I ran into the issue that rider didn't pick up the environment variable MSBUILDSINGLELOADCONTEXT=1 that is required for GitVersionTask. I will try to resolve this, but it's also solved by the above suggestion of using a Boogie fork without GitVersionTask.

@keyboardDrummer keyboardDrummer marked this pull request as ready for review August 13, 2020 21:02
@keyboardDrummer
Copy link
Member Author

Made obsolete by #794

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.

1 participant