Jonathan Protzenko

Hmm I guess the high-level description is: - fetch & launch VS2015 installer with C++ & F# flags - fetch & launch Cygwin installer with silent mode & wget +...

``` D:\cygwin\home\protz\Code\mitls-fstar\src\windows\quiccrypto>nmake -f makefile.vs Microsoft (R) Program Maintenance Utility Version 14.10.25017.0 Copyright (C) Microsoft Corporation. All rights reserved. set PATH=..\kremlib;..\evercrypt;%PATH% & .\test.exe D:\cygwin\home\protz\Code\mitls-fstar\src\windows\quiccrypto> ``` nothing seems to run... any clue...

On my machine, when I copy/paste that line, it displays some output then fails with an illegal instruction error. Nothing shows up when this is executed via the Makefile...

it also doesn't invoke gmake instead of make for building HACL* doesn't check for `brew install make` doesn't check for `brew install gnu-time`

Unfortunately these tests are unconditionally enabled and are not gated on the presence of the required CPU features. If you have any way to submit a patch that would run...

We chatted about key expansion this morning. It's on the radar of @parno. I don't know if @karthikbhargavan's C implementation of AES-GCM also features key expansion. Can you elaborate on...

Ah sorry, I got confused between the two. My bad. Then I don't know why Spec.AEAD misses key expansion. I see it there: https://github.com/project-everest/hacl-star/blob/fstar-master/specs/Spec.AEAD.fsti#L114

You may need to switch to a more recent opam. Can you check if you're on OPAM 1.X? If so, I recommend deleting your $(which opam) and re-running everest check.

ah, yes, everest check only installs opam for you on windows; for linux, I think it's merely a matter of adding Anil's ppa and then installing opam from there

maybe @tahina-pro knows what's up? it could be that you need to run "make" in the quackyducky directory, or that you have failed to export QD_HOME -- try fixing those...