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 the ability for Kani to use a locally installed toolchain at runtime #3058

Closed
jaisnan opened this issue Mar 5, 2024 · 0 comments · Fixed by #3056
Closed

Add the ability for Kani to use a locally installed toolchain at runtime #3058

jaisnan opened this issue Mar 5, 2024 · 0 comments · Fixed by #3056
Assignees
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.

Comments

@jaisnan
Copy link
Contributor

jaisnan commented Mar 5, 2024

In order to use GPG verified toolchain components, Kani needs to be able to use locally installed toolchains.
These toolchains are typically fetched from the rust-lang server and then, verified with the associated .asc file.

Kani's setup currently depends on rustup to install the toolchain, which doesn't allow us to use verified components. This also means having rustup itself as a dependency.

Being able to do this, will also enable us to remove rustup as a runtime dependency.

@jaisnan jaisnan added the [C] Feature / Enhancement A new feature request or enhancement to an existing feature. label Mar 5, 2024
@jaisnan jaisnan self-assigned this Mar 5, 2024
jaisnan added a commit that referenced this issue Mar 7, 2024
Adds `--use-local-toolchain` to Kani's setup flow, which accepts a local
toolchain and then uses that to finish the Kani setup.

Some notes:

1. Why? This is mainly for installing GPG verified toolchains. 
2. This is missing some cleanup and refactoring work, like ensuring that
the user defined toolchain matches the one that Kani was built against
etc. Marked as Todo, for later.

Resolves [#3058](#3058)

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant