Making the CMake build system a first class citizen #986
Comments
|
This is super. I would prefer to deprecate the python based build as soon as it is redundant. Maintaining two systems is not a path forward, and the python system has its limitations. My only issue with cmake/ninja is that i dont get good debug symbols for the vs profiler. Haven't dug into why, probably the warning that it can't find vc140.pdb during linking is a big clue. |
|
@NikolajBjorner Thanks for your support. Regarding the issue you've observed. Could you create an issue detailing reproduction steps (e.g. MSVC/Visual Studio version, CMake version, build type) and I'll take a look? Broken debug info is definitely a blocker and that needs to be fixed. |
|
For starters, I get these kind of warnings (RelWithDebInfo) on my various machines. api_log_macros.cpp.obj : warning LNK4099: PDB 'vc140.pdb' was not found with 'api_log_macros.cpp.obj' or at 'C:\z3\build\vc140.pdb'; linking object as if no debug info I am not sure where "vc140.pdb" gets pinned by the build system and where I would fetch it from. About repros |
|
@NikolajBjorner Thanks for the detailed info. Am I right in thinking that MSVC 19.00 corresponds to Visual Studio 2015? Also does this problem happen when you use Visual Studio as the CMake generator (instead of Ninja)? I'm not very familiar with the MSVC toolchain so I'm not sure how well things are supposed to work when you build a binary outside of Visual Studio but then try to profile it using Visual Studio. |
@NikolajBjorner I just noticed you're doing a 32-bit build (x86) rather than a 64-bit (x64) build. Is that intentional? So far I've not been able to reproduce this but I was using |
|
@NikolajBjorner Moving this discussion to #990 |
|
@NikolajBjorner @wintersteiger Personally I'd like to do moving the CMake files into their correct location (i.e move files out of I wanted to check with you before I create a PR to do this though because it created some controversy last time I proposed this. |
|
It would deprecate a conceptual contribution from @agurfinkel to the master branch (still anticipating in suspense the Spacer pull request). |
Spacer pull request? Could you elaborate on that? |
|
@NikolajBjorner this would not impede me in any way. |
|
Re continuous integration: sure, go ahead if you have time to do that! I think Travis now also supports OSX so it makes sense to set something up there. We currently have two CI toolchains, one for the nightly binaries (running on local VMs on a mac mini in my office) and one for the per-commit-batch CI runs (running on Azure VMs). The latter is basically a failed experiment, because VSTS/visualstudio.com just doesn't provide the features we need and it's a pain to work with. On top of that, maintaining all of that takes way too much of time, so I'd be happy for external contributors to take over some or all of this. We don't really have an agreed upon budget for any of this, but I'm sure we could contribute some Azure VMs if needed. |
|
I may have some time next week to start looking at this. I have quite a bit of experience using TravisCI so that's probably the solution I'll go with. The way I've done this in the past though is to have the build logic in separate shell scripts so that their functionality can be repurposed to other situations (e.g. building locally, building in a Docker container). Then I just have Travis simply call the build script with the appropriate environment variables set. One nice thing we can get out of doing this is have ASan and UBSan builds which will detect problems running the simple tests and API examples. We'll likely need a suppression file for UBSan though due to #964 . |
|
@wintersteiger @NikolajBjorner So I don't think I'm going to have time to implement CI this week but something we need to think about is how much of Z3's configuration space we should cover and test. Here are the configuration parameters I can think of
As you can see the configuration space is rather large. There is a trade-off between configuration coverage and the time it will take to run the configuration. I would prefer to keep the number of configurations we test small so that we get the build results for PRs as fast as possible. This means I will have to pick a subset of the above configuration space.
|
|
Of course this is dependent on the host machine but are these tests very resource intensive? Do they take hours to run or can they complete in a few minutes? |
|
These are fairly quick. A couple of minutes at most. |
While I am in favour of removing the old build system I worry that doing this too abruptly will adversely affect Z3's users. My recommendation would be to announce the old build system's deprecation in Z3's release notes when the next stable release is made. That way the deprecation is properly announced (most Z3 users probably don't read Z3's issue tracker and therefore don't know about the planned deprecation) and users have ample time to migrate. This of course assumes that a new release of Z3 is fairly imminent. So until the old build system is actually deprecated I think it would be wise to test at least one configuration of the old build system given that people are still relying on it. |
|
We currently run z3test/scripts/smalltest.py on Linux (Ubuntu 14.04 x86, Ubuntu 14.04 x64, Debian 8.5 x64), OSX 10.11, and z3test/scripts/win(32|64)test.py on Windows and those VMs produce the nightly binaries as well (via z3/scripts/mk_*_dist,py). The build scripts that trigger all this are in z3test/build. I don't think we need more configurations than the ones we have now, at least not right away. I have recently removed the FreeBSD build (and nobody complained) and I think we could also remove Debian (if their packages don't use our nightly binaries, but I don't think they do). I'd like to keep Linux x86 + x64 and Windows x86 + x64. The number of users of the x86 configurations is decreasing, but for now I think we should keep them. The CI builds use different VMs of the same OSs, except Ubuntu 14.04 x64 runs 16.04. These use the same scripts but are triggered by visualstudio.com build definitions. |
|
@wintersteiger @NikolajBjorner I have a first proto-type ready for you both to take a look at You can find my fork at https://github.com/delcypher/z3/tree/travis_ci_proto_type You can see some example builds at https://travis-ci.org/delcypher/z3/builds/247161333 You can click on any of the configurations and see the build log. Here is a rough tour of how it works
Some additional notes
The parts that need special attention from you both are
Do these scripts do everything you want them to do? Do you have any other feedback regarding this proto-type? |
|
Pretty awesome.
According to win32test we do: The real important directory is regressions/smt2.
|
|
The python doctests are currently broken. There is a script that is supposed to run them (src/api/python/z3test.py), but it doesn't work in many environments, it just returns "ok" without actually running anything. I haven't figured out whether they actually run or don't run during the CI and if so on which platforms. The root of the problem is the relative import of modules, which apparently fails silently in some versions of Python. |
That script does run in the Travis tests I link to. The problem is that the build produces such a large log that it gets truncated. If you scroll to the bottom of https://travis-ci.org/delcypher/z3/jobs/247161334 you'll see a note about it being truncated, telling you that you need to look at the raw log. This is a problem I've encountered before using TravisCI. The trick I've used in the past is to hide the output of some tasks by writing it to a log file and then dumping the log file to the console iff the command fails
The script does this
The script doesn't do this but could
The script doesn't do this. Last time I tried it, it failed but that might be because
The script does I think these are the same thing.
The script doesn't run this. My reasoning was that the scripts probably expect the old build system and Windows. I haven't tried it though. |
Thanks I didn't even know about that script and therefore my proto-type makes no attempts to run it. |
Yes Doxygen in the builds are enabled just to make sure the build succeeds. The result gets thrown away after the build. It would certainly nice to upload the result of the build somewhere. However because the CMake build system does not know how to build the OCaml bindings no documentation for those bindings gets generated right now. TravisCI does allow build artifacts to be uploaded so this is something we could add in the future. |
|
Another thing to note is that the 32-bit build configurations I have in the proto-type don't work :( The main reason is that the even though I've used a multilib gcc (version of GCC that supports building 32-bit code) I don't have 32-bit versions of python/mono/java (etc...) installed so the 64-bit python/mono/java can't load the 32-bit One solution is to simply not test the python/.NET/java APIs in this configuration. Another (which is more complicated) is to tell docker to use a base image that is 32-bit which will therefore give us 32-bit builds of everything. The problem with this approach is there aren't any official 32-bit ubuntu docker images so we'd have to maintain our own image for this purpose. There are plenty of unofficial images though (e.g. https://hub.docker.com/r/delcypher/ubuntu32/ ) |
|
I've made some more progress on this
What's missing?
I think what I have now is good enough that we can start using it alongside the existing CI infrastructure. Most of the missing features are going to be quite time consuming to add so I'd like to add them at a later date. If you're agree then
|
|
Pretty awesome. Hope it gets operational in time your attention gets taken elsewhere. The current C# tests may as well be ignored. There are 4 trivial tests so not worth spending time on porting. The examples from the z3 repository also test API capabilities in disguise of being examples. These are much more useful. I noticed a bunch of warning messages in the gcc build. I will be looking at them at later at some point. Good to have diverse targets. |
There are getting started instructions here TravisCI is free to use for open source projects. However if you want more concurrent jobs there might be an option to pay for it. I'm not sure about this though. I'll open a PR soon with the build scripts. I'm currently testing 32-bit Ubuntu builds and I want to make sure this works before submitting.
Once those warnings are fixed it might be useful to treat particular warnings as errors so that they don't get reintroduced. |
|
PR opened: #1126 |
|
I just remembered that the /linkresource flag for the .NET API triggered some problems in the past. Did those issues get resolved? |
|
@wintersteiger Yes that flags caused issues so I simply don't pass it. There is a comment in the CMake build system explaining the situations. z3/src/api/dotnet/CMakeLists.txt Lines 150 to 154 in 97e2632 Basically the problem was the |
|
@delcypher Yes, it may well require a relative path. For releases and nightly binaries we will need that set though, .NET users rely on that to keep the right version of libz3.dll. Doesn't CMake have facilities for converting absolut to relative? |
Perhaps. I don't remember if I tried relative but I suspect it won't work. The documentation for /linkresource says it is a file name, not a path. This bizarre restriction for the z3/src/api/dotnet/CMakeLists.txt Lines 206 to 212 in 97e2632 means I can't make this work in the multi-configuration generator case (e.g. Visual Studio/Xcode). In the single configuration generator case (e.g.
It does but that isn't the problem here. |
|
Yes, we'll need that if we want to publish the binaries produced via CMake are going to be published. Usually the two files are always in the same directory anyways and we won't add any new APIs that require this, so hardcoding some of the strings/paths etc shouldn't be a major issue. |
when doing single configuration builds. Under multi-configuration builds this won't work so we just emit a warning and don't pass the flag. This implements a requested made by @wintersteiger in Z3Prover#986 (comment) . WARNING: This has NOT BEEN TESTED.
when doing single configuration builds. Under multi-configuration builds this won't work so we just emit a warning and don't pass the flag. This implements a requested made by @wintersteiger in Z3Prover#986 (comment) . WARNING: This has NOT BEEN TESTED.
|
I'm packaging 4.6.0 release for FreeBSD. Should I build Z3 using CMake, or keep using old python machinery? |
|
@arrowd: Whatever you prefer. Note that our release packages have signed .NET libraries, signed by our private key, so if you want us to publish a release package, we'll have to build that ourselves, or possibly delay-sign them. I removed FreeBSD Ci/nightly/release last year because it had very few downloads, so few that it's fair to say "nobody" wants them. |
|
@delcypher: The Visual Studio backend of cmake produces a solution and project files that aren't usable. They overwhelm VS with a lot of tiny sub-projects. So much so, that it literally takes minutes before it can start a build. Further, all those little sub-projects have their own compilation settings, so if we need to change a compiler option, we have to either click millions of times, or hack the project files outside of VS. The philosophy in VS is a bit different; usually there would be one sub-project for each product, i.e. libz3.dll, z3.exe, c_example, etc, instead of projects that produce static libraries and sub-modules can be within folders or project filters (see currently used .vcxproj files). VS does it's own dependency analysis and incremental compilation features. How much effort is it to teach cmake to do that? |
I noticed the slowness before. I was running Visual Studio in a VM and assumed it was slow because of the VM. When I used it, it was spending most of its time doing the initial indexing I think. It was fine once indexing was complete and Z3 built (and re-built) fine for me. Are you sure that the number of projects here is the bottleneck? So I'd expect there to be ~76 projects, which doesn't seem that large. Does Visual Studio really not scale well to that number of projects?
Err yeah, you shouldn't do that. If you need to change a compiler option you do that at the CMake level. Not the Visual Studio level. When you change the CMake build system the Visual studio solution and projects will get regenerated. This is the price you pay when you use a meta build system like CMake. Similarly when you use CMake's Makefile backend you don't modify the generated Makefile when you want to change build flags, instead you modify the CMakeLists.txt files or you edit the CMake cache (using
I believe the reason CMake is doing this is because each component is treated as a CMake "object library". CMake "object libraries" act like libraries in CMake's language but they don't get linked, only the object files get built. Then the I don't think there's any easy way to fix because I think it might require re-architecting the CMake build. The build is structured the way it is right now because I was trying to make it as similar as possible to the python build system so that they could co-exist easily. All that being said I really am not an expert on the interaction between Visual Studio and CMake because I don't use it very often. If it's merely a presentation issue there are ways to reorganise how projects are present in Visual Studio from within CMake https://cmake.org/cmake/help/v3.8/command/source_group.html If it's more than just a presentation issue then we need to think about how to best fix this. Given that Microsoft's Visual Studio team has recently put a lot of effort into improving the CMake experience in Visual Studio and your connections to Microsoft perhaps it would be good to get in contact with them to see if they can help? |
|
@delcypher do you need help for the OCaml API? I don't know much about Cmake, but I know about OCaml… |
|
@c-cube. It would be great if you can help out on the ocaml part if you are also using it. |
|
Shouldn't be this closed now? Seems everything requested was implemented already. |
|
The build process for ocaml is based on the python systems. This was not ported. |
Since the CMake build system in #461 I've been slowly implementing additional feature to make it on par with the original Python/Makefile based build system.
The following features are missing (but are being actively worked on)
API_LOG_SYNCthat corresponds to the #1037).FOCI2 support. Waiting for response in Is FOCI2 dead? #1032EDIT: FOCI2 was deprecated and has been removed..cppsource files ([CMake] Regeneration of some.cppfiles are broken #1030) (Implemented in PR [WIP][CMake] Fix broken regeneration of some .cpp files #1094)Since we are very close to having feature parity and the build system has been in place for over a year (and thus we've had plenty of time for people to try it) I thought it might be a good time to re-evaluate the position of the build system within the project. I also hear that Visual Studio 2017 is supposed to have substantially better CMake integration which is a nice bonus for Visual Studio users.
Right now the build system isn't really a "first class citizen" because it lives in
contrib/and is not tested by CI. I'd like to change this so (resources permitting) I'd like to seecontrib/to where CMake expects them to live. This isn't essential but it would be a nice change because I find myself frequently shooting myself in the foot when I forget to run thecontrib/cmake/boostrap.pyscript. EDIT: Done in [CMake] Move CMake files into their intended location #1070 and is now mergedNote I am not suggesting removing or deprecating the original Python/Makefile. Although that is what I'd like to see happen eventually this is not my decision to make. If this is the route we want to go down a first step would be to set up extensive testing (as I'm suggesting above) so that any problems with the CMake build system can be fixed before deprecating the old build system.
Thoughts?
The text was updated successfully, but these errors were encountered: