karamel icon indicating copy to clipboard operation
karamel copied to clipboard

Build with dune

Open tahina-pro opened this issue 4 years ago • 4 comments

This PR is a partial fix to #139 : with this PR, I can now build KReMLin with dune instead of ocamlbuild.

I moved all .ml files into the src/ directory and wrote a dune file to cover that directory tree.

The only part that still requires ocamlbuild at this point is the ctypes test.

tahina-pro avatar Jul 12 '21 22:07 tahina-pro

I'm all in favor of moving everything to Dune, so 👍 for me. Can we do something about the ctypes test? Dune folks promised an easier way to build ctypes programs but as far as I know they haven't come up with the "automatic" solution.

What do other people do with ctypes and dune?

msprotz avatar Nov 11 '21 16:11 msprotz

There is some relevant discussion here: https://github.com/project-everest/hacl-star/pull/426

msprotz avatar Nov 11 '21 16:11 msprotz

I see that https://github.com/ocaml/dune/pull/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 finish this PR?

msprotz avatar Jan 18 '22 14:01 msprotz

Thank you for the update. However, that doc reads (emphasis mine):

Beginning in Dune 3.0, it’s possible to use the ctypes stanza to generate bindings for C libraries without writing any C code.

So I'd suggest to wait until Dune 3.0 (along with its official opam package) is officially released. If anyone were to resume work on this PR right now, then CI changes would be needed to reinstall Dune with --dev-repo.

tahina-pro avatar Jan 18 '22 19:01 tahina-pro

The ctypes test now builds with dune instead of ocamlbuild. However, I had to write all dependencies by hand in dune files, and the ctypes.depend file generated by krml -ctypes is not used. As an alternative, dune might be able to generate all ctypes stubs, thus replacing Karamel's -ctypes option, but I believe this level of automation should be investigated separately, outside of the scope of this PR.

By the way, I have an Everest green: project-everest/everest@b12d6f0b77bad1fd7a05ca9473fc0bd625c83398

tahina-pro avatar Mar 07 '23 05:03 tahina-pro

As an alternative, dune might be able to generate all ctypes stubs, thus replacing Karamel's -ctypes option

Actually, this is not true, ctypes users still need to write a type description functor and a function description functor, so in our case, krml -ctypes should still generate those.

https://dune.readthedocs.io/en/stable/foreign-code.html#stub-generation-with-dune-ctypes Are there any deep reasons why you don't rely on this? Did you encounter any difficulties?

After hours of trying and failing, here are my road blocks:

  • the OCaml stubs produced by krml -ctypes do not align with the OCaml stubs expected by dune's ctypes rule: dune expects separate functors for types and functions, with the type functor taking a Ctypes.TYPE module argument and the function functor taking Ctypes.FOREIGN
  • dune expects an external library name, and I don't know how to specify it, and I don't know what it is for. More precisely, I am not sure dune's ctypes rule works for things other than system libraries: cases other than packages supported by pkg-config are poorly documented
  • even as I try to rewrite OCaml stubs by hand (skipping krml -ctypes) just for Ctypes1, following the documentation, I still end up with these error messages (cf. tahina-pro/kremlin@7d166135debbe26ec451f7ee9f2d2b3fb70da3ec):
File ".Client.eobjs/_unknown_", line 1, characters 0-0:
Error: No rule found for
ctypes0__function_gen__Function_description__Functions.ml
File ".Client.eobjs/_unknown_", line 1, characters 0-0:
Error: No rule found for ctypes0__type_gen.ml
make: *** [Makefile:254: .output/Ctypes2.out/_build/default/Client.exe] Error 1

I am not sure it is worth investing so much time and energy in a dune feature that is explicitly meant as experimental:

Note that Dune support for this feature is experimental and is not subject to backward compatibility guarantees.

So, a saner alternative could be to enrich Karamel's -ctypes option with (or create a new Karamel option for) the generation of those dune rules that I wrote by hand in this PR, and which are actually not much more than a translation of the Karamel-generated ctypes.depend Makefile into dune. But again, as I mentioned above, trying to recover automation for the ctypes example is out of the scope of this PR, which is merely to phase out ocamlbuild.

tahina-pro avatar Mar 07 '23 20:03 tahina-pro

Thanks, this is great to document. @victor-dumitrescu you authored a bunch of this, what do you think? do you think, in addition to ctypes.depend, that we should generate a dune file? or is there a better way to solve Tahina's issues?

msprotz avatar Mar 07 '23 20:03 msprotz

If I remember correctly (although it's been a while) the main difficulty with building with dune was that while it might ultimately be coerced to work with the Ctypes test here, it would be a lot more difficult to build hacl-star-raw with dune, which is the only way in which -ctypes is used in the end. So I get the impression it would be better to have a manual dune file for this test, since I don't think generating a dune file would be useful elsewhere?

victor-dumitrescu avatar Mar 09 '23 16:03 victor-dumitrescu

Thanks a lot Victor for chiming in! In that case, if hacl-star-raw is indeed the only user of krml -ctypes, then the ctypes test should be structured as similarly as possible to the way hacl-star-raw is actually built. From what I remember, it is not even the case on ocamlbuild-based Karamel master: at least before hacl-star-raw moved out of the hacl-star repository, hacl-star-raw was not even built with ocamlbuild, but directly with a Makefile, using the ctypes.depend file generated by Karamel. If still so, then I believe the ctypes test should be retargeted to make instead of dune, in the meantime, until it is decided to move hacl-star-raw to dune.

In all cases, this should be out of the scope of this PR. So, @msprotz, are we ready to merge this PR? Thank you all again!

tahina-pro avatar Mar 14 '23 16:03 tahina-pro

I will submit a commit directly on your branch that builds ctypes just like hacl-star-raw is built, and avoids that un-ergonomic dune build

This is done. This means that @tahina-pro's suggestion is now implemented:

In that case, if hacl-star-raw is indeed the only user of krml -ctypes, then the ctypes test should be structured as similarly as possible to the way hacl-star-raw is actually built.

msprotz avatar Apr 08 '23 09:04 msprotz

Thanks a lot Jonathan for your help!

tahina-pro avatar Apr 19 '23 21:04 tahina-pro

Thanks Tahina, much appreciated.

msprotz avatar Apr 19 '23 21:04 msprotz