To use dev-dependencies, you need to guard with cfg(all(kani, test))

[tedinski]

When cargo builds a project in test mode that has a dev-dependency, we see 3 basic calls to rustc (i.e. kani-compiler, in our case):

1. Build the main project, but NOT IN TEST MODE (as a lib).
2. Build the dev-dependency.
3. Build the main project, now in test mode (as a bin).

We're adding --cfg=kani to all these calls, so if we gate on just cfg(kani) for the use of the dev-dependency, the first build will fail with an unknown import. (Possibly this is deliberate on cargo's part: ensuring cargo build will succeed before testing? Unfortunately, we inject our additional cfg(kani) so it's not actually the same as a cargo build...)

If you instead gate your proofs module with #[cfg(all(kani, test))], things will work properly. For example:

#[cfg(all(kani,test))]
mod proofs {
    use foo; // something from dev-dependencies
// ...
}

We should make this unnecessary, somehow. If we adopted #1214, then perhaps we could detect the lack of --test in kani-compiler and thus disable --cfg=kani. That would fix it...

[celinval]

I would like to step back a bit and ask a more fundamental question. Do we want to pass --cfg=kani everywhere or just while compiling the target crate?

[tv42]

If I use #[cfg(all(kani,test))] in the library (not tests/), cargo kani no longer finds the proof (since test wasn't set):

No proof harnesses (functions with #[kani::proof]) were found to verify.

[celinval]

Hi @tv42, you either have to pass --tests flag to Kani or you need to change your configuration to be #[cfg(any(kani,test))]

[celinval]

I don't think there is much to do in this issue. The usage of cfg should reflect how the user wants to build their code.

[tv42]

#[cfg(any(kani, test))] isn't great because then tooling like rust-analyzer complains "use of undeclared crate or module kani".

I'll test cargo kani --tests after some current runs complete..

[celinval]

@tv42 can you please create an issue describing your case and the problems you are facing so we can assist you?