project-everest / everest

https://project-everest.github.io/
Apache License 2.0
193 stars 29 forks source link

Port to FreeBSD #80

Open web-sst opened 3 years ago

web-sst commented 3 years ago

I ported enough of the project to FreeBSD to build hacl-star and would like to find help to complete the remainder. Next step, how does one extend coverage for the assembly routines in hacl-star to a new OS? Is anyone interested in helping with this work?

msprotz commented 3 years ago

Hi @web-vertalo

The first tidbit would be to fix hacl-star/dist/configure so that it builds out of the box on freebsd. This probably implies fixing https://github.com/project-everest/hacl-star/issues/393 so that either:

If the ABI calling conventions differ between FreeBSD and Linux, then we need figure out how to generate a fourth variant of the assembly .S files, and you'd have to provide more context on what exactly differs.

Hope this helps! Ideally we'd love to have a complete PR including CI for FreeBSD to make sure we keep things working.

Cheers,

Jonathan

web-sst commented 3 years ago

Pursuing the first suggestion from @msprotz, I cleaned up some Linuxisms (e.g. /bin/bash) and added flag setting for FreeBSD, and added -thread to hacl-star to get past the first error in quackyducky builds. Now I'm stuck here:

ocamlbuild -tag debug -use-menhir -tag thread -use-ocamlfind -quiet -pkg batteries -pkg menhirLib -pkg fstarlib -pkg process -pkg hacl-star -pkg yojson -cflags -w,-8 Main.native
+ ocamlfind ocamlopt -linkpkg -g -thread -package yojson -package hacl-star -package process -package fstarlib -package menhirLib -package batteries FStar_Getopt.cmx HashingOptions.cmx Hashtable.cmx OS.cmx Version.cmx Options.cmx Ast.cmx Hashing.cmx Batch.cmx Desugar.cmx Binding.cmx BitFields.cmx parser.cmx lexer.cmx ParserDriver.cmx Deps.cmx InlineSingletonRecords.cmx TypeSizes.cmx Simplify.cmx StaticAssertions.cmx Target.cmx Translate.cmx Main.cmx -o Main.native
File "_none_", line 1:
Error: Files Hashing.cmx
   and /usr/home/web/src/vertalo/everest/_opam/lib/ctypes/ctypes.cmxa
   make inconsistent assumptions over interface Ctypes_types
Command exited with code 2.
Hint: Recursive traversal of subdirectories was not enabled for this build,
as the working directory does not look like an ocamlbuild project (no
'_tags' or 'myocamlbuild.ml' file). If you have modules in subdirectories,
you should add the option "-r" or create an empty '_tags' file.

To enable recursive traversal for some subdirectories only, you can use the
following '_tags' file:

  true: -traverse
  <dir1> or <dir2>: traverse

I don’t understand the -traverse option, but imagine that is not the issue if this code builds on other systems. The standard advice for inconsistent interface assumptions seems to be to rebuild the .mli file. I’m using ctypes.0.18.0, and there is no .ml file corresponding to ctypes_types.mli. Can someone point me in the right direction?

web-sst commented 3 years ago

The quackyducky/3d Makefile does not pass the clean target down to 3d/ocaml, so the 3d/ocaml/_build directory was not removed, resulting in a dirty build.

msprotz commented 3 years ago

Hi @web-vertalo perhaps it'd be helpful to break down this discussion into individual pull requests and/or issues on each project. For instance, I don't know that @tahina-pro keeps an eye on this discussion -- maybe separating the EverParse issues in https://github.com/project-everest/everparse/issues and the HACL* one on its respective bug tracker might be helpful?

We can keep this discussion for the specific issues of the everest configuration script.

Thanks!

tahina-pro commented 3 years ago

The quackyducky/3d Makefile does not pass the clean target down to 3d/ocaml, so the 3d/ocaml/_build directory was not removed, resulting in a dirty build.

This particular issue should be (coincidentally) solved by project-everest/everparse#45 . Thank you @web-vertalo for reporting!

(That said, yes, I agree with Jonathan that EverParse-specific issues should be reported to the EverParse issue tracker.)

web-sst commented 3 years ago

I thought one conversation thread and separate PRs per project was the way to go, and stand corrected. Happy to oblige.