Dune support

[Alizter]

Hi, would you be interested in getting a dedicated Dune stanza for coq-of-ocaml?

I suppose it would be somewhat dual to the coq.extraction stanza. You could have something like this:

(coq.of-ocaml
 (name my_program))

(coq.theory
 (name my_proofs)
 (theories my_program))

The coq.of-ocaml stanza could convert all .ml files in scope of the stanza and make a coq theory with the specified name. (We could of course allow for some restriction of which ml files are chosen too).

Dune would call coq-of-ocaml to generate this theory. It is not clear to me if it is a good idea to allow to .v files to be promoted and included as part of the build directory. However it would be possible to treat these generated .v files as a coq theory that can be reasoned about in a separate theory.

However whether or not the produced .v files are available for the user to further modify poses an interesting restriction. It would be difficult to keep updating the .v files for instance every time the ml files are updated. Keeping the theories separate doesn't have this problem, however would suffer from visibility issues. The user would have to inspect _build to see what the theory actually contains.

Let me know if this is something you might find useful, it wouldn't be very difficult to write for Dune IMO.

cc @rgrinberg who might be interested

[clarus]

Hello,

Thanks for the suggestion! I am not well versed in Dune, so I cannot comment much on the technical aspect. Indeed, we often proceed in two steps:

1. the generation of the .v files using coq-of-ocaml;
2. running a patching script, typically doing search and replace.

But ideally, only step 1) should be necessary, if we allow ourselves to edit the .ml files so that the translation is done right.

In any case, I would be interested and find this useful! Thanks!

[Alizter]

I'll create an issue in the Dune repo so we can discuss the implementation some more.

[clarus]

OK top thanks!