Thanks a lot for this! I will try to have a look at this PR this week.

I’m a bit surprised by this:

The intended use case is for the .mli file to become the interface for the .ml file extracted from the .v file.

Though the idea is very nice, coqffi is not intended to do that. What coqffi does is ensuring that the Coq definitions which uses the axioms introduced in the FFI module it generates correctly use the implementation of the original mli file.

This is summarized by this graph introduced in a blogpost about how to use coqffi to implement en Echo server in Coq.

@lthms Thank you very much for the detailed reply. It looks like I misunderstood what coqffi is doing. I will mark this PR as draft and study your blog post further so I can amend the implementation.

@lthms I've updated this PR so that it now takes in the cmi of the specified module instead. In order to do this, the user must specify which library is being talked about. This allows for composition with libraries in a workspace or those that are installed. For now, only libraries installed using Dune are supported (due to the presence of cmi).

I thought about allowing for multiple libraries, but that would make resolving the module name trickier.

Another question: Do you want flag support?

I've added some basic flag support.

The support you are describing looks awesome, thank you so much for doing it. I on the other hand have not been the best reviewer you could have hoped for.

I had a quick look this evening, mostly the code part, and the tests. Looks good so far. I plan to have a test-run of my own this week.

I've also added :standard support today which let's you coqffi an entire library.

OK so there is a huge issue with this PR atm, which is that coq.theory cannot pick up the output of the coq.ffi stanza. I will try to fix this, but if I don't finish this week, coq.ffi will have to miss 3.6.

I've fixed the ability for coq.theory to pick up the generated .v files. However I had to drop support for :standard since supporting dir_contents in this case is quite complicated. It is not a particularly important use case either.

I agree. Besides, using coqffi on a hierarchy of modules is a bit more involved, and would require to generate a bunch more file, so I think it’s okay to not support it for now.

Moreover this should maybe be guared with (using coqffi), it seems to me.

Can dune easily sort module by dependencies? Meaning, if i give (modules a b) but in practice b uses things introduced by a, then can we know that easily from dune?

If we do, I think it would make more sense taking the time to support this.

For a list of modules sorted by dependencies relation A, B, C, then it would mean

• For each module, use the --witness flag: this will generate a .ffi file in addition to a .v file
• For B, pass the -I A.ffi ; for C, pass -I A.ffi -I B.ffi

(with the correct path prefix)

By doing so, it’s possible to have C.v rely on a type introduced in either A or B.

Does it makes sense?

@lthms , yes it makes sense, and Dune can do that. I guess in your case the dep information is what ocamldep would give. Then we just need to setup the rules as:

{ a.ml }       --{ coqffi }--> { a.v a.ffi }
{ b.ml a.ffi } --{ coqffi } --> { b.v b.ffi }

Exactly! The set of ffi files used as input for some rules will be an overset, but that is not an issue in practice.

OK seems I need to do some more work on this. I have split coqffi into its own stanza/language/files so that we can easily work on it in the future. I need to understand how the .ffi file rules will work so I will open a new draft and close this PR.

#6489

Why do we need to close PRs just to reopen them again? It makes the dicussion harder to follow, and worse meta-data in general.

@ejgallego because this is now a new feature and not an extension to Coq lang.

@ejgallego because this is now a new feature and not an extension to Coq lang.

We can just rename the PR? Anyways, not a big deal, just wondering about the logic as a curiosity.