mitls-fstar
mitls-fstar copied to clipboard
project-everest
Custom setup using Cygwin and Ocaml Issue
I am trying to follow the readme build environment setup for the Cygwin OCaml setup. I have the relevant packages described and a .fstar submodule of the F* repos with a OCaml build (as suggested in the text). I've had no errors till now, but when running the suggested command "make all-ver -j 2" in the tls directory in Cygwin, I get
make: *** No rule to make target 'all-ver'. Stop.
I tried "make all -j 2" but it produces the result:
make -C ./src/tls all make -C ./src/tls make[1]: Entering directory '/home/kristoffer/mitls-fstar/src/tls' rm -f cache/OCaml/.depend cache/Kremlin/.depend cache/Model/.depend make[1]: Entering directory '/home/kristoffer/mitls-fstar/src/tls' rm -f cache/OCaml/.depend cache/Kremlin/.depend cache/Model/.depend make -C ../parsers gen make -C ../parsers gen make[2]: Entering directory '/home/kristoffer/mitls-fstar/src/parsers' make[2]: *** No rule to make target 'Parsers.HKDF.rfc.gen', needed by 'gen'. Stop. make[2]: Leaving directory '/home/kristoffer/mitls-fstar/src/parsers' make[2]: Entering directory '/home/kristoffer/mitls-fstar/src/parsers' make[2]: *** No rule to make target 'Parsers.HKDF.rfc.gen', needed by 'gen'. Stop. make[2]: Leaving directory '/home/kristoffer/mitls-fstar/src/parsers' make[1]: *** [Makefile:11: refresh-depend] Error 2 make[1]: Leaving directory '/home/kristoffer/mitls-fstar/src/tls' make: *** [Makefile:10: model-all] Error 2 make: *** Waiting for unfinished jobs.... make[1]: *** [Makefile:11: refresh-depend] Error 2 make[1]: Leaving directory '/home/kristoffer/mitls-fstar/src/tls' make: *** [Makefile:13: test] Error 2
What am I missing in the setup? I experience with the Docker setup and with Windows 8.1 and 10.
Best regards, Kristian
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 two then git clean -fdx then building again?
Yes, you need QD_HOME set to the directory where EverParse is installed. By the way, this README.md seems really outdated, it does not mention such dependencies as EverParse, HACL*, or even Kremlin. So the best way for now is to use the Everest script following instructions at https://project-everest.github.io/
Thank you for your suggestions. I ended up using the instructions from https://project-everest.github.io/ and was able to call check and make without errors.
Cheers, Kristian
