How do I specify an Ocaml to Coq dependency across dune files?

Hi all,

I have a Coq file set up to create an OCaml file through extraction. The Coq file (extraction.v) is built with dune:

 (name test)
 (modules Extraction))

Extraction.v has just this:

Require Import Extraction.
Extraction "" nat.

Running dune build Extraction.vo creates extraction.vo and in the build directory, as expected.

Now in the ocaml/ subdirectory of my main directory I, which uses the code in, and another dune file:

 (name main)
 (modules test main))

At the moment, I use a custom makefile to copy the generated from Dune’s build directory to ocaml/, which isn’t great. How can I teach dune to understand that it needs to compile Extraction.v to generate And how do I ask it to copy the generated into the ocaml/ directory?

Or should I not copy at all? (In that case, how do I just tell dune to build it by compiling Extraction.vo?



I see that there’s an open ticket on the Dune tracker about this (, though in my simple case with just one file I’d be quite OK with a manual solution, as long as it can involve just dune (instead of having to glue things together with Make)

Since the rule for the .vo is already defined automatically by dune, you’re a bit out of luck and now cannot specify any extra targets. The solution here is indeed to have proper support for extraction in dune, and I can’t think of any workaround :frowning_face:

Forgetting about extraction for a bit, I wonder if there’s a fundamental feature missing here in dune. In make for example, it’s not very hard to add new dependencies to an existing rule. In this case, we just want to add an additional target to a rule.

Let’s see if @diml has anything to say about this.

Indeed, as originally planned, extraction requires built-in support; fortunately for your use case things will be easy to solve. We shall we back to work on coq-dune language version 1.0 pretty soon hopefully.