Z3 bindings don't build on .NET Core 2 without a lot of manual migration

[MattWindsor91]

I've tried to build the Z3 bindings on macos 10.13 using the .NET Core SDK version 2.1.3, and run into a few problems that needed manual intervention.

* `project.json` being the prerelease version of the .NET Core project file, one has to run `dotnet migrate` to get a .NET Core 1.x MSBuild.
* This MSBuild doesn't have version information---I'm not sure how to make cmake populate this, so I had to manually add it.
* Even so, .NET Core 2.x seems to provide code contracts now, so if I try to upgrade the MSBuild to 2.x I have to delete `DummyContracts.cs`.
* Using cmake/Ninja, nothing seems to copy the `build/src/api/dotnet/*.cs` files to somewhere the .NET Core builder can find them, causing lots of `CS0246` errors for missing native API bridging.  Copying these manually worked.  I seem to have got this working before, so maybe it's an issue with the build generator I'm using...?

For more detail, here are the steps I've taken to get a successful build (against branch `d86ef02`):

```
$ git clone https://github.com/Z3Prover/z3 z3-2
$ mkdir z3-2/build
$ cd z3-2/build
$ cmake -G 'Ninja' ..
$ ccmake .
[ set BUILD_DOTNET_BINDINGS to ON, configure twice and generate ]
$ ninja
[ build succeeds ]
$ cd ../src/api/dotnet/core
```

The .NET Core project file is in Preview 2 `project.json` format, needing a `dotnet migrate`:

```
$ dotnet migrate
[ migration succeeds ]
$ dotnet restore
[ restoration succeeds ]
$ dotnet build
/.../src/api/dotnet/Expr.cs(62,16): error CS0246: The type or namespace name 'Z3_lbool' could not be found (are you missing a using directive or an assembly reference?) [/.../src/api/dotnet/core/core.csproj]
[ 20 more CS0246 follow ]
```

The `core.csproj` `dotnet migrate` generates looks like this:

```xml
<Project Sdk="Microsoft.Net.Sdk">

  <PropertyGroup>
    <TargetFramework>netcoreapp1.0</TargetFramework>
    <DefineConstants>$(DefineConstants);DOTNET_CORE</DefineConstants>
    <DebugType>portable</DebugType>
    <AssemblyName>Microsoft.Z3</AssemblyName>
    <OutputType>Library</OutputType>
    <PackageId>core</PackageId>
    <PackageTargetFallback>$(PackageTargetFallback);dnxcore50</PackageTargetFallback>
    <RuntimeFrameworkVersion>1.0.4</RuntimeFrameworkVersion>
  </PropertyGroup>

  <ItemGroup>
    <Compile Include="..\*.cs" Exclude="bin\**;obj\**;**\*.xproj;packages\**" />
  </ItemGroup>

</Project>
```

The glob at the bottom doesn't include `Native.cs` etc., which are in `build\src\api\dotnet`.  Copying these over seems to fix the build, but I'm not sure why this step is needed.

To get a .NET Core 2.0 build with an accurate version, I `mv DummyContracts.cs DummyContracts.cs.old` and hacked the msbuild to be:

```xml
<Project Sdk="Microsoft.Net.Sdk">

  <PropertyGroup>
    <TargetFramework>netcoreapp2.0</TargetFramework>
    <DefineConstants>$(DefineConstants);DOTNET_CORE</DefineConstants>
    <DebugType>portable</DebugType>
    <AssemblyName>Microsoft.Z3</AssemblyName>
    <AssemblyVersion>4.6.0.0</AssemblyVersion>
    <OutputType>Library</OutputType>
    <PackageId>core</PackageId>
    <AssetTargetFallback>$(AssetTargetFallback);dnxcore50</AssetTargetFallback>
    <RuntimeFrameworkVersion>2.0.4</RuntimeFrameworkVersion>
  </PropertyGroup>

  <ItemGroup>
    <Compile Include="..\*.cs" Exclude="bin\**;obj\**;**\*.xproj;packages\**" />
  </ItemGroup>

</Project>
```

`dotnet build` then works and gives me a `Microsoft.Z3.dll` I can slot in front of the packaged version to get Z3 working.

I figure this kind of build is quite niche at the moment, but it'd be nice to have a slightly smoother build process!

[delcypher]

@MattWindsor91 Thanks for giving this a try and using the CMake based build system to do so. I know ".NET core" exists but I don't have any familiarity with it. That being said I'll try my best to explain some of the problems you're seeing.

Looking at the steps you give it looks like you're fighting and hacking the build system rather than changing it to suit your needs.

The first thing I should point out that I did leave room in the CMake based build system for ".NET core" to be supported one day. Take a look at cmake/modules/FindDotNetToolchain.cmake. This file is responsible for detecting the ".NET" toolchain. Currently it only supports the Windows ".NET" toolchain and Mono. The fact that you were able to successfully configure with BUILD_DOTNET_BINDINGS set to ON on macOS indicates you have Mono installed.

What needs to be done here is to add support for detecting if ".NET core" is installed and also provide an option to pick which toolchain to use when both Mono and ".NET core" are available (as in your case).

the reason I'm trying to do this is because I use Z3 (through z3x86win) in an F# project, and I'm trying to migrate it from Mono to .NET Core, without any success: the Microsoft.Z3.dll in z3x86win seems to work at first through the .NET Standard shims. but then tries to pull in kernel32.dll even if given a valid native z3 dylib.)

By z3x86win I assume you mean that you're using a built release of Z3 for 32-bit x86 Windows... but you're using macOS... I don't understand why you would expect that to work.

project.json being the prerelease version of the .NET Core project file, one has to run dotnet migrate to get a .NET Core 1.x MSBuild.

This sounds like a ".NET core" specific thing. I do remember hearing about project.json files being a way of declaring projects but given that

• Z3 doesn't have this file is its repository.
• You seem to be doing some kind of migration of the project.json to the MSBuild format.

I can't really help with this. I don't understand why you would add the project.json and then immediately convert it to something else...

This MSBuild doesn't have version information---I'm not sure how to make cmake populate this, so I had to manually add it.

Looking at your build steps that can't really isn't going to work so well. You seem to be using a high level ".NET Core" build tool to try to build the .NET bindings but the CMake build system (and the previous Python build system) take a very low level approach and manually invoke the compiler directly.

