I have a Coq file set up to create an OCaml file through extraction. The Coq file (extraction.v) is built with dune:
Extraction.v has just this:
Require Import Extraction.
Extraction "test.ml" nat.
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:
(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
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?
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.
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:
(targets "test.ml" "test.mli")
(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:
(targets "test.ml" "test.mli")
(action (run coqc "Extraction.v")))
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]
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:
Require Import Test.XYZ.
Extraction "extr.ml" xyz.