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

Add two new CI workflows to check Kani against verify-rust-std #3386

Merged
merged 6 commits into from
Jul 26, 2024

Conversation

celinval
Copy link
Contributor

@celinval celinval commented Jul 25, 2024

This PR adds the following workflows:

  1. verify-std-check: This workflow will run either in a PR or via workflow call. It pulls the main branch of verify-rust-std repository, and see if it can verify the repo with the new Kani version from HEAD.
    • If verification succeeds, the workflow will succeed.
    • If the verification fails and this is a PR, the workflow will compare the verification result against the base of the PR. The workflow will succeed if the results match*.
  2. verify-std-update: This workflow will run the verify-std-check workflow. If it succeeds, it will update the verify-rust-std branch from HEAD. This workflow will fail if features/verify-rust-std branch diverges, and a merge is required.

The motivation for this PR is to help us identify any changes to Kani that may break the Rust verification repository, and to keep the verify-rust-std up to date as much as possible.

  • The fallback logic is needed since toolchain upgrades can potentially break the std verification. This will happen in cases where the new toolchain version is incompatible with the library version from the verify-rust-std. Those cases should not interfere with Kani development, and they should be fixed when we update the verify-rust-std repo.

Call-out

Here is an example of a verify-std-check run: https://github.com/celinval/kani-dev/actions/runs/10101499265.
Here is an example of a verify-std-update run: https://github.com/celinval/kani-dev/actions/runs/10101909177.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@celinval celinval requested a review from a team as a code owner July 25, 2024 21:20
Copy link
Contributor

@jaisnan jaisnan left a comment

Choose a reason for hiding this comment

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

I am approving under the assumption that should the workflow to update features/verify-rust-std on its own fail, we will modify it again to not push directly.

Is that a correct assumption?

@celinval celinval merged commit 70bd021 into model-checking:main Jul 26, 2024
27 checks passed
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.

2 participants