Lucas Franceschino
Lucas Franceschino
Strangely enough, PR https://github.com/hacspec/hax/pull/730 doesn't fix this issue but fixes the looping behavior in `cipher`, from `https://github.com/RustCrypto/traits`. So there are various bugs there.
This is still a problem, a759a1a87e11a3100e605f0312831596a0543dfb doesn't help
Still there after #970
@Nadrieril mostly fixed the bug with its PR #996! So it was just extremely slow because it was re-doing things again and again. This pseudo-loop was hiding another bug; I...
Let's close this. The extraction now works: the extraction itself takes around 40s, but the haxmeta/JSON business takes around 4 minutes on my laptop... Let's see how we can improve...
We need to discuss that, I'm not sure this is still an bug.
Ah, thanks for investigating.
Yeah, maybe that's the best thing to do, let's try it.
Hi @clarus! Actually Hax also uses THIR, so it might indeed be interesting to chat :) The "frontend" of Hax is the part that links into Rustc. It mirrors Rust...
https://github.com/hacspec/hax/pull/650 https://github.com/hacspec/hax/pull/655