Build hacl-star-raw OCaml bindings with Dune

[craigfe]

This ports the existing Makefile rules for building the hacl-star-raw OCaml bindings to use Dune, leaving a hybrid build system in which Make handles evercrypt and Dune uses this to build the OCaml library.

The immediate result of this is that hacl-star is usable with an opam monorepo workflow (which requires that the dependency tree be buildable with Dune). In the medium term, this is a path to making hacl-star compatible with the MirageOS 4.0 cross-compilation toolchain, allowing Tezos to be deployable on unikernels and eliminating the need for Mirage's own HACL bindings. (CC @TheLortex)

The Dune rules are more complex than the previous Make ones, partly because KreMLin emits the stub dependencies in Makefile format and partly because Dune has no support for wildcards in its rules. The overall process is:

• the rules in lib/ and lib_gen/ are generated by a gen_dune_rules.ml executable which parses the ctypes.depend file;
• the generation process is tied to dune test, so any change in the ctypes.depend without regenerating the Dune rules will cause the tests to fail;
• the rules can be regenerated with dune runtest --auto-promote.

For now, I've stripped out the OCaml auto-detection in the configure step. I'm not sure how to port this logic to work with Dune vendoring; perhaps others have ideas? I also haven't looked at how the CI works yet, or dealt with the Makefile templating logic. Pointers appreciated.

[msprotz]

Hi Craig,

I took a quick look at this; the short version is, it looks great and I'm happy to see things moving towards Dune. Here's some high-level remarks before I do a detailed review:

• I think it'd be easier to have KReMLin emit directly the right dune file rather than you writing a utility to convert the Makefile dependencies into dune format; what do you think of ditching this part: https://github.com/FStarLang/kremlin/blob/master/src/GenCtypes.ml#L562 and replacing it with something that directly emits the right dune stuff?
• is there any way to have variables? I find it regrettable that the CFLAGS are repeated everywhere, maybe dune has a mechanism for that?
• I remember Anil or someone saying that there would soon be an easier mechanism to build ctypes bindings with dune -- is this the "improved" version? it feels like there ought to be a more "high-level" construction in Dune to describe a binding rather than 40 lines for each entry; do you know of any plans to make that happen in Dune, and if not, can we improve Dune first before?
• we absolutely need to keep the check for whether ocaml is installed or not because some CI targets don't have an OCaml setup, and it is not ok to require users of EverCrypt to have a complete OCaml setup in order for their build to be successful; why not simply keep configure as-is, or improve it to make sure dune is installed in addition to checking for the right ocaml version and ocamlfind packages?

Thanks!

Jonathan

[craigfe]

Hi Jonathan,

Thanks for the very rapid response :-)

• I think it'd be easier to have KReMLin emit directly the right dune file rather than you writing a utility to convert the Makefile dependencies into dune format; what do you think of ditching this part: https://github.com/FStarLang/kremlin/blob/master/src/GenCtypes.ml#L562 and replacing it with something that directly emits the right dune stuff?

I completely agree; I initially wasn't sure how closely linked the two projects are / how problematic it is to need to release them in lockstep. I suppose the way forward is for me to try to port the Dune generation logic to KreMLin as an opt-in (e.g. with a flag), and leave the Makefile generation intact?

I'm not sure how much more general the KreMLin generation is vs. hacl-star's requirements, but I'll find that out :-)

• is there any way to have variables? I find it regrettable that the CFLAGS are repeated everywhere, maybe dune has a mechanism for that?

In Dune land, this is typically done by storing the CFLAGS in an s-expression file. I've pushed a commit that goes that way instead.

• I remember Anil or someone saying that there would soon be an easier mechanism to build ctypes bindings with dune -- is this the "improved" version? it feels like there ought to be a more "high-level" construction in Dune to describe a binding rather than 40 lines for each entry; do you know of any plans to make that happen in Dune, and if not, can we improve Dune first before?

First-class support for Ctypes in Dune is tracked by this issue and this RFC, which is currently being worked on by @mbacarella here. Given the size of that feature, I suspect it's worthwhile going ahead with a hand-rolled set of Dune rules first and then improving them on a second pass when possible.

• we absolutely need to keep the check for whether ocaml is installed or not because some CI targets don't have an OCaml setup, and it is not ok to require users of EverCrypt to have a complete OCaml setup in order for their build to be successful; why not simply keep configure as-is, or improve it to make sure dune is installed in addition to checking for the right ocaml version and ocamlfind packages?

The problem with the current approach is that it gives false-negatives when building via Dune with a vendored ctypes, since ocamlfind isn't necessarily installed or aware of the available packages. Thinking about it a bit more, I think it's not difficult to fix: Dune just needs to tell the configure script to assume that the OCaml dependencies are available, and non-Dune users will keep the same behaviour. I've pushed a commit that does this in a fairly brainless way.

[msprotz]

Thanks for the very rapid response :-)

Of course!

I suppose the way forward is for me to try to port the Dune generation logic to KreMLin as an opt-in (e.g. with a flag), and leave the Makefile generation intact?
As far as I know, there's two users of the OCaml binding generation feature of kremlin: HACL, and kremlin's own ctypes test. The latter uses OCamlBuild anyhow, and I would LOVE to see it ported to Dune. So, if you want to rip out the Makefile support and have only Dune from here on, that's 100% fine by me.
In Dune land, this is typically done by storing the CFLAGS in an s-expression file. I've pushed a commit that goes that way instead.

Great!

First-class support for Ctypes in Dune is tracked by this issue and this RFC, which is currently being worked on by @mbacarella here. Given the size of that feature, I suspect it's worthwhile going ahead with a hand-rolled set of Dune rules first and then improving them on a second pass when possible.

Indeed. I hope this work converges soon. But you are right that we should go ahead -- the dune file would be auto-generated anyhow, so it's not the end of the world.

• we absolutely need to keep the check for whether ocaml is installed or not because some CI targets don't have an OCaml setup, and it is not ok to require users of EverCrypt to have a complete OCaml setup in order for their build to be successful; why not simply keep configure as-is, or improve it to make sure dune is installed in addition to checking for the right ocaml version and ocamlfind packages?

The problem with the current approach is that it gives false-negatives when building via Dune with a vendored ctypes, since ocamlfind isn't necessarily installed or aware of the available packages. Thinking about it a bit more, I think it's not difficult to fix: Dune just needs to tell the configure script to assume that the OCaml dependencies are available, and non-Dune users will keep the same behaviour. I've pushed a commit that does this in a fairly brainless way.

Got it. However, I'm not sure your commit is right: if the user runs ./configure without options, then this test:

if [[ "$enable_ocaml" == "0" ]]

returns true and therefore unconditionally disables OCaml bindings.

How about a variable called ocaml_support that has three states: enable, disable, and empty (auto-detect).

Then the logic becomes:

if [[ $ocaml_support == "enable" ]]; then
  echo "... OCaml support unconditionally enabled"
elif [[ $ocaml_support == "disable" ]] || ! detect_ocaml; then
  # disable here
fi

Thoughts?

[msprotz]

I initially wasn't sure how closely linked the two projects are / how problematic it is to need to release them in lockstep

There's a way to make your PR here run against a kremlin branch and then make sure we merge both in lockstep without breaking anything. I can help with that sort of CI regressions, let's look at it once you have the changes on the kremlin side.

[msprotz]

I also forgot to mention that dist/gcc-compatible/configure is auto-generated and that you should edit this one but also dist/configure (the reference one)

[avsm]

We can definitely upgrade to the dune-supported-ctypes when that lands in a few months. It's worth having this edition in an interim release, as that'll support older dune clients too.

[msprotz]

@craigfe anything I can do to help with this?

[craigfe]

@msprotz: Apologies for letting this PR hang; it's still on my TODO list and not forgotten.

I'll shift my patch onto Kremlin as discussed in the next few days and then ping you. Thanks again for the help :-)

[msprotz]

@craigfe hey, I was wondering if you had had any chance to make progress on this? we're hoping to switch the build of kremlin itself to dune, and there's a ctypes example in the kremlin tree, so having dune support in kremlin would be a really great way to make sure we don't need to keep our ocamlbuild dependency just for this: https://github.com/FStarLang/kremlin/blob/master/test/ctypes/myocamlbuild.ml

CC @tahina-pro

[msprotz]

I see that ocaml/dune#3905 was merged and there is now very nice documentation here: https://dune.readthedocs.io/en/latest/foreign-code.html#ctypes-stubgen

Is there any chance we could try to use this to simplify our build?

[msprotz]

FYI, in FStarLang/karamel#212, Tahina and I looked into building bindings with Dune. In the current state of things, building with dune is worse than building by hand with GNU Make.

Compare GNU Make: https://github.com/FStarLang/karamel/pull/212/files#diff-79d14c68062282c555defd7aaf293674db9793e219b3a9aba196cf371d8ef621

With hand-writing every single rule within Dune: FStarLang/karamel@6df4e93

The former is more generic and reusable than the latter. With the latter scenario, krml would have to generate complete dune files (I don't want to do that).

Furthermore, bindings are now covered by hacl-packages, which is another reason to close this issue.

In the even that building ctypes bindings with Dune becomes natural and seamless, I'm happy for this issue to be reopened, but on the hacl-packages side. Thanks!