[coq] [draft] Support for coqffi

[ejgallego]

This is a draft PR to support @lthms coqffi rules that allows for Coq to call OCaml libraries https://github.com/coq-community/coqffi . This has been written in collaboration with @lthms .

As of today, we add a (ffi_modules ...) field to (coq.theory ...) and the corresponding rules for .cmi to .v generation. This is a pretty small patch and highlights how to add a simple rule to Coq's mode.

There are some open issues and todos before we can consider this ready:

• blocker: fix code to locate a cmi from a lib + OCaml module name. As of today we just do a hack, however it doesn't work for wrapped modules; we couldn't find the right API for it.
• syntax: there are several options, may need to specify flags, etc... so this is still work in progress
• documentation / changelog
• more tests [should be disabled by default until coqffi is stable]
• version check for (coq.theory ...)

[ejgallego]

This doesn't work, we also tried:

  let cmi_path =
    let open Result.O in
    let* ml_lib = Lib.DB.resolve lib_db (Loc.none, Lib_name.of_string ml_lib_name) in
    let info = Lib.info ml_lib in
    let obj_dir = Obj_dir.public_cmi_dir (Lib_info.obj_dir info) in
    Result.Ok (Path.relative obj_dir (coq_module_name ^ ".cmi"))

which works but it doesn't compute the right cmi path for wrapped libs.

[ejgallego]

Updated with a fresh attempt to locate a cmi path, but unfortunately it only works for local libs.

[lthms]

Updated with a fresh attempt to locate a cmi path, but unfortunately it only works for local libs.

This is already a pretty great improvement, congrats!

[ejgallego]

Adding @rgrinberg 's comments on how to move forward with this:

The correct way is to find the Obj_dir.t that corresponds to this library and then use it to resolve the module. You can obtain the module by name by getting the Modules.t of the library.

For external libraries, the Modules.t should be available straight fromdune-package.

What might be problematic is obtaining Modules.t for external libraries. Because I recall that we only wrote this value to dune-package for special cases. That should be easy enough to fix.

[lthms]

Thanks @ejgallego (and @rgrinberg ) for the heads-up. I have tagged a first beta release for coqffi, so I will have some time now to work on this. I hope I will be able to have a first clean version for modules from local libraries later this week!

[ejgallego]

Hi @lthms , I'm closing this PR due to inactivity, but I'd love to reopen and finish it if you still find it useful.

[lthms]

Yeah, sorry about that. I’ve been focused on other things. Yet, coqffi has become way more stable now, and I think that as soon as I release the first stable version, I will give this another try.

Thanks again a lot for taking the time to guide me the other time.

[ejgallego]

Great to hear, looking forward to completing this, and to using coqffi