Lift requirement of having the `prusti` feature enabled
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
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)
bors r+
Canceled.
bors r+
Canceled.
bors r+
Timed out.
bors retry
Timed out.