Dear dune developers,

Coq vernacular files can contain extraction commands, that, when processed by Coq, produce OCaml code from Coq code. For example, coqc generates VarDRaft.ml and VarDRaft.mli when processing the following directive:

Extraction "VarDRaft.ml" vard_raft_failure_params.

There are many Coq projects that build large OCaml projects in this way by extracting OCaml code and then linking it with other code.

However, it's usually hard to set up a build that does the least amount of processing possible to produce the OCaml project (i.e., that skips proofs that may take hours). I have personally resorted to brittle Makefile hacks to accomplish this, e.g., in Verdi Raft.

If there was some way to make dune aware of extracted OCaml files, they could be included in composable builds as other files. I believe this has to be done by manual annotation, since it is not always possible to tell (at least not without a Coq plugin) which files will be produced by an extraction command.

cc: @ejgallego