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.

Sign up for GitHub

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

Jump to bottom

Build cache should consider changes to the compiler #2229

Open
celinval opened this issue Feb 23, 2023 · 2 comments
Open

Build cache should consider changes to the compiler #2229

celinval opened this issue Feb 23, 2023 · 2 comments
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected.
Milestone
Proof Caching

Comments

@celinval
Copy link
Contributor

Proposed change: For internal development, we should include information about the current compiler version (e.g.: the commit hash or a hash of the kani-compiler binary. We should also include the toolchain version that's being used.

Motivation: This will alleviate the development pain of remembering to do a cargo clean whenever making changes to the compiler. Not doing so can manifest in weird / inconsistent results that end up taking time to debug.
@celinval celinval added the [C] Internal Tracks some internal work. I.e.: Users should not be affected. label Feb 23, 2023
@celinval celinval added this to the Proof Caching milestone Feb 23, 2023
@celinval celinval mentioned this issue Feb 23, 2023
Merged
4 tasks
@celinval
Copy link
Contributor Author

Some context: rust-lang/cargo#8073

@celinval
Copy link
Contributor Author

celinval commented Mar 3, 2023 •
edited
Loading

For Kani developers, if you make any change to kani-compiler or the rust toolchain, you might need to clean the build cache. For the regression, remove the build/ folder in the repo root, for one off test, delete the target directly. Another option is to pass the --force-rebuild flag to cargo kani

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected.
Projects
None yet
Milestone
Proof Caching
Development

No branches or pull requests
1 participant
@celinval