Jonathan Protzenko
Jonathan Protzenko
Unsurprisingly, this breaks windows where indeed, our CI does not generate a config.h (it should!).
I think there is still some benefit to this, namely that we check that the C code generated by krml is syntactically correct for MSVC, so I'd like to keep...
Thanks, I needed a couple more tweaks, hopefully this time is the right time.
So now `make` will error out if you don't have config.h and Makefile.config. You can still write these by hand (Mozilla does), but of course the suggestion is to run...
Yeah that's because the nightly job for refreshing dist/ isn't running yet. So this PR contains a refresh of dist/ as well. Currently blocked on a review, then I'll merge...
Thanks, if this looks good for you on Monday, please go ahead and merge (I'll be off on vacation).
Actually if the spec was using `prims.pow2`, none of this would happen because it is implemented efficiently with a `shift` under the hood. Can we do `let Spec_P256_Lemmas.pow2 = prims.pow2`?
Ah, my bad! I thought this was a pow2. So yeah, need to prove that fast exponentiation is equivalent. But the fact that the stack overflow is in Z is...
Also note that we should remove the two `NOSHORTLOG=1` flags from `make ci` because this generates huge unreadable build logs (we *used* to process these build logs to report some...
closing this one since it has been superseded by the new CI