Jonathan Protzenko
Jonathan Protzenko
~I can confirm this is fixed. Thanks!~ Actually I just saw this again. Will try to send a repro soon.
I think the code got rewritten and I don't remember which set of revisions last triggered it. I'm ok with closing, and we'll reopen it if it resurfaces. Thanks.
I thought I had modified the Docker file to pick up the latest versions of tooling but apparently not.
I'm also pushing a couple other low-hanging fruits on this branch, such as chopping the libcrux_intrinsics prefix for intrinsics.
I chatted about this with @nikswamy the other day. It has to do with i) a bad error message and ii) an actual issue with a type variable that would...
FYI, just gave this a quick try, and I don't seem to be receiving the comments at all anymore (or at least, the one I noticed had a problem)
Is no one else in the Rust ecosystem doing this? (Retaining inline comments.) Should this be a discussion with upstream Rustc to add more support in the compiler itself?
FYI I tried this just now and I got this: ``` [Charon__GAstOfJson.type_decl_kind_of_json] failed on: `Assoc ([("Error", `String ("Unsupported type: foreign type: core::fmt::rt::{extern#0}::Opaque")) ]) ``` to reproduce, add `--extract-opaque-bodies` to $(CHARON)...
Concerning your remark about inline: we could make this the behavior of CInline by default, since we tend to always want something marked as inline to be always inlined. But...
@karthikbhargavan would @mamonet be available to push a fix for this?