Proposal: always building in "test mode"

[tedinski]

In short: build with cargo test --no-run not cargo build, making the current --tests option the default (and only) build mode.

There are three currently open issues related to this proposal:

1. RMC should use fully qualified name for harness selection and it should not rely on no_mangle attribute #661 This would be resolved by having #[kani::proof] expand to include #[test] under cargo kani. This would ensure that the function always gets codegen'd.
2. Cargo rmc subcommand should be able to use dev-dependencies #585 Building in "test mode" includes dev-dependencies.
3. Cargo rmc fails with crate-type bin (and tests) #473 This is caused by building in "bin" mode, building in "lib" mode resolves it. Unfortunately, building with --tests re-causes the issue. We need to figure out how to accommodate this.

What are the drawbacks?

1. Building in test mode builds all the (what cargo calls) "integration" tests under ./test/. Given that Kani just flat links everything together, this might cause problems? (Have these ever been observed?) So a prerequisite might be to do proper linking of multiple binaries (stemming from multiple "integration tests"), before we switch to this.
2. ?? Feedback wanted.

[camshaft]

If we're concerned about integration tests, we can pass test --lib by default, which will only build the unit tests (see https://doc.rust-lang.org/cargo/commands/cargo-test.html#target-selection). You could then make integration tests opt in with another flag.

[zhassan-aws]

Building in test mode builds all the (what cargo calls) "integration" tests under ./test/. Given that Kani just flat links everything together, this might cause problems? (Have these ever been observed?)

Confirmed that this causes problems in #1448.

[celinval]

I have mixed feelings about this one. I'm curious to know more about the motivation here.

In some cases, users might want to use test code in their harnesses. Like extra assertions and sanity checks. Some dev-dependencies might be relevant while writing harnesses.

On the other hand, building things in test mode will compile things like the std test library which we don't use. Not all dev-dependencies and test code are desirable or suitable for verification. E.g.: crates like pretty_assertions. If we force the test mode, now users will have to guard them with #[cfg(all(test, not(kani)))].

I would prefer that we keep supporting both modes (test and regular build) until we have strong use cases that makes one undesirable. I have a soft preference to using regular build by default. This will make the user choice clear on what to use at each scenario.

[Kixunil]

I would be surprised if test mode is less common than regular mode. If regular mode is still desired --no-test flag would solve the issue. Or if specific projects want to override it allow to put override into Cargo.toml but for the sake of newbies default to tests.

Note that not enabling test is crazy-counter-intuitive since all other testing infrastructure does enable it.