Jonathan Protzenko

@franziskuskiefer is this something that hacl-packages can address?

Build working properly in hacl-packages... from here on, the build of the dist/ folder is only for internal development and as such I don't see this as a dealbreaker. But...

The build log contains errors about ``` make[2]: *** [: Hacl_Bignum256_32_Hacl_Bignum4096_32_Hacl_Bignum256_Hacl_Bignum4096_Hacl_Bignum32_Hacl_Bignum64_Hacl_GenericField32_Hacl_GenericField64_Hacl_Bignum_Hacl_Bignum.o] Error 1 ``` so this still doesn't appear to be working. Let me try to suggest an alternative today.

New error: ``` internal/Hacl_Bignum.h:39:10: fatal error: lib_intrinsics.h: No such file or directory 39 | #include "lib_intrinsics.h" | ^~~~~~~~~~~~~~~~~~ compilation terminated. Makefile.basic:53: Hacl_Chacha20Poly1305_256.d: No such file or directory make[2]: *** [Makefile.basic:48:...

Once we merge #649, we can address this very simply.

@franziskuskiefer what do we do with this? is there freebsd CI on hacl-packages?

Per the discussion with Franziskus, no immediate action needed on this. If someone wants to reinstate FreeBSD CI, let's do it on hacl-packages, with proper GitHub actions. Thanks.

The original issue was fixed and the discussion moved onto unused variables, which is tracked in #583

Transferring this issue to project-everest/everquic-crypto

Will you resubmit this? I'm actually quite keen on getting rid of that VLA. @polubelova and I chatted about this, and if we put Hacl.Impl.SHA3 on the right-hand side of...