Learn and contribute back to Boogie by setting up CI for Windows #101
Comments
|
Hi there, |
|
Having a Windows build in Travis CI would be good, I guess. However, I want to note that the Linux build is not running anymore for quite some time now. When I go to https://travis-ci.org/boogie-org/boogie, I get:
|
|
I was not aware of the newly added Windows support on Travis CI. If possible, I also prefer TravisCI to VSTS as the workflow to make a pull request is much clearer. I can definitely look into that. To enable Linux build on Travis-CI again requires ownership of this repository or administrator permission in the organization AFAIK, so I might not be able to help. |
hc825b
changed the title
|
Hi Chiao Hsieh, I'd be curious to know how you got on with this. Incidentally, we have a Windows build of Boogie running on a different CI platform (Jenkins). Until recently, this has worked quite well, but the current test results from Boogie are inconsistent between our build and the Travis Linux one. Debugging them is also hard because compilation on Windows and testing are both somewhat difficult to get working on a given machine. It would be great to find a more-cross-platform-friendly solution, IMO; I wonder if you ran into similar issues? Cheers, Alex |
|
FYI, I think it would be worthwhile to take a look into the recently released GitHub Actions functionality. It seems that it supports CI for Linux, Windows, and MacOS. I still haven't tried it, but my students did set it up for some of our other projects (Linux builds only) and it was pretty straightforward. |
|
Hi Alex (@alexanderjsummers), Sorry for the very late response! I've tried using the Windows support in Travis CI as suggested by others. IMHO, Windows support in Travis CI is still not mature enough as of now, and my result is not quite desirable. The Windows support in Travis CI is based on Chocolatey package management system to install required dependencies, and I stumbled on problems to find the path to tools installed by Chocolatey such as MS Build and Python 3 and to config the environment variable correctly. My last attempt about three months ago seems to compile Boogie successfully according to the log on Travis CI, but I could not run the unit tests or If interested in more details, you can found latest commits in Chiao |
|
@hc825b This is a great effort. Are you interested in trying to wrap this up? I looked at your Travis log. It seems that it cannot find I would guess you next step should be to try to figure out how to install |
|
Actually, |
|
@zvonimir That is precisely where I stumbled and decided to stop working on it. If you take a closer look at line 27 in my Another possible root cause is that Z3 is not properly installed. |
|
I see. Try to print some additional info to aid with debugging. For example, maybe Also: On my machine this folder has to be in the path variable for lit to work: |
|
I am able to run @zvonimir: To answer your question on wrapping this up, I'd say I couldn't/shouldn't spend more time on this. Although I'd really like to see this finished and integrated, it is simply that my work is no longer related to Boogie. If your students can take over, I'll be happy to answer their questions or provide some little help. |
|
Hi Chiao and Zvonimir, Thanks for the updates and interesting discussion! We also observe many inconsistent test outputs on our Jenkins server (we are at least running the tests the right way these days, but still haven't seen the expected outputs for all tests). I spoke with @RustanLeino a few weeks ago about how to fix these up to be less brittle, but I'm afraid I haven't had the time to try it yet. I think it's likely that you're seeing the same issues. Could you perhaps send me the list of test failures that you get, please? That'd be helpful for when I finally get to this (unfortunately likely to be in about a month because of teaching commitments...). Best wishes, |
|
We might be able to use OutputCheck to achieve this, and the README in the test folder recommends: https://github.com/stp/OutputCheck/blob/master/README.md |
Hi Alex, Details can be found in my Travis build logs at https://travis-ci.org/github/hc825b/boogie Below should be the names of the tests with unexpected results. |
|
Hi, I am also interested in getting the Boogie tests to work on Windows. I am part of the Viper team and we test many of our tools on Windows and since we rely on Boogie it would be great if we could get this working. I am happy to help. @hc825b , thanks for your test output. You seem to be using Z3 4.5.5, which is quite an old version (except I misinterpreted the build output). That may be one reason why you have so many unexpected failures, but not sure. In particular, Boogie is not compatible with older Z3 versions, since command line inputs for Z3 have changed etc... On our Windows Jenkins build (using Boogie commit 327fcfd and Z3 4.8.8), we only have 9 unexpected failures, namely for these files: functiondefine/fundef.bpl I looked into the reasons. There are three issues (as already hinted at by @alexanderjsummers).
where grep is used (i.e., // RUN: grep define "%t1" > "%t2")
livevars/bla1.bpl
test15/IntInModel.bpl I would really like to get all tests running on Windows. One potential solution that I see right now is to somehow mark all the tests that are "brittle", i.e., which check for an execution trace or a model. Then at least on Windows we could ignore those tests. Would the Boogie developers accept a change along these lines, if I were to identify the brittle tests? For the tests that use grep, it would be nice if we could find alternatives. In the long run, the ideal solution would be to make these checks less brittle, which will take more work though. |
|
I just ran all tests on a Windows setup (Windows 10, Boogie 2.6.15, Z3 4.8.8) and all tests except the three in @gauravpartha @alexanderjsummers: I think the problem on your end is that you are still using the obsolete Boogie build. The "official" build now uses .NET Core, and all expected outputs were updated to match this build. I agree that there are some annoying tests that need to be updated a lot because Z3 updates or even small updates in Boogie change the produced model / error trace. It would be great to find a better solution for that. However, at least in my experience, the same Boogie/Z3 combination usually behaves the same across different operating systems. @zvonimir: Could you check if the |
|
@bkragl This is really weird since I did this work on Windows using .NET Core and Z3 4.8.8. Which seems to be the same setup you are using. How are they failing? Could you provide more details? Is it just because of Everyone, I already suggested above the solution for how to handle these "annoying" tests: #101 (comment) |
Yes, it's because of Are you using Cygwin or some other POSIX environment? If I run inside Cygwin (where |
@bkragl Thanks a lot for the pointer. We are using msbuild and not .NET Core. I'll try to update that and hopefully then only the three "grep" tests will fail. @zvonimir Thanks a lot for the pointer to OutputCheck. It's not clear to me yet how well one can check the key parts if, for example, the counterexamples produced are completely different. I agree that if it's possible that would be a good solution and that's what one should try first. Hopefully once I update the way we build Boogie to .NET core, there won't be any Z3 discrepancies. |
|
I was able to successfully run the tests on our Windows Jenkins server using .NET Core and all the tests pass. Thanks a lot for the support!! GitVersionTask was giving me trouble at first and I couldn't solve it by setting the environment variable Currently, the documentation for running the driver tests (https://github.com/boogie-org/boogie/blob/master/Test/README.md) provides the If you think this is a good idea, I could add a pull request. Thanks again. |
Great to hear that the test run successfully now!
In my opinion, by now we can drop |
I agree. Making |
|
Can we close this issue now? |
Sure, I will close the issue. Feel free to reopen/rename the issue if needed. |
Hi Boogie team,
I'm a PhD student in CS UIUC, and I'm self-learning and using Dafny and Boogie for my research now. I noticed that the CI for Windows is missing, so I am thinking to set up Microsoft VSTS CI as I have some experience with VSTS.
I've set up a showcase using my own fork at https://github.com/hc825b/boogie
You can check the build logs publicly available on https://boogie-org.visualstudio.com/boogie/_build?definitionId=1
Right now it only compiles
Source/Boogie.slnand run unit tests with VS2017. I'll continue on driver tests.I'd like some opinions from you guys to see if this is something helpful, and also discuss how I can make a "pull request" since how I configured VSTS is not reflected on the code I added.
Thanks!
Chiao Hsieh
The text was updated successfully, but these errors were encountered: