Xia Li-yao

Creusot now partially supports `dyn` (implemented in https://github.com/creusot-rs/creusot/pull/1705). Feel free to open an issue to extend support to more traits on a case-by-case basis.

The removal of opam versions seems to have happened here (two days ago) https://github.com/ocaml/opam-repository/pull/27977 That seems to be an initiative to prune packages from the ocaml opam repository.

The opam-repository folks have been quite responsive on this. They've restored the missing dune version (https://github.com/ocaml/opam-repository/pull/28068). You probably want to ask about unarchiving elpi too. On the long-term, it looks...

Yes, I think creusot should let users enable those features unconditionally. ```rust #![feature(stmt_expr_attributes,proc_macro_hygiene)] ```

If it is a goal to be able to compile verified projects with a stable toolchain, we will need to disable all unstable features when compiling. `stmt_expr_attributes` and `proc_macro_hygiene` are...

@jhjourdan proposed to have the dummy version of `requires`/`ensures` remove loop invariants, that avoids the need for `cfg_attr`, so I'm trying that now.

Commands to run `why3find` on all the tests (the long flag is just to turn off warnings to make the logs are more readable): ``` why3find config --detect --why3-warn-off unused_variable,axiom_abstract...

Closed by #1205 and #1255

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...

TODO: - [x] Handle `size_of` - [x] Allow conversions in logic between `*mut` and `*const` - [x] Finish the pointer specs and document their rationale