Hi,

Lately, I have been working on coqffi, a tool to generate “FFI modules” to OCaml functions. It is my hope that coqffi will eventually be adopted by the Coq community, as a convenient way to mix Coq and OCaml code.

coqffi takes a cmi file as its input, and generate a Coq module. I have been using it with dune with a lot of success, as demonstrated by the examples directory of the repo (see the dune file).

For instance,

(rule
  (target File.v)
  (action (run coqffi -finterface %{cmi:file} -o %{target})))

The fact that dune understands out of the box that File.v is a dependency of a theory declared with the coq.theory stanza is truly amazing. Thanks!

I was wondering if, when the time is right, it would be possible to add a dedicated field in dune to the coq.theory for instance, for coqffi to be more easily accessible to Coq users.

Desired Behavior

Basically, the idea is to have a more straightforward way to generate FFI modules, for instance, ffi_modules.

Example

(library
  (name MyLib)
  (public_name pkg.MyLib))

(coq.theory
  (theory Test)
  (ffi_modules (MyLib.Test))

Which would means (1) generate the Test.v module from the cmi of the Test module from the MyLib library, and (2) add this module to the list of modules of the coq theory Test.

We could imagine being able to provide coqffi arguments, like

(coq.theory
  (theory Test)
  (ffi_modules ((MyLib.Test :flags -finterface))))

So to wrap-up, do you think such a thing is possible? Is there a way for me to make it happen (which is not hacking dune to add the feature, but more from the coqffi side. The first obvious step is to publish a stable version of coqffi of course, but in addition to that, is there anything that comes to your minds?

Thanks for your feedback!