cargo-charon does not generate an llbc file upon a second invocation
you can reproduce by running cd libcrux/libcrux-ml-kem; ./c.sh; ./c.sh with the following revisions:
libcrux: 1366394ec8d5b63da49d33a69f73f164a3ec2cfa (on lucas/extract-intrinsics)
charon: c7b2396375cec464fb1e1f27477890681697e3ad (on fix-203)
everest/karamel: 04cb86b94f57c495b715d6e9f98e29352d72d5f3 (on protz_trait_methods)
eurydice: 24b384be011a7bf793a32ec39aa36d365e60313d (on protz_trait_clauses)
upon the second attempt, the state of the top-level target folder is such that the output of charon is
warning: some trace filter directives would enable traces that are disabled statically
note: `trace` would enable the TRACE level for all targets
note: the static max level is `warn`
help: to enable INFO logging, remove the `max_level_warn` feature from the `tracing` crate
[ TRACE charon:154] [main]:
Arguments: Args { inner: ["/Users/jonathan/Code/charon/bin/charon", "--errors-as-warnings"] }
[ TRACE charon:130] [in_toolchain]:
Using rustup-provided toolchain.
[ TRACE charon::toml_config:63] [read_toml]:
Reading options from the `Charon.toml` file
[ TRACE charon:130] [in_toolchain]:
Using rustup-provided toolchain.
Finished dev [unoptimized + debuginfo] target(s) in 0.04s
and no LLBC file ends up being generated.
First step would be to reproduce the bug If I understand correctly, the setup is two crates A and B with B depending on A, and if we call charon on B then A, then the second call doesn't produce an llbc file. If that's not it maybe try some other combinations? x) Basically every call to charon should produce an llbc file; if that's not happening that's a bug.
If you can reproduce the next step is to add a corresponding test to the test suite; if you can't reproduce then we'll see with @msprotz.