Lucas Franceschino

Ah yes, thanks @maximebuyse, somehow I missed that closure! Clearly, we do not support mutable closures (aka `FnMut`). Some quick notes on supporting FnMuts: > - normal closures to FP...

I just took a look at that: - to find what is slow in the engine `cargo hax into --profile BACKEND` is helpful - the AST import is very slow,...

I looked at this issue yesterday. In import_thir, the slow part is not so much importing, but renaming local instance names. The problem is not about this specific operation, but...

Related to https://github.com/cryspen/hax-evit/issues/24

`re` is used to link our printed Rust to pretty printed rustfmt Rust, this pretty printing can be disabled with `HAX_RUSTFMT=no`. We need to use the new generic printer to...

Quoting @franziskuskiefer: "running it on some of the Rust crypto crates like sha2 or hmac will run into that issue" Let's investigate when we have time, we should have a...

Since https://github.com/cryspen/hax/pull/694, we are using OCaml 5, so the issue should not reproduce on main.

Here is a design document for this naming issues: https://docs.google.com/document/d/1D_Cqa3JU_1ktm4LMZaLY6gowq2-2xdthhoQ3lPJT9_Q/edit?tab=t.as6omwfs8eh2 I think I need 1-2 days to implement it, but this would fix most of those issues. ------ ### Actions...

- https://github.com/cryspen/hax/issues/1285 is a F* bug - https://github.com/cryspen/hax/issues/911 is a wontfix (allowing two crates with the same name means we need to disambiguate everything -- the invasive / frequency of...

I'm going to remove the parent to this issue for the first three issues.