-
Notifications
You must be signed in to change notification settings - Fork 13
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Fix solver versions #180
Fix solver versions #180
Conversation
b1f764f
to
8fc3707
Compare
42f3382
to
43a6bda
Compare
43a6bda
to
b838956
Compare
24c7a05
to
0534afc
Compare
0534afc
to
5d0467a
Compare
This was previously mis-identified because the Z3 4.8.11 test configuration was accidentally using Z3 4.8.10.
a6de8a7
to
414e053
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for working on this Kevin. I think it's a great step in the right direction. My only concern is the operational one where we are sometimes running into rate-limiting for the build servers. I don't know what the right approach to that is. Maybe only run the full matrix daily rather than on every commit?
@kquick, is there any reason not to merge this while we continue to consider better ways to specify the matrix? |
Generally no. I don't think the JSON approach is too difficult though, I just hadn't had any time to work on this. Since there's a conflict though I'll sign up to resolve the conflict and add the JSON approach by next Monday (if you wanted to merge before then please feel free to). |
No urgency here, I just didn't want this to bitrot. |
b750378
to
ebd703c
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fantastic! I'm much happier with the way the CI matrix is handled now. I've left some minor suggestions/questions on the .pl
script.
@robdockins I think this is ready for a final review now. |
This latest version that uses the generated matrix is more efficient (it will vary multiple solvers in a single run since the tests are independent for each). I haven't seen any rate limiting issues in this more recent configuration, but I think the new generator will give us the ability to add customization over time of day or other parameters in the future if needed. |
Runs tests using various fixed versions of the supported solvers.
This now runs all tests against specific revisions of solvers, and will let us expand the set of revisions in the future as needed. For many of the solvers, this also establishes a "lower limit" to the supported version; if it was important to show support for earlier versions of any of these solvers we could do so, but it would mean additional controls over which tests were run, and so that didn't seem worth it at the present time unless specific needs can be identified.
Overall, this will help us maintain a compatibility matrix and also identify any regressions that occur in the future.