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:
(coq.theory
(name test)
(modules Extraction))
Extraction.v has just this:
Require Import Extraction.
Extraction "test.ml" nat.
Running dune build Extraction.vo creates extraction.vo and test.ml in the build directory, as expected.
Now in the ocaml/ subdirectory of my main directory I main.ml, which uses the code in test.ml, and another dune file:
(executable
(name main)
(modules test main))
At the moment, I use a custom makefile to copy the generated test.ml 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 main.ml? And how do I ask it to copy the generated test.ml into the ocaml/ directory?
Or should I not copy test.ml at all? (In that case, how do I just tell dune to build it by compiling Extraction.vo?
Thanks!
3 Likes
I see that there’s an open ticket on the Dune tracker about this (https://github.com/ocaml/dune/issues/2178), 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 
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 @jeremiedimino has anything to say about this.
1 Like
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.
Adding the following to dune in the ocaml/ subdirectory almost works, but not quite:
(rule
(targets "test.ml" "test.mli")
(deps "../Extraction.vo")
(action (run cp "../test.ml" "../test.mli" "./")))
It works the first time I run it, but then if I modify ocaml/dune it breaks because test.ml isn’t in _build/default anymore. Does dune delete unexpected build outputs? Is there a way to ask it to not do that? (Sorry if I missed something in the manual.)
An alternative I tried was to use a rule to explicitly call coqc, but I didn’t find a way to invoke it with the right flags. Something like this:
(rule
(targets "test.ml" "test.mli")
(deps "Extraction.vo")
(action (run coqc "Extraction.v")))
Indeed dune will clean build targets it is not aware; this is needed to get correct rebuilds for example when you remove a module from your source tree. In this case not even the copy_files stanza will help I think 
I’m aiming to update the Coq dune mode next week, adding extraction support should be easy, however I am not sure about the right syntax for the stanza, suggestions are welcome.
Regarding the flags indeed for now they are not exported as a variable, however as an über hack you can have a look to _build/log and just copy them [this won’t be future-proof but hopefully will help until proper extraction support lands]
1 Like
With Emilio’s latest changes, this works in Dune 2.5. The trick is to move Extraction.v to the ocaml/ subdirectory and add a coq.extraction stanza in there:
coq/dune:
(coq.theory
(name Test)
(modules XYZ))
ocam/Extraction.v:
Require Import Test.XYZ.
Extraction "extr.ml" xyz.
ocaml/dune:
(coq.extraction
(prelude Extraction)
(extracted_modules extr)
(theories Test))