api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration.

[yatli]

This PR updates cmake-dotnet integration and enables multi-targeting .NET package builds.
A .csproj is created during a build, and sent to dotnet command, generating a NuGet package where package metadata is properly set.

The dependency between libz3 and the nupkg is also taken into consideration. The native binary will be included into the nupkg, so that when a user references the package, the native binary is automatically imported to the process.

For x64 build, the dotnet build type is switched to Any CPU and Prefer32Bit is disabled.
For x86 build, the dotnet build type is x86.

[yatli]

Related: #1423 #1801

[yatli]

Note, mono supports netstandard2.0 and net45. It also consumes nuget packages.

[NikolajBjorner]

fantastic.

1. Andrew Helwer is creating a process for properly signed NuGet packages. There was some question about which platforms to create packages for. There was also a question whether the code contracts used in Z3's .NET code should be removed for supporting newer .NET and various platforms. I suggested to punt on it for now not having a clear idea of who would consume this.
2. Should I update the build configurations to test some of this?

[yatli]

Makes sense. I’m also interested in creating a signed xplat build—the classical sign procedure is “too manual” for a distributed and xplat build.

I’ll keep working on the build script and try to figure out the best model to incorporate binaries of different OS. I’m also wondering if we can completely switch away from GAC and use NuGet — during installation we can register a file system location as a local nuget repository (code already in FindDotnet.cmake).

The builder agent does need an update — I recommend configuring latest .NET Core SDK release (as of now v2.1). Travis should have a built-in package for that on Windows. The Linux builder would perhaps need a bootstrap script — if it runs on docker there’s also an official dotnet image.

[NikolajBjorner]

Travis builds use docker
VSTS builds are currently mainly self-hosted with a single exception where I am trying out more sustainable options. Currently Travis is broken with:

CMake Error at src/api/dotnet/CMakeLists.txt:142 (add_dotnet):

Unknown CMake command "add_dotnet".

[yatli]

ADD_DOTNET should be uppercased. I didn't know commands are case sensitive :)

[yatli]

hmm, still not working. ADD_DOTNET is not found either.
yet it does not complain about find_package(Dotnet) not found -- a system override?

update: it does not complain because I didn't tell it to. fixed (see https://travis-ci.org/Z3Prover/z3/jobs/426491671#L1035).

we need to compose dotnet from docker: https://hub.docker.com/r/microsoft/dotnet/

[NikolajBjorner]

@ahelwer: FYI
@yatli: the build failures might be because several of the Travis instances are not set up to build dot-net bindings and therefore don't have dependencies installed. The build should only generate .Net bindings when -DBUILD_DOTNET_BINDINGS=TRUE is set. Could it be that some of the failing calls are guarded by weaker checks?

[NikolajBjorner]

BTW, one commonality among the failing builds is that they also build python bindings.
Two of the succeeding builds are Linux and don't build python bindings.

[yatli]

@NikolajBjorner I checked a few failed builds, they all have this: https://travis-ci.org/Z3Prover/z3/jobs/426578219#L3544

resulting in: https://travis-ci.org/Z3Prover/z3/jobs/426578219#L3584

All of the success builds have export DOTNET_BINDINGS=0 or ADDITIONAL_Z3_OPTS+=('-DBUILD_DOTNET_BINDINGS=OFF' '-DINSTALL_DOTNET_BINDINGS=OFF')

[NikolajBjorner]

very good, I am trying to disable some ci specific code for now.
Perhaps the environment variable gets set elsewhere.

[NikolajBjorner]

sorry, haven't been able to chase dependencies here: removing these breaks other parts.

[NikolajBjorner]

The default is to build dotnet bindings and the failing builds indeed do this.
Is there an alternative to the command dotnet.exe on those platforms?
Such as https://docs.microsoft.com/en-us/dotnet/core/linux-prerequisites?tabs=netcore2x

[yatli]

That’s exactly what it’s looking for, the official .net core 2.0 sdk:) An option would be to add the official install instructions to Travis init script — I see mono is installed this way. Sorry I wrote dotnet.exe in the error message even for UNIX platforms — it’s actually looking for the dotnet executable. Yatao

…

________________________________ From: Nikolaj Bjorner <notifications@github.com> Sent: Tuesday, September 11, 2018 7:05 PM To: Z3Prover/z3 Cc: Yatao Li; Mention Subject: Re: [Z3Prover/z3] api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration. (#1815) The default is to build dotnet bindings and the failing builds indeed do this. Is there an alternative to the command dotnet.exe on those platforms? Such as https://docs.microsoft.com/en-us/dotnet/core/linux-prerequisites?tabs=netcore2x<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdocs.microsoft.com%2Fen-us%2Fdotnet%2Fcore%2Flinux-prerequisites%3Ftabs%3Dnetcore2x&data=02%7C01%7Cyatli%40microsoft.com%7C1153cf8e74c94080e63308d617d68658%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636722607476007185&sdata=Zdw82WWvIaYZm27wleah%2BQts72hkb4QVnpfh7kXVZ%2FM%3D&reserved=0> — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FZ3Prover%2Fz3%2Fpull%2F1815%23issuecomment-420235581&data=02%7C01%7Cyatli%40microsoft.com%7C1153cf8e74c94080e63308d617d68658%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636722607476007185&sdata=5xRTvprZ%2FfBs9vUS9MMprlrh3LCvL4UDJr86%2FYP9c0Q%3D&reserved=0>, or mute the thread<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FATufsMp5_UtRu4r9b-VhkOy7goPbq0Clks5uZ5kJgaJpZM4WgZq1&data=02%7C01%7Cyatli%40microsoft.com%7C1153cf8e74c94080e63308d617d68658%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636722607476007185&sdata=8Q482QeVJhWs2rw4LtQSfyKgrTohn%2B4wPz5AtexZQqE%3D&reserved=0>.

[yatli]

I just realized the CI config file is right there at the root.
Let me try to sort it out.

[yatli]

Guess I'll stop making blind shots now...

[yatli]

umm, no curl and no wget?

[yatli]

Good build says:

-- Found .NET toolchain: /usr/bin/dotnet (version 2.1.502)

Bad build says:

-- Found .NET toolchain: /usr/bin/dotnet (version 2.1.503)

investigating

update: problem repro'ed on my linux box by running the ci script manually.

[yatli]

related: https://github.com/dotnet/coreclr/issues/18157
until they have an official fix, let's manually copy Microsoft.Z3.dll to the test directory.
(after 2hrs fighting with the toolchain) okay, maybe some sed black magic also...

[yatli]

I think the CI builds are all good now. I've added logic in the test script similar to Java, so that the .NET tests for the ASAN build are disabled.

[NikolajBjorner]

Fantastic!

The python build breaks.
There is the following:

Update version numbers

def update_version():
major = VER_MAJOR
minor = VER_MINOR
build = VER_BUILD
revision = VER_REVISION
if major is None or minor is None or build is None or revision is None:
raise MKException("set_version(major, minor, build, revision) must be used before invoking update_version()")
if not ONLY_MAKEFILES:
mk_version_dot_h(major, minor, build, revision)
mk_all_assembly_infos(major, minor, build, revision)
mk_def_files()

mk_all_assembly_infos(major, minor, build, revision)

is specific to .Net, but called regarless of whether .net bindings are being built.
It seems to be in the wrong place

[NikolajBjorner]

What is odd is that the build fails in seemingly random ways.

Some builds fail with:

Traceback (most recent call last):
2019-01-16T18:19:05.7464822Z File "scripts\mk_make.py", line 16, in
2019-01-16T18:19:05.7464822Z update_version()
2019-01-16T18:19:05.7464822Z File "C:\z3-build\vsagent_work\7\s\scripts\mk_util.py", line 3060, in update_version
2019-01-16T18:19:05.7464822Z mk_all_assembly_infos(major, minor, build, revision)
2019-01-16T18:19:05.7464822Z File "C:\z3-build\vsagent_work\7\s\scripts\mk_util.py", line 3108, in mk_all_assembly_infos
2019-01-16T18:19:05.7464822Z raise MKException("Failed to find assembly template info file '%s'" % assembly_info_template)
2019-01-16T18:19:05.7464822Z mk_exception.MKException: "Failed to find assembly template info file 'src\api\dotnet\Properties\AssemblyInfo.cs.in'"
2019-01-16T18:19:05.7776214Z Content of build\master\debug:
2019-01-16T18:19:05.7776214Z Traceback (most recent call last):
2019-01-16T18:19:05.7776214Z File "scripts/win64test.py", line 27, in
2019-01-16T18:19:05.7776214Z win64test()
2019-01-16T18:19:05.7776214Z File "scripts/win64test.py", line 13, in win64test
2019-01-16T18:19:05.7776214Z util.buildz3(branch=b, everything=True, clean=True, debug=d, dotnet=True, java=True, static=False, jobs=1, clang=False, VS64=True)
2019-01-16T18:19:05.7776214Z File "C:\z3-build\vsagent_work\7\s\z3test\scripts\util.py", line 173, in buildz3
2019-01-16T18:19:05.7776214Z mk_make(branch, debug, dotnet, java, clang, static, VS64, extraflags)
2019-01-16T18:19:05.7776214Z File "C:\z3-build\vsagent_work\7\s\z3test\scripts\util.py", line 137, in mk_make
2019-01-16T18:19:05.7776214Z raise Exception("Failed to execute mk_make\n%s" % cmd)
2019-01-16T18:19:05.7776214Z Exception: Failed to execute mk_make
2019-01-16T18:19:05.7776214Z ['python', 'scripts\mk_make.py', '-b', 'build\master\debug', '-d', '--parallel=4', '-x', '--dotnet', '--java']

I could reproduce this when first pulling the merged pull request.
Then it stopped reproducing in two other tests.

Others get further,

:02.4028366Z [ 97%] Generating Microsoft.Z3.buildtimestamp, ../../../Microsoft.Z3/Microsoft.Z3.4.8.5.nupkg, ../../../Microsoft.Z3/Microsoft.Z3.4.8.5.symbols.nupkg
2019-01-16T18:34:02.4154506Z ======= Building .NET project Microsoft.Z3 [Debug AnyCPU]
2019-01-16T18:34:02.5966309Z error: Invalid input 'D:/a/1/s/build/src/api/dotnet/build/Microsoft.Z3.csproj'. The file type was not recognized.
2019-01-16T18:34:04.7077556Z NMAKE : fatal error U1077: 'echo' : return code '0x1'
2019-01-16T18:34:04.7078040Z Stop.
2019-01-16T18:34:04.7088497Z NMAKE : fatal error U1077: '"C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\BIN\amd64\nmake.exe"' : return code '0x2'
2019-01-16T18:34:04.7088647Z Stop.
2019-01-16T18:34:04.7095810Z NMAKE : fatal error U1077: '"C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\BIN\amd64\nmake.exe"' : return code '0x2'

which looks like a dotnet core / nuget installation issue.

[yatli]

I deleted the assembly info template as it's not needed for the new .NET sdk. Including it in a build will result in "duplicated assembly info" errors.

The python could leverage the new project template Microsoft.Z3.csproj.in -- it's written in a cmake-specific way but we could just simulate the behaviour by loading the file in python, and substitute the ${CMAKE_STUFF}

Edit:
Looking at the python build script there's even configure_file so it'd be easy to roll it up. I'll have a try later today -- maybe a new PR?

[yatli]

The file type was not recognized is an SDK issue -- probably there's a dotnet 1.x installation that accepts only project.json.

[NikolajBjorner]

Will try to catch up on any build machine issues during weekend, hopefully this one. Would be great to finish this. Seems like tons of work to get here.

Can you move makeallassrmblyinfo to methods in configuration objects so it is local?

[yatli]

Sure, I'll take of it.

[AdaskoTheBeAsT]

Did you had a chance to take a look at build machine if latest .net core sdk was installed there?

[NikolajBjorner]

I now see why the python build was broken.
The AssemblyInfo.in file is used in the python build even if it is redundant. This file was removed in the pull request. The offending code in mk_util.py was't part of this pull request at all.

[NikolajBjorner]

Did you had a chance to take a look at build machine if latest .net core sdk was installed there?

Pretty sure it isn't yet installed and that is the source of the other build failure. There were two classes of failures.

[NikolajBjorner]

At this point all main changes from this pull request are integrated and build machines are underway.
The VS2013 build still fails with

MSBUILD : error MSB1001: Unknown switch.
Switch: --no-restore

The flag is used in cmake\modules\FindDotnet.cmake
Maybe related to version of dotnet.exe that comes with hosted builds: 1.0.4\x64\dotnet.exe

[AdaskoTheBeAsT]

it can be - --no-restore switch was added in .net core 2.0

[NikolajBjorner]

right, need to figure out what revision to specify in hosted build. 2.2.213 is broken.

[AdaskoTheBeAsT]

I see - shouldn't be 2.1.502? Travis .net core

[NikolajBjorner]

2.1.300 so far seems to do fine

[yatli]

I’m getting hands-on the python side. Will submit a new PR when I make progress. Yatao

…

________________________________ From: Nikolaj Bjorner <notifications@github.com> Sent: Monday, January 21, 2019 6:00 AM To: Z3Prover/z3 Cc: Yatao Li; Mention Subject: Re: [Z3Prover/z3] api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration. (#1815) 2.1.300 so far seems to do fine — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FZ3Prover%2Fz3%2Fpull%2F1815%23issuecomment-455906563&data=02%7C01%7Cyatli%40microsoft.com%7C832ab8c0feed4cab206708d67f22bf95%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636836184554136668&sdata=E33XI3hPBvEMlYqmqfpgdjuA1gw1rQbdoILJVcNajHI%3D&reserved=0>, or mute the thread<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FATufsPzGdnHHkEpZ-Y14igtCbk-xYpWrks5vFOcVgaJpZM4WgZq1&data=02%7C01%7Cyatli%40microsoft.com%7C832ab8c0feed4cab206708d67f22bf95%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636836184554136668&sdata=wET70wrLmzpcuIbKb1iztTr9v7GVipW1H5%2BGdGayStc%3D&reserved=0>.

[NikolajBjorner]

note that your original PR is now integrated. Thanks!!!

There are some differences between the python and cmake.
I am not sure whether these are critical to address for usability:

• the python still has an option non-dotnet core generation. Perhaps time to delete this. It could break our own build machines, so another weekend to fix. At some point I will delete it.
• the python scripts directly integrate template files instead of using nicer template files with replacement. They do take care of some important features, such as signing with EPRC (or is it ERPC or whatever).
• platform 1.7 vs other target versions.

[NikolajBjorner]

The mac build seems not working.

I set up a pipeline last week and the cmake version with Mac is failing:
https://z3build.visualstudio.com/Z3Build/_build/results?buildId=1017

Note that the Travis-CI build with Mac doesn't build dotnet bindings.

[yatli]

just to confirm, "MacOS build with CMake", right?

edit: looks like a nuget source registry issue. the local source is not picked up.
edit: the problem is about sed in macOS having different switches:

-- Registering NuGet local repository 'Microsoft Z3 Local Repository' at '/Users/vsts/agent/2.152.1/work/1/s/build'.
sed: 1: "/Users/vsts/.nuget/NuGe ...": invalid command code v
sed: 1: "/Users/vsts/.nuget/NuGe ...": invalid command code v

[NikolajBjorner]

confirmed.
yes, seems so too

[yatli]

this is the relevant context, in FindDotnet.cmake:

z3/cmake/modules/FindDotnet.cmake

Lines 161 to 162 in ab98837

	EXECUTE_PROCESS(COMMAND sed -i "/${repo_name}/d" "${nuget_config}")
	EXECUTE_PROCESS(COMMAND sed -i "s#</packageSources># <add key=\\\"${repo_name}\\\" value=\\\"${repo_path}\\\" />\\n </packageSources>#g" "${nuget_config}")

From the log, sed misinterprets "/Users/vsts..." as commands U and v.
Ok it comes back to my mind. I was using '#' as the separator -- it should automatically override the default command separator '/'.

The first sed invocation did not use this trick.

[yatli]

I'm not on my dev box, @NikolajBjorner could you please try modify the first command to:

 EXECUTE_PROCESS(COMMAND sed -i "#${repo_name}#d" "${nuget_config}")