Skip to content
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

Disable MIRI check until it runs cleanly on CI #360

Merged
merged 1 commit into from May 26, 2021

Conversation

alamb
Copy link
Contributor

@alamb alamb commented May 25, 2021

Which issue does this PR close?

Related to #345 (but doesn't fix the underlying issue)

Rationale for this change

The MIRI checks enabled in #323 have been failing frequently with false positives on PRs and master. Until they run cleanly and only fail when there are actual problems, running these CI checks on all PRs is slowing everyone down and causing confusion,

What changes are included in this PR?

  1. Disable MIRI check on CI

I disabled the whole thing this time, whereas prior to #323 they "ran" but the results were not checked. That seems like a waste of CPU time / github actions credits to me.

Are there any user-facing changes?

Hopefully contributors' PRs will stop getting failing checks

@alamb
Copy link
Contributor Author

alamb commented May 25, 2021

cc @roee88 @vertexclique

Copy link
Member

@jorgecarleitao jorgecarleitao left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree that the checks are not being helpful: we know that it is an issue, and IMO we should just track this separately until it is fixed, instead of having the run not doing anything useful to us.

Copy link
Contributor

@nevi-me nevi-me left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, i agree with Jorge's comment

@jorgecarleitao jorgecarleitao merged commit 74d5957 into apache:master May 26, 2021
@alamb
Copy link
Contributor Author

alamb commented May 26, 2021

I think @roee88 has found the root cause: #345 (comment) 👍

@alamb alamb mentioned this pull request Jun 7, 2021
@alamb alamb deleted the alamb/disable_miri branch June 15, 2021 11:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants