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

Kani needlessly recompiles everything every time #2036

Closed
Kixunil opened this issue Dec 23, 2022 · 1 comment · Fixed by #2232
Closed

Kani needlessly recompiles everything every time #2036

Kixunil opened this issue Dec 23, 2022 · 1 comment · Fixed by #2232
Assignees
@celinval
Labels
[C] Bug This is a bug. Something isn't working. T-User Tag user issues / requests
Milestone
Proof Caching

Comments

@Kixunil
Copy link

Kixunil commented Dec 23, 2022

When trying to get kani to work one often has to do small changes to a file. Kani recompiles all crates all over again even when only one file changed. Including proc macros, so if there's some technical reason why the code can't be reused for conversion to CBMC at least proc macros should be reusable.
@Kixunil Kixunil added the [C] Bug This is a bug. Something isn't working. label Dec 23, 2022
@zhassan-aws
Copy link
Contributor

Hi @Kixunil. This is indeed very annoying. We've had to disable incremental compilation because of a few bugs that we're working on fixing. This is tracked in #1736.

@zhassan-aws zhassan-aws added the T-User Tag user issues / requests label Dec 23, 2022
@celinval celinval added this to the Proof Caching milestone Jan 19, 2023
@celinval celinval mentioned this issue Jan 19, 2023
Closed
@celinval celinval mentioned this issue Feb 2, 2023
Merged
4 tasks
@celinval celinval self-assigned this Feb 2, 2023
@celinval celinval mentioned this issue Feb 23, 2023
Merged
4 tasks
@celinval celinval moved this to In Progress in Kani 2023-03-06 Feb 23, 2023
@celinval celinval mentioned this issue Feb 28, 2023
Merged
4 tasks
celinval added a commit that referenced this issue Mar 3, 2023
@celinval
Remove glob to collect all artifacts introduced by cargo kani (#2246)
ccec549 
This change allows us to pin-point exactly which build artifacts are related to a cargo build run. This is required to re-enable the build cache (#2036) where multiple artifacts can co-exist in the same folder.

The solution implemented here is rather hacky, but it's more reliable than other alternatives I've tried (see #2246). Now, `kani-compiler` will generate stubs in the place of binaries, shared, and static libraries when those types are requested. Those stubs will contain a JSON representation of the new type `CompilerArtifactStub`, which basically contain the path for the `metadata.json` file where the compiler stores the metadata related to a given crate.

`kani-driver` will parse `CompilerArtifact` messages to figure out which artifacts were built for the given build. For libraries, it will derive the name of the metadata file from the `rmeta` filepath. For other types of artifacts, it will parse the output file, convert it to `CompilerArtifactStub`, and extract the path for the `rmeta` filepath.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@celinval celinval

Labels
[C] Bug This is a bug. Something isn't working. T-User Tag user issues / requests
Projects
No open projects
Kani 2023-03-06
Status: In Progress
Milestone
Proof Caching
Development

Successfully merging a pull request may close this issue.

Enable build cache in cargo kani celinval/kani-dev
3 participants
@Kixunil @celinval @zhassan-aws