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

[Armael]

trafficstars

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]

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]

I think the only user was @dewert99

[dewert99]

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.

[Lysxia]

We've now fully switched to using why3find via cargo creusot prove. I tried to keep the old code path through creusot-rustc for a while but it was getting too much of a hassle after some refactoring so it ended up getting removed.