Do not run performance benchmarks for tags #2745
Merged
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.
Description of changes:
Currently, the performance benchmarks also run when pushing
kani-*
tags, which is essentially done each time we're going to publish a new release. In that case, the performance CI job fails with the error:There's at least two occasions in which I've seen this happen:
kani-0.35.0
tag: https://github.com/model-checking/kani/actions/runs/5957239259/job/16159564100kani-0.36.0
tag: https://github.com/model-checking/kani/actions/runs/6110889802/job/16585358347It doesn't make sense to run performance benchmarks in this case, since the candidate commit will have already triggered a performance benchmarks CI job when it's merged into
main
.Resolved issues:
Resolves #2744
Testing:
How is this change tested? N/A (changes to GA workflows cannot be tested)
Is this a refactor change? No.
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.