Improve error messages using annotate-snippets

[Kixunil]

WIP The code contained a bunch of unsound unsafe which I've fixed here but I think some things are still off. At least some spams look weird and there's an unknown VC, so I will need to categorize it.

Whenever a VC failed to prove, the user would have to launch the why3 IDE and click through to find the line where the proof failed. This was quite annoying. It's preferable to have error messages similar to what rustc/cargo emit so that the location is immediately visible.

This change uses the why3 OCaml API to inspect the failures and prints them out in the same style rustc uses using the annotate-snippets crate (which is the crate that rustc currently uses internally).

Closes #2012

[jhjourdan]

To be honest, I don't think we can merge this in the current state:

• There are some changes about spans int the Creusot code. While I acknowledge that there are some missing spans here and there, some of this code seems just garbage to me, which gives me low confidence on the quality of the rest of the code.

• A large amount of code involves linking with the Why3 API in OCaml, and I know writing such stub is subtle and would require careful reviews. In addition, the impact on the build system is non-trivial, and, again, I would like that this could be carefully reviewed to make sure it is portable enough. We decided from the start of the development of Creusot not to link with OCaml code precisely to avoid the complexity related to that. Maybe one day we will change our minds about that, but then we would do that directly for the main Creusot executable, which will not only bring us better error messages, but also all sorts of other advantages (performances, incremental proofs...).

I'm really sorry for that.

[Kixunil]

There are some changes about spans int the Creusot code. While I acknowledge that there are some missing spans here and there, some of this code seems just garbage to me, which gives me low confidence on the quality of the rest of the code.

Oh, crap, sorry, I didn't mean to commit those parts, that was a mistake. I saw some missing spans and tried to add them and submit a PR separately but that work is not finished yet. Yeah, it's garbage because I didn't understand it so I tried to brute-force it with an LLM as a stopgap for the tool to work with the intention to come back and clean it up. It seems I mistyped some git command and included it. I'm very sorry to have taken your review time on that crap.

Regarding the linking part, did I misunderstand this message? #2012 (comment) Or did you hope the integration would be simpler which turned out to not be the case?

In any case, I plan to maintain it as a separate binary for myself so we can merge it later when the situation changes.

[jhjourdan]

Regarding the linking part, did I misunderstand this message? #2012 (comment) Or did you hope the integration would be simpler which turned out to not be the case?

Sorry for me not being precise in #2012 (comment): I did mean that we could have an OCaml process linking with the Why3/Why3find APIs which would somehow communicate with another process written in Rust. I did not imagine that you would figure out a way to use the Rust-OCaml FFI, write stubs and have a working build system for that.

[Kixunil]

Ah, I see, that would've made so much sense. I guess I could try that. The stub already does some kind of serialization, so it should be fairly easy to just move to another process.