There is a project called Vellvm, which generates some OCaml code from Coq. It’s OCaml source includes:
- Auto-generated code (during build)
- Library code
- Sample main/testing code
I switched it from ocamlbuld to dune. The pull request is pending and they are about to merge it. https://github.com/vzaliva/vellvm/tree/dune
Now, there is another project, HELIX, which wants to use Vellvm as a library. https://github.com/vzaliva/helix/tree/LLVM It also generates some OCaml code from Coq and using dune.
Right now it assumes that vellvm will be a git submodule (or symlink) under
HELIX Coq code depends on Vellvm Coq code. This works pretty well. When generating ML code, it creates files
ml/extracted. Vellvm Coq code is re-used and re-extracted as ML here. So far so good.
Now I am trying to find a way to have some additional OCaml code from Vellvm re-usable in projects like HELIX. Currently, it is just
llvm_printer.ml but there might be more in the future. The directory structure is:
One of the problems is that
llvm_printer.ml depends on some modules from
extracted. Luckily they are the same in both Vellvm and HELIX as they generated from the same Vellvm Coq code.
One reason I’ve chosen to use dune here is the promise of composable builds. But I may have misunderstood the limitations…