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

Allow specifying the Rust toolchain to use #56

Open
joshlf opened this issue Feb 7, 2024 · 2 comments
Open

Allow specifying the Rust toolchain to use #56

joshlf opened this issue Feb 7, 2024 · 2 comments

Comments

@joshlf
Copy link

joshlf commented Feb 7, 2024

In a recent zerocopy PR, we had to stop testing our nightly-only features under Kani. The reason is that those features were recently updated to work with a more recent version of the nightly Rust toolchain, and so are now incompatible with older nightlies. Since the Kani GH action selects its own toolchain, it makes that action incompatible with our nightly-only features. At the moment, we don't use Kani to test any of those features, so we simply disabled those features when using Kani. In the future, though, this could become a problem for us if we want to use Kani to test nightly-only features.

It would be great if the Kani GH action allowed specifying which Rust toolchain to use.

Here's the code in question from our Kani GH action invocation in CI:

          # Use `--features __internal_use_only_features_that_work_on_stable`
          # because the Kani GitHub Action uses its own pinned nightly
          # toolchain. Sometimes, we make changes to our nightly features for
          # more recent toolchains, and so our nightly features become
          # incompatible with the toolchain that Kani uses. By only testing
          # stable features, we ensure that this doesn't cause problems in CI.
          args: "--package zerocopy --features __internal_use_only_features_that_work_on_stable --output-format=terse --randomize-layout --memory-safety-checks --overflow-checks --undefined-function-checks --unwinding-checks"
@celinval
Copy link
Contributor

celinval commented Feb 8, 2024

Hi @joshlf, unfortunately, Kani relies on a specific version of the rust toolchain, and this cannot be changed today. We try to keep Kani as up-to-date as possible, but some changes to the Rust compiler can break Kani's compiler, and requires us to spend time ensuring we address them correctly.

We have been working with the Rust compiler team to introduce stable APIs to the compiler that would allow us to break this strict requirement. Until then, unfortunately, this issue will be blocked.

@joshlf
Copy link
Author

joshlf commented Feb 9, 2024

Okay, thanks for the context! Not a big deal for us to work around it as we're currently doing. Feel free to close if you'd prefer not to leave this open :)

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

No branches or pull requests

2 participants