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

Kani compiler should include its backend version #2140

Closed
celinval opened this issue Jan 20, 2023 · 1 comment · Fixed by #2232
Closed

Kani compiler should include its backend version #2140

celinval opened this issue Jan 20, 2023 · 1 comment · Fixed by #2232
Assignees
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected.
Milestone

Comments

@celinval
Copy link
Contributor

Proposed change: The kani-compiler should include its version when execution includes --version --verbose.

Motivation: Cargo uses the compiler version to create a hash code for its compiler. This currently does not include the backend version, but it sounds like they are opened to change it. So this will probably be the best mechanism to implement proper caching invalidation when our users update Kani in case the new version still relies on the same version rustc version.

https://github.com/rust-lang/cargo/blob/ee755e77dae6cd419babe6f778dfff9337a4c7cf/src/cargo/core/compiler/context/compilation_files.rs#L662-L664

@celinval celinval added the [C] Internal Tracks some internal work. I.e.: Users should not be affected. label Jan 20, 2023
@celinval celinval added this to the Proof Caching milestone Jan 20, 2023
@celinval celinval self-assigned this Jan 25, 2023
@celinval celinval changed the title Kani compiler should include the its backend version Kani compiler should include its backend version Feb 2, 2023
@celinval
Copy link
Contributor Author

celinval commented Feb 2, 2023

I just tried this and it looks like rustc doesn't take into account he backend passed to RunCompiler when printing its version. So this will likely need some changes to rustc as well.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected.
Projects
No open projects
Status: Todo
Status: In Progress
Development

Successfully merging a pull request may close this issue.

1 participant