Jonathan Protzenko
Jonathan Protzenko
There was a blog post somewhere where Mirage folks were unhappy with the __has_include (which we should now be able to get rid of). According to https://en.cppreference.com/w/cpp/compiler_support this is in...
I'm happy to approve a PR that removes __has_include from lib/c/* and assumes everyone runs configure and thus has a valid config.h -- Mozilla has a hand-written config.h, correct?
Interesting. But then are you compiling AVX or AVX2 code? How are you defining `HACL_CAN_COMPILE_VEC128`?
Ok I thought about it and I believe your solution is actually even better. This means clients who want to integrate HACL have two options: - -D... compiler options using...
Then maybe append `[rename=Hacl_Hash]` to your HASH_BUNDLE so that the filename is more palatable?
- Please resolve conflicts - Please refresh dist/mozilla -- right now I still see that very long filename in there. ``` git rm -rf dist/mozilla/* make compile-mozilla git add dist/mozilla...
It's the `mul` proof that seems to trigger a memory explosion with the long calc chain.
I tried splitting the long calc chain into smaller steps (no more than two `==` steps per calc statement). The memory usage went to 12GB this time. CC @nikswamy who...
Closing since this file is now gone.
You do not need OCaml; a simple "./configure && make" in dist/gcc-compatible should work. If ./configure does not give the results you want (e.g. because you're cross-compiling to a specific...