prusti-dev icon indicating copy to clipboard operation
prusti-dev copied to clipboard

Lift requirement of having the `prusti` feature enabled

Open JonasAlaif opened this issue 3 years ago • 9 comments

Having prusti-contracts = { path = "path/to/prusti-contracts", features = ["prusti"] } as a dependency breaks regular cargo build since the Prusti procedural macros generate #[prusti::attr = "..."] attributes and these require register_tool(prusti). One solution would be to require users to have this in their Rust source:

#[feature(register_tool)]
#[register_tool(prusti)]

but it still remains a bit impractical to keep switching the prusti feature on and off between prusti verification and regular release builds.

Instead I get Prusti to enable the feature when it runs cargo. This however comes with a caveat that cargo will report:

error: none of the selected packages contains these features: prusti-contracts/prusti

in the case that prusti-contracts isn't a dependency of the crate currently being verified. ~~The only way to catch specifically this error and give the user a hint on how to fix this is to capture the stderr of the running cargo, but we still want all the output cargo spits out printed to the terminal, so we tee the stdout and stderr.~~

In the future we can also probably use the cargo config patch.crates-io for prusti-contracts to ensure that we get the version Prusti was compiled with, e.g. using the commit hash

JonasAlaif avatar Sep 06 '22 08:09 JonasAlaif

Thanks! ~~The stderr tee looks a bit hacky, I think it would have been fine to keep the error message from cargo and explain what it means in one of our guides. We'll see over time how stable this is.~~ (tee hack removed)

Aurel300 avatar Sep 06 '22 09:09 Aurel300

bors r+

JonasAlaif avatar Sep 22 '22 14:09 JonasAlaif

Canceled.

bors[bot] avatar Sep 22 '22 14:09 bors[bot]

bors r+

JonasAlaif avatar Sep 22 '22 14:09 JonasAlaif

Canceled.

bors[bot] avatar Sep 22 '22 14:09 bors[bot]

bors r+

JonasAlaif avatar Sep 22 '22 14:09 JonasAlaif

Timed out.

bors[bot] avatar Sep 22 '22 21:09 bors[bot]

bors retry

JonasAlaif avatar Sep 23 '22 08:09 JonasAlaif

Timed out.

bors[bot] avatar Sep 23 '22 14:09 bors[bot]