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.
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
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?