Does not build on macOS

[chris-wood]

It looks like fstar.exe is expected to be in a certain location?

/bin/sh: ../../../FStar/bin/fstar.exe: No such file or directory
make[1]: *** [.depend] Error 127

[ad-l]

The environment setup for F* is quite complicated and the recommendation is to use the everest script at https://github.com/project-everest/everest (which will also setup everparse)

You may also be interested in the TLS parsers on mitls dev https://github.com/project-everest/mitls-fstar/blob/dev/src/parsers/Parsers.rfc

[tahina-pro]

I wrote a documentation page to build EverParse from its sources, now at https://project-everest.github.io/everparse/build.html or, equivalently, doc/build.rst. I managed to build and run EverParse on FreeBSD 12.2 (but then, C code generated by EverParse will not build because kremlib does not support FreeBSD yet kremlib's FreeBSD support has not been ported to EverParseEndianness.h yet.)

Could anyone please test building and running EverParse again with Mac OS at this point, following those instructions, and post your feedback here in this issue? Thank you in advance,

[landonf]

Could anyone please test building and running EverParse again with Mac OS at this point, following those instructions, and post your feedback here in this issue? Thank you in advance,

Building against a non-writable OCaml installation (using make everparse) failed in install-hacl-star-raw when attempting to modify ld.conf to include the new ocaml-packages path:

ocamlfind: /opt/local/lib/ocaml/ld.conf: Permission denied

Building against a user-writable opam installation got to the packaging stage, but failed in package.sh when attempting to discover libffi:

++ dpkg -L libffi6
++ grep '/libffi.so.6$'
++ head -n 1
src/package/package.sh: line 193: dpkg: command not found
+ libffi=
+ [[ -n '' ]]
++ pacman -Qql libffi
++ grep '/libffi.so.7$'
src/package/package.sh: line 197: pacman: command not found
++ head -n 1
+ libffi=
+ [[ -n '' ]]
++ rpm --query libffi --list
++ grep '/libffi.so.6$'
src/package/package.sh: line 201: rpm: command not found
++ head -n 1
+ libffi=
+ [[ -n '' ]]
+ echo libffi not found
libffi not found
+ exit 1
make: *** [everparse] Error 1

[tahina-pro]

Thank you @landonf for testing on your side!

Building against a non-writable OCaml installation (using make everparse) failed in install-hacl-star-raw when attempting to modify ld.conf to include the new ocaml-packages path:

ocamlfind: /opt/local/lib/ocaml/ld.conf: Permission denied

Yes, this is documented in step 3 of https://project-everest.github.io/everparse/build.html#linux :

You need to specify an OCaml version number (between 4.08.0 and 4.12.x), so that OCaml will be installed in your user profile, because some EverParse dependencies do not work well with a system-wide OCaml. Thus, if opam says that there is an ambiguity, you should re-run opam init with the non-system package for OCaml.

make everparse intentionally does everything in userspace, including HACL*'s install-hacl-star-raw and install-ocaml. We could ask the HACL* people whether performing the "install" parts of those two rules as root is supported at all.

[tahina-pro]

Building against a user-writable opam installation got to the packaging stage, but failed in package.sh when attempting to discover libffi:

Thank you for reporting! Yes, I learnt how to do so on Ubuntu, Arch Linux and Fedora, by testing, but definitely not for Mac OS X. Could you or anyone please point me to the right command to discover the location of shared objects such as libffi.so.* (or however it should be named) on Mac OS? Thank you in advance.

At least you reached the point where you successfully managed to build everything in EverParse, and the error you encountered is only a matter of populating the everparse/ subdirectory to make it standalone. However, the copy being interrupted at this point, your everparse/ subdirectory is not usable at this stage. Fortunately, everything has been built in the source tree, so you should be able to use EverParse after setting up the environment variables as prescribed in steps 5 to 8 of https://project-everest.github.io/everparse/build.html#build-in-the-source-tree and adding the directory containing z3 to the PATH. Maybe I should add a paragraph in the documentation mentioning that fact.
Conversely, maybe I should swap the copy stages for populating EverParse, copying EverParse first and the dependencies only later, so that everparse/ directories can be used at least on the machine where they were built even if some dependencies are missing to make them fully standalone.

Thank you again!