Using cmake/Ninja, nothing seems to copy the build/src/api/dotnet/*.cs files to somewhere the .NET Core builder can find them, causing lots of CS0246 errors for missing native API bridging. Copying these manually worked. I seem to have got this working before, so maybe it's an issue with the build generator I'm using...?

This is deliberate. The python (old build system) made the mistake of writing generated build files into the source tree. This causes loads of problems when trying to build multiple configurations from a single source tree, so instead the CMake build system emits generated build files into the build tree and leaves the source tree untouched.

The CMake build system could be taught to copy over all the *.cs files into the build tree too. However this hasn't been necessary so far because we invoke the C# compiler directly and pass it the absolute paths to all the source files. I don't think we should make the change you're suggesting because it introduces the problem of making sure the copied files are always up to date. This can be solved but it doesn't seem like the right thing to do given that I think that using ".NET Core"'s high level build tools is the wrong thing to do here.

Presumably it is possible to invoke ".NET Core's" C# compiler directly? If so then the approach to implement support properly into Z3's build system would be

• Modify cmake/modules/FindDotNetToolchain.cmake to detect ".NET Core"
• Modify src/api/dotnet/CMakeLists.txt to invoke the ".NET Core" compiler and make any other additional changes necessary.

If it is not possible to invoke ".NET Core's" C# compiler directly or there is some huge advantage to using ".NET Core"'s high level build tools then we need to take a different approach. My guess is that it would be something like this...

• Modify cmake/modules/FindDotNetToolchain.cmake to detect ".NET Core"
• Modify src/api/dotnet/CMakeLists.txt to do the follwing when the toolchain is ".NET Core"
  • Generate our own csproj file that contains the paths to all the source files and correct version information.
  • Set the build step to invoke dotnet build and then copy the result to the right location.

I'm not keen on this approach because it means we have a completely different code path for ".NET Core".

I don't have time to work on this but if you have the time to work on it I'm happy to provide advise on the CMake side of things.

[MattWindsor91]

@delcypher: Thank you very much for the quick response, and apologies that I don't know enough about either the Z3 build system or .NET Core to offer much in the way of constructive ideas.

By z3x86win I assume you mean that you're using a built release of Z3 for 32-bit x86 Windows... but you're using macOS... I don't understand why you would expect that to work.

To be honest, this is mostly a holdover from building against mono, where this approach works all the way up to needing to provide a native Z3 library for macOS. (z3x86win is this package, for reference).

The problem in .NET Core is that there doesn't seem to be a nuget package available on macOS for Z3 (zen_z3_osx doesn't seem to contain Microsoft.Z3, or at least all of my references fail to resolve). Adding the x86 Windows version as a package gets my assembly to compile properly regardless of platform---I guess the compiler can still get the right metadata out of Microsoft.Z3.dll!---but actually trying to use the x86 Windows build runs into the probably all too expected problem of it trying to reference half of Windows. It's probably best if I abandon nuget entirely and just reference Microsoft.Z3.dll directly in future---then I can avoid things like the two versions of Z3 mismatching, etc.

I can't really help with this. I don't understand why you would add the project.json and then immediately convert it to something else...

The project.json file to which I'm referring is this one, which is in the Z3 source tree but, I guess, is probably not officially supported?

Presumably it is possible to invoke ".NET Core's" C# compiler directly? If so then the approach to implement support properly into Z3's build system would be

I can run .NET Core's Roslyn through /usr/local/share/dotnet/sdk/2.1.3/Roslyn/bincore/RunCsc (on macOS; presumably it's similar on other *nix).

It's probably best if cmake did detect and invoke the .NET Core compiler instead of having a parallel, high-level build system, especially since the code contracts fix in src/api/dotnet/core doesn't seem necessary anymore. I'm unsure what would be needed to make that work---cmake can be told to use RunCsc through the DOTNET_CSC_EXECUTABLE cmake knob, but the build then fails because it expects .NET Framework libraries such as mscorlib to be available. (I don't know much about .NET Core's inner workings, but it seems that it doesn't have a GAC, and thus gacutil doesn't exist either.)

[delcypher]

@MattWindsor91

To be honest, this is mostly a holdover from building against mono, where this approach works all the way up to needing to provide a native Z3 library for macOS. (z3x86win is this package, for reference).

Oh it's a nuget package, I was missing that context.

The project.json file to which I'm referring is this one, which is in the Z3 source tree but, I guess, is probably not officially supported?

Sorry. I completed missed that file being in Z3's source tree. @wintersteiger can tell you whether it is officially supported.

I can run .NET Core's Roslyn through /usr/local/share/dotnet/sdk/2.1.3/Roslyn/bincore/RunCsc (on macOS; presumably it's similar on other *nix).

It's probably best if cmake did detect and invoke the .NET Core compiler instead of having a parallel, high-level build system, especially since the code contracts fix in src/api/dotnet/core doesn't seem necessary anymore. I'm unsure what would be needed to make that work---cmake can be told to use RunCsc through the DOTNET_CSC_EXECUTABLE cmake knob, but the build then fails because it expects .NET Framework libraries such as mscorlib to be available. (I don't know much about .NET Core's inner workings, but it seems that it doesn't have a GAC, and thus gacutil doesn't exist either.)

It requires the changes I roughly sketched out in my previous comment. If you're interested in working on this I can sketch this out in more detail if you like.

but it seems that it doesn't have a GAC, and thus gacutil doesn't exist either.

That is for installation of .NET dlls when using mono. It isn't essential that gacutil is present but the CMake code currently emits an error if it can't be found.

[wintersteiger]

Yes, src/api/dotnet/core contains the files I use to compile .NET Core DLLs. I haven't used it in a while though and I'm sure they won't work out of the box for Core 2.0. I never integrated any of this into the Python or CMake systems, because it wasn't requested frequently (about once a year we get requests for various custom DLLs that I have to build manually anyways). It's not "officially supported", because I currently don't have the time to maintain/extend it.

Regarding the contracts, it's nice if Core 2.0 supports that, but I doubt their usefulness, so we could discuss removal.

For the CMake build, I guess it would make sense to generate a project.json file in the right directory and we can start out by simply adding a hand-crafted one in src/api/dotnet/core2 that it can copy over to the build directory.

[firelizzard18]

If you're going to build via generating a project file, don't use project.json, use <projectname>.csproj instead. Some time ago, the dotnet toolchain migrated back to an MSBuild-based system and deprecated project.json in favor of MSBuild XML project files.

Personally, I'd think it makes more sense to directly invoke Rosyln's CSC, as I would expect that to fit more nicely into your existing build system. But if it makes sense to use dotnet/msbuild, you can generate a project file that manually references everything. On the other hand, you could just use MSBuild itself, as it is a generalized build system. As far as I can tell, the dotnet build system is largely built via MSBuild targets and props files. These are installed with the .NET Core SDK. On my system, they're in C:\Program Files\dotnet\sdk\<version>\ and its subfolders.

A simple dotnet MSBuild project file:

<Project Sdk="Microsoft.Net.Sdk">

  <PropertyGroup>
    <TargetFramework>netcoreapp1.0</TargetFramework>
    <AssemblyName>Microsoft.Z3</AssemblyName>

    <!-- do not automatically include anything -->
    <EnableDefaultCompileItems>false</EnableDefaultCompileItems>
  </PropertyGroup>

  <ItemGroup>
    <!-- unnecessary if default compile items are enabled -->
    <Compile Include="src\**\*.cs" />

    <!-- explicity add generated code -->
    <Compile Include="build\src\**\*.cs" />
  </ItemGroup>

</Project>

Adding <EnableDefaultCompileItems>false</EnableDefaultCompileItems> prevents dotnet from automatically adding any source files it finds within the project directory. Thus, you can manually add exactly the files you want.

[yatli]

Hi,

May I recommend moving to a multi-targeting .csproj supporting both netstandard2.0(netcoreapp2.0 for executables) and net451:

<Project Sdk="Microsoft.Net.Sdk">

  <PropertyGroup>
    <!-- A unified nupkg supporting both platforms will be built -->
    <TargetFrameworks>netstandard2.0;net461</TargetFrameworks>
    <AssemblyName>Microsoft.Z3</AssemblyName>
    ......

We're building a compiler and trying to leverage z3 for inference tasks. Here's a cmake module file I wrote for .NET core 2.0+ integration: https://github.com/Microsoft/GraphEngine/blob/master/cmake/FindDotnet.cmake

It supports both .NET core and .NET Framework projects (we're using it for our C# and F# projects) -- you can use ADD_DOTNET, ADD_MSBUILD and RUN_DOTNET to inform cmake about how to build the projects, what nupkgs they create/depends on, configuration, etc.

For example:

ADD_DOTNET(Reisen.Core/Reisen.Core.fsproj
    PACKAGE Reisen.Core
    VERSION 0.0.1
    DEPENDS GraphEngine.Core)

ADD_DOTNET(Reisen.FFI/Reisen.FFI.csproj
    PACKAGE Reisen.FFI
    VERSION 0.0.1
    DEPENDS GraphEngine.Core Reisen.Core)

# Trinity and Reisen are our native libraries
ADD_DEPENDENCIES(BUILD_Reisen.Core Trinity Reisen)