Build script fails to execute Kremlin.native

[fefrei]

I'm trying to get Vale to run within the Ubuntu subsystem on Windows 10.

Running scons in the repository eventually results in a call to cd obj/crypto/hashing && /home/felix/vale/tools/Kremlin/Kremlin.native. This fails with Invalid argument, likely because this is a Windows binary:

file ~/vale/tools/Kremlin/Kremlin.native
/home/felix/vale/tools/Kremlin/Kremlin.native: PE32+ executable (console) x86-64, for MS Windows

Renaming Kremline.native to Kremlin.exe results in a file that is executable on Windows, but I'm trying to work in the Ubuntu subsystem.

What's going wrong here? Is Kremline.native supposed to be a Windows binary?

[BarryBo]

Thanks for reporting this. I do much of my development on Bash For Windows, including Vale work.

The checked-in copy of Kremlin, in tools/Kremlin/Kremlin.native is indeed a PE32+ Windows binary. For Ubuntu builds, you'll need to replace it by a Linux binary. The sources are at https://github.com/FStarLang/kremlin, and it is built using OCaml. Or you can grab one from the Docker image at https://hub.docker.com/r/projecteverest/everest/. That image contains the full output of our end-to-end build.

[fefrei]

Wonderful, thank you! I got a satisfying scons: done building targets this time.

I'll leave this open in case you want to improve the documentation or error messaging here.