search

creusot-rs / creusot

Creusot helps you prove your code is correct in an automated fashion.
GNU Lesser General Public License v2.1
1.12k stars 50 forks source link

refactoring: have the `cargo creusot why3 {replay,prove}` subcommands be handled by `cargo-creusot` #1016

Open Armael opened 4 months ago

Armael commented 4 months ago

This is a follow-up on #943 which performed this refactoring for the why3 ide subcommand. The same refactoring also makes sense for the replay and prove subcommands, and would make the code more consistent.

laurentder commented 3 months ago

We plan to stop using why3 prove and replace it with calls to why3find. Before doing so, we'd like to know if anyone else is using why3 prove. If you do, please let us know here. For why3 replay, a PR is currently underway to integrate it into cargo-creusot.

xldenis commented 3 months ago

I think the only user was @dewert99

dewert99 commented 3 months ago

From @xldenis in #943:

Hmm I think cargo-creusot should be the one to run why3 ide, I would like creusot-rustc to have no particular knowledge of the ide or anything. Its responsibility is generating a text file, that's it. The workflow we want to build should be encapsulated by cargo creusot instead.

Do you think that would be possible?

I think running why3 ide in cargo creusot seems reasonable, but I still think running why3 prove (or why3find if it works similarly) in creusot-rustc has some benefits. This allows creusot to reuse rustcs error reporting to report verification errors, including reusing the rustc Spans to avoid dealing with paths and more properly handle verification errors inside macros. If we decide work on counter examples having the translation context may be useful from mapping why3's counter examples to Rust.