chore: Run single-platform integration tests even if nightly build failed #2369
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
I think conserving resources for the people working on fixing the deep test issue is actually a good idea. Regarding the technical, I believe that this should work. |
fabiomadge
reviewed
Jul 6, 2022
| @@ -53,13 +53,12 @@ jobs: | |||
| run: dotnet pack --no-build dafny/Source/Dafny.sln | |||
|
|
|||
| check-deep-tests: | |||
| if: ${{ !contains(github.event.pull_request.labels.*.name, 'run-deep-tests') }} | |||
There was a problem hiding this comment.
Suggested change
| if: ${{ !contains(github.event.pull_request.labels.*.name, 'run-deep-tests') }} | |
| if: !contains(github.event.pull_request.labels.*.name, 'run-deep-tests') |
There was a problem hiding this comment.
Nope, that's what I tried first, but then the value looks like a YAML tagged value: https://yaml.org/spec/1.2.2/#691-node-tags :)
There was a problem hiding this comment.
It worked before and the docs also claim so.
There was a problem hiding this comment.
Are you sure, that the initial problem weren't the unmatched parentheses?
There was a problem hiding this comment.
My bad, I just tried it. 😞
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There's no good reason to not run the integration tests in this situation: the results can still help tell you if your PR is in good shape while the nightly build gets fixed.
Our previous attempt to fix this didn't work because if
check-deep-testsfailed, theintegration-testsjob was skipped no matter what it'sifclause evaluated to. Instead this change removes theneeddependency entirely. All jobs still have to pass to unblock the PR anyway.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.