Build with dune

[tahina-pro]

This PR is a partial fix to #139 : with this PR, I can now build KaRaMeL 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 also builds with dune instead of ocamlbuild.

[msprotz]

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]

There is some relevant discussion here: hacl-star/hacl-star#426

[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 finish this PR?

[tahina-pro]

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]

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@b12d6f0

[msprotz]

Thanks Tahina for the updated PR.

I'm trying to make sense of your proposed changes and I don't understand the relationship between test/ctypes/dune and https://dune.readthedocs.io/en/stable/foreign-code.html#stub-generation-with-dune-ctypes -- it looks like you explicitly set out to avoid dune's built-in support for ctypes.

Are there any deep reasons why you don't rely on this? Did you encounter any difficulties? It would good to document and understand, since right now your proposed build seems harder to maintain than the previous one.

Thanks

[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@7d16613):

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.

[msprotz]

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?

[victor-dumitrescu]

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?

[tahina-pro]

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!

[msprotz]

Apologies for the delay, I was on vacation then traveling. This overall looks good. Some remarks:

• I'm confused by your usage of + in make recipes, see my various comments
• I think we should get rid of krmllib's OCaml build, I have no clue what purpose this serves
• please remove the top-level myocamlbuild.ml at the root of krml
• 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
• I'm seeing a lot more warnings now in the build, notably warning 7 -- do you know what's up?

once all of the above are done, we can merge. thanks for your patience

[msprotz]

From the GNU make manual, "5.7.1 How the MAKE Variable Works":

Using the MAKE variable has the same effect as using a ‘+’ character at the beginning of the recipe line.

Is there a reason why you added these?

[tahina-pro]

Yes, I can remove this redundant + for clarity, thanks for pointing out!

[tahina-pro]

FYI, f3fac5a introduced +$(MAKE) for the test rule, but it was keeping a pre-existing +, so I could remove it from there as well

[msprotz]

any reason for removing KRML_HOME when it's present in the other recipe above?

[tahina-pro]

this is probably an overlook, let me restore that. Thanks!

[msprotz]

1. based on my understanding of the GNU Make manual, section "9.3 Instead of Executing Recipes": adding a + here means that if someone runs, e.g., make -n extra to see what would be done by make, then dune is still invoked... do I understand this right, and is this a desired behavior?

2. do you know who uses C.ml and TestLib.ml? I don't, and the last reference to them comes from 2017. Can we just remove those files, and the corresponding targets and dune-project files?

[tahina-pro]

1. I wasn't aware of 9.3, thanks for pointing out. However, I was concerned with Appendix B:

‘warning: jobserver unavailable: using -j1. Add `+' to parent make rule.’

where I initially anticipated dune to make use of GNU Make's jobserver (which finally dune doesn't), so let me remove this.
(This also means that there is no way to make the jobserver available to a non-Make process while also honoring make -n)

2. I'm not aware of any F* code depending on krmllib being extracted to OCaml using the handwritten C.ml or TestLib.ml. Not even the (now disabled) miTLS extraction to OCaml does that. So yes, let me simplify things and remove that extra rule.

Thanks again for chiming in!

[msprotz]

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.

[tahina-pro]

Thanks a lot Jonathan for your help!

[msprotz]

Thanks Tahina, much appreciated.