Lucas Franceschino

Related to https://github.com/hacspec/hax-actions/actions and PR https://github.com/cryspen/libcrux/pull/210.

Yes, the solutions I describe above were not easy to implement when items could not be renamed, that's why it's not used yet. With https://github.com/FStarLang/FStar/pull/3369, we can now introduce a...

Thanks for the bug report, it's probably due to the test driver being generated which contains some hax unsupported chunks of code. I will look into that. This is related...

This is still relevant

Still relevant

I updated this PR in a way the current generic printer and the new one cohabit. We need to move PV to this generic printer (see https://github.com/hacspec/hax/issues/745), and then we...

Another stealing bug (from issue #474): https://github.com/hacspec/hax/blob/aa14fb139280e7fcd28acb45db27b01b53c9de93/tests/rust-ast/src/lib.rs#L14-L20 _Originally posted by @franziskuskiefer in https://github.com/hacspec/hax/issues/474#issuecomment-1916302172_ [Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/latest-main/gist=3fb3ef965c6df7b5a0c7d22e7d7dfeab) Status: works OK in `8ab62258df` ✅

Yes, exactly, that's what is happening :( Thus it's not even clear we can come up with a visit order of items that would avoid stealing issues...

reproducer for a stealing bug with `cargo hax into -k mir-built`: https://hax-playground.cryspen.com/#json+mir/a339b28377/gist=6630144c4732a2bd55ef8ded02b30ef6 (I haven't shown you the playground yet @Nadrieril, right? :smiley: 'right click > show MIR' on a rust...

We were discussing that yesterday with @Nadrieril: he found a way to override queries, which basically means we can just reimplement the code that used to do the stealing! 🥳...