Use <target>/kani as the target directory and clean at every build
#1847
Conversation
We currently put cargo-kani compilation artifacts inside regular cargo target. This can conflict with users compilation artifacts and unnecessarily rebuild code). This can also cause `cargo kani` to fail compilation if users try to run `cargo kani` and `cargo kani --legacy-linker` without cleaning their target directory.
kani-driver/src/call_cargo.rs
Outdated
| let outdir = target_dir.join(build_target).join("debug/deps"); | ||
|
|
||
| // Clean directory before building since we are unable to handle cache today. | ||
| // TODO: https://github.com/model-checking/kani/issues/1736 | ||
| self.cargo_clean(&target_dir)?; |
There was a problem hiding this comment.
Would deleting the <target>/kani directory instead work?
There was a problem hiding this comment.
Sure. cargo clean seems like a good way to clean stuff generated by cargo build, but the effect is the same, so if you prefer, I can just remove the folder.
There was a problem hiding this comment.
Thanks. I think the advantage of just removing the kani directory is to not wipe out the artifacts of a normal (non-kani) cargo build.
There was a problem hiding this comment.
Which would hopefully make the UX a bit "less-terrible".
There was a problem hiding this comment.
BTW, we were providing the correct target directory to cargo clean, so it was only wiping out target/kani not the entire target. Anyway, not a biggie.
Description of changes:
We can't really handle caching compilation artifacts today. So we are going to perform a
cargo cleanbefore building the goto program. I also changed our target to use thekanisubfolder inside target.We currently put cargo-kani compilation artifacts inside regular cargo target. This can conflict with users compilation artifacts and unnecessarily rebuild code). Now we force rebuild without modifying the target, that would always delete the entire user build folder, which seems like a terrible UX.
Resolved issues:
Resolves #1821.
Related RFC:
Call-outs:
Testing:
How is this change tested? Existing tests + manually tests.
Is this a refactor change? No
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.