Nadrieril

This refers to [this surprising change](https://github.com/AeneasVerif/charon/pull/272/files/0fb1b5de2ba2d3fc53feb152c6469df9a4c5eb74#diff-65de021b714c84083be304ab2d85bed8012f36a79321a993007d0083e27b8201).

More specifically, that changes indicates that the file no longer tests the codepath in charon that we wanted to test. We could use `core::intrinsics::discriminant_value` to guarantee we get the right...

We hide `Sized` on purpose by passing `--hide-marker-traits` to charon; that's easy to solve. The other properties you mention are also tracked by existing traits: - `core::marker::DiscriminantKind` has the discriminant...

Of note, this behavior is specified in [RFC 1328 "Global Panic Handler"](https://rust-lang.github.io/rfcs/1328-global-panic-handler.html): > After the handler returns, the runtime will then unwind the thread. If a thread panics while panicking...

The stripping of unused parameters is necessary but not trivial. I'm thinking you could avoid that by making `Helper` depend on these generics: ```rust #[hax_lib::associated_item(0f46abbe-c101-4d57-bcad-9b465291783c)] // We include whatever M1..Mn...

I'm following developments but don't need to be involved in the meeting, ty :)

This issue most importantly requires a test to be added in `tests/cargo`, where two crates with the same name end up in the crate graph, and we extract items from...

May I ask that we move conversations about specific points to a review thread on some part of the diff? I believe the project recently decided this was the best...

You might be interested in https://docs.rs/serde-seeded/latest/serde_seeded and https://docs.rs/serde_state/latest/serde_state which try to do this.

cc @dianne