Vale and miTLS fail to build on OS X using master branch

[tchajed]

The master branch doesn't compile for me. Vale and miTLS don't build.

For Vale, the error I get is a mysterious scons: *** [obj/testcbc.txt] Error -6, which comes from ./everest and does not appear in the logs.

For miTLS, I get

File "FStar_Mul.ml", line 1, characters 14-31:
Error: Unbound module Prims

also on stderr and not in the logs.

This is a fresh compile, just a clone followed by ./everest pull and ./everest make. I'm on OS X 10.11.

[msprotz]

Vale has been notoriously broken for a long while on OSX. @Chris-Hawblitzel may have some clues.

[s-zanella]

Hmmm... @protz Vale builds fine for me on OS X (I haven't tried running full verification, but that's not needed for the other projects that depend on Vale).

@tchajed The first error you get in Vale is known. I reported it on the #vale channel and it hasn't been resolved. It's a runtime exception in one of the tests that you can ignore.

[msprotz]

@s-zanella yes, but the error prevents everest make from going any further I think

[beurdouche]

Indeed, Vale still fails.

================================================================================
Rebuilding Vale
Running build_vale
271 lines of outputobj/crypto/hashing/testsha256.c:34:3: warning: implicit declaration of function 'Sleep' is invalid in C99 [-Wimplicit-function-declaration]
  Sleep(200);  // Sleep for 200ms
  ^
1 warning generated.
302 lines of outputscons: *** [obj/testcbc.txt] Error -6
303 lines of output
log written to log/vale
================================================================================

Note that I don't have a problem with any other project...

[BarryBo]

testsha256.c is just a checked-in C file, with hand-written C. And the Sleep() call is in dead code. If someone wants to prune out the dead code, we could prevent this build break in the future, for all platforms.

[tchajed]

I think @s-zanella addressed the Vale issue as well as we currently understand it on Slack.

@BarryBo: testsha256.c isn't the issue; the error is that testcbc.exe prints success but exits with code 134 due to an assertion failure in a stack check.

The Vale issue shouldn't matter since everest continues compiling everything else anyway. The miTLS failure is still unexpected.

[s-zanella]

@BarryBo That's just a non-fatal warning. The error comes from running obj/testcbc.exe, which seems to access memory out of bounds. The error does stop the Vale build at that point, but nothing needed by other projects is missing.

[BarryBo]

Ah, OK. It's unclear what went wrong with the assembly code then. Would need access to a repro with a debugger.

[s-zanella]

I used lldb, but I couldn't see what's wrong. A random thing I tried: increasing the size of buffer[16] to e.g. 56 in src/crypto/aes/testcbc.c makes the error go away. Make it much larger and it fails again. An alignment issue?

[msprotz]

Vale build was fixed by https://github.com/project-everest/vale/commit/77f0ccf3d8a95f9cdbe5fb834da7b6c276da0b07

[msprotz]

I believe this is good now. Please reopen if you still can't build the freshest master.