FFI fails at compile time

Stream: lean4

[Marcus Rossel]

I'm running into an issue with FFI-ing to Rust, which I don't understand. When I call a Rust-function (via Lean's FFI to C) at runtime (i.e. from the main function), it works as expected. But when I do the same thing at compile time (from an elab), the function returns a different (incorrect) result.
I'm trying to reduce it to an #mwe right now, but might there be a high-level reason why this is happening? (Side note: the Rust code depends on another crate).

---

Or how might one debug-print from Rust code? Then I could inspect the values there as well.

[Mario Carneiro]

you can call lean_dbg_trace from rust

[Marcus Rossel]

Thanks, that helped me find the problem! I had to lake clean :see_no_evil: