[WIP] Dotnet core compat

[samuelgruetter]

I managed to build dafny on .NET Core on Fedora, and I can generate a linux executable based on .NET Core, which successfully can verify a .dfy file, but when it tries to compile it to C#, it fails because it uses CodeDOM, which has a .NET Core package which makes compilation of dafny succeed, but fails at runtime because no compatible compiler is found, and it seems that CodeDOM is not available on .NET Core and one should use Roslyn instead, which has a different API. See https://stackoverflow.com/questions/38441249/net-core-dynamic-compilation.

Steps to run it on my Fedora machine:

sudo dnf install dotnet-sdk-2.2

git clone [email protected]:Z3Prover/z3.git

cd z3
git checkout z3-4.8.4
python scripts/mk_make.py
cd build
make
cd ../../

git clone [email protected]:boogie-org/boogie.git

cd boogie

dotnet build Source/BoogieDriver/BoogieDriver-NetCore.csproj
dotnet publish Source/BoogieDriver/BoogieDriver-NetCore.csproj --output `pwd`/Binaries

cd ..

git clone [email protected]:samuelgruetter/dafny.git
cd dafny
git checkout dotnet_core_compat

dotnet build Source/Dafny.sln --framework netcoreapp2.2

dotnet publish Source/Dafny.sln --framework netcoreapp2.2 --runtime linux-x64 --output `pwd`/Binaries

mkdir -p ./Binaries/z3/bin/
cp ../z3/build/z3 ./Binaries/z3/bin/

What prevents us from moving to dotnet is that it seems that no CodeDOM implementation is available for .NET core at runtime. This could probably be fixed by using the Roselyn API instead of the CodeDOM API for compilation of C# programs.
However, at this point it might make sense to ask if the dafny program should invoke the C# compiler (and go compiler, Java compiler, etc) at all, because that works for simple toy examples, but for more serious software engineering projects with library dependencies, compiling a set of source files is a complex task for which you have to use a dedicated tool (such as eg the dotnet CLI, nuget, maven, etc). Trying to make dafny as smart as these tools will never work, and it seems to me that dafny trying to compile cs files to assembly violates the "separation of concerns" software engineering principle. So my suggestion here would be to entirely remove the code which invokes the C# compiler (and other language compilers) from dafny, and have the user invoke csc, dotnet build, mvn build or any other such command on their own. And maybe provide a simple shell or bat script for the trivial toy example case, which invokes dafny and then csc and runs the executable.

[robin-aws]

+1 for removing any responsibility for compiling C# from the Dafny CLI. I'm running into similar issues trying to add testing support (#451). It's also definitely not scalable to attempt to add the same support for compiling and running in every target language for parity.

[keyboardDrummer]

Closing this PR since Dafny has moved to .NET Core.

What prevents us from moving to dotnet is that it seems that no CodeDOM implementation is available for .NET core at runtime. This could probably be fixed by using the Roselyn API instead of the CodeDOM API for compilation of C# programs.

We have indeed moved to using the Roslyn API.