AeneasVerif
Charon does not generate any output if there is an internal compiler error
Charon does not generate any output if there is an internal compiler error, even though it actually manages to recover from those errors. Also, I note that if I copy this code to move it here then Charon outputs the serialized file. Maybe this is the solution?...
Does it output something with --errors-as-warnings in the case you're testing?
Said differently, this is charon working as intended: in my mind, calling charon by itself should only produce a well-formed output. --errors-as-warnings is the flag that allows it to produce an output that may be missing some items.
That said, things have changed and a few other options can make the output contain missing items (e.g. --hide-marker-traits or --exclude) so I'm thinking we may simply set --errors-as-warnings to be the default and always emit an llbc file.
Does it output something with
--errors-as-warningsin the case you're testing?
No that's the issue: in case there is a rustc internal error it doesn't output anything, even in the presence of--errors-as-warnings (which is actually expected, because --errors-as-warnings simply changes the way the Charon errors are reported - it doesn't have any effects on rustc's own errors).
Hm I see. I presume what happens is that when we catch_unwind a compiler panic, this still eventually causes run_compiler to panic because the compiler remembers that it panicked.
In fact the export code used to be where you point to, I moved it because I wanted as little code as possible to be run within the compiler callbacks. Maybe I should just restore the catch_unwind around the compiler invocation that I removed in https://github.com/AeneasVerif/charon/pull/362.
Actually putting the code there where you put it perfectly makes sense to me: the only issue is that I don't think we can control those internal rustc errors (unless we manage to get rid of all of them of course ^^').
I re-added the top-level catch_unwind which I hope should fix this, but I did not have a test case at hand for this. Could you confirm we now emit llbc?