Extracting ml using dune: A query on stanza usage

Using Coq
1

Dear Coq Discourse,

I have a question about extracting Ocaml from Coq using dune via the coq.extraction stanza.

I was trying to get a minimal example of Ocaml extraction with dune made but in the process I received errors. Whilst fixing these errors I discovered that I can get .ml extraction using a normal (coq.theory) stanza and a (coq.extraction) stanza without any extracted modules set. This doesn’t feel right to my intuition of how dune works so I am asking for clarification on this matter.

Context

I was looking through the dune documentation and saw that dune supports as build operations both extracting coq theories to ocaml via the coq.extraction stanza and also using Js_of_ocaml using the executable stanza. As an exercise, I wanted to test to see how viable it was to use dune to automate both steps in one build processs by writing a simple coq function then using dune to turn it into some js code, before testing the emitted js in a simple .html document.

I have not really made use of Coqs extraction tools before, but I have at some point checked it out by using the Extraction Command in Coq and building using a Coqmakefile. The only thing I have done with the extracted .ml is inspect it, but in theory I know how to extract coq to Ocaml in the makefile approach. my problem occurs when I try to do thing the dune way.

Other than setting up an opam switch with dune, coq, and js_of_ocaml, I have no experience of running js_of_ocaml but that is something I will find out once I learn how to get the Coq-extraction up and running properly with dune.

Question

I’ve cooked up a small git repo to help make my question more specific. There are two top level directories /dune_extraction_test and /makefile_extraction_test which contain the same test.v file given below, just containing an identity function and are built using dune / the coq-makefile respectively:

From Coq Require Extraction.
Definition c: nat->nat := fun  b => b.
Check c.
Extraction "test" c.

The make-file extraction goes through fine and is just there as a comparison. What I am confused about is the specifics of doing so using dune. In particular, observe the following three dune stanza:

Dune config using coq.theory stanza

 (coq.theory
 (name test)
 )

Dune config using coq.extraction stanza

(coq.extraction
(prelude test)
(extracted_modules )
)

Dune config using coq.extraction stanza with named module

(coq.extraction
(prelude test)
(extracted_modules test)
)

Using any of the three stanzas on test.v I can extract ml code from the Coq code into the _build directory . This is odd to me as in the first case the docs do not say that a regular theory stanza can emit .ml code, and in the second case I note that the docs say explicitly that (extracted_modules <names>) is an exhaustive list of OCaml modules extracted. I interpret this as meaning that the test module should not actually be extracted in this case that they are not on the list, however this is not what occurs on my machine.

I know that dune is somewhere looking into the extracted_modules field in the build process because if I change it to something like (extracted_modules fail) it errors out with:

Error: Rule failed to generate the following targets:
- test_theory/fail.ml
- test_theory/fail.mli

My Question is/are: am I using coq.extraction stanza correctly? Why is it that Coq successfully extracts modules with an empty extracted_modules field or indeed using the coq.theory stanza?

I know the dune implementation is (or at least up to somewhat recently has been) still in development, so I assume there are changes still being felt out / not all things having being implemented.

I imagine that In order for dune to use the extracted .ml further on in the build process I am required to use coq.extraction stanza with explicitly given extracted_modules so that dune may locate them?

2

At the level of individual shell commands, given a .v file there is only one thing to do with it: call coqc on it. Although there is only one action to take, it may be done with different intents, the most common intents being to compile into .vo and to extract to .ml+.mli. What the dune stanzas do is to specify your intent to the dune build system, because that matters for the purposes of managing dependencies. You are telling the build system whether a .v is meant to produce .vo or .ml, which other parts of the project may then depend on.

To recap, under the hood, it’s all coqc, so whichever stanza you pick, you will see the same artifacts. The choice of stanza does not affect how the source files are consumed, but it affects how the produced files will be used by the build system.

One difference between compiling to .vo and extracting to .ml is that given a.v you know from the file name that it will compile to a.vo, but to know what .ml files will be extracted you have to compile it because there are extraction commands where the output file name is implicit. This is a problem for build systems: they need to figure out how files depend on each other to decide in what order to compile files, but here we have to compile a file to even know that there is an extracted .ml that other files may depend on. Dune solves this chicken-and-egg problem by requiring you to write down the names of the .ml files to expect from extraction. That’s the purpose of the extracted_modules field. If you don’t specify the right modules, it won’t affect the coqc command that is run, but it may confuse the build system later on: either it won’t know about an extracted file that will be needed elsewhere, or it expects an extracted file but won’t find it.

Hope that clears up things for you.

1 Like
3

Thanks for the response! In-between asking this question and your reply I took another look at the dune docs and improved my understanding of how the build system works and the use of deps and targets, so your explanation makes sense!

As a quick followup up: I noticed in the course of getting my project up and running that that if one does not set an output directory flag on a coq.extraction stanza then dune/coq gives a little warning of:

File "./theory.v", line 9, characters 0-43:
Warning: Setting extraction output directory by default to
".../project/_build/default/app/coq".
Use "Set Extraction Output Directory" or command line option
"-output-directory" to set a different directory for extracted files to
appear in. [extraction-default-directory,extraction,default]

to set an output directory. However setting the flag to anything other than

(flags (-output-directory "."))

produces an error as like you have explained one has confused dune due to it expecting a target .ml file in the current directory and it then not getting one. I suspect that this warning is a hold-over from the coq-makefile days? This issue is nothing more than an annoyance on the terminal (that one can get to disappear with the above flags field), but it may prove a source of confusion to people in a similar position to me coming into asking this question.

Do you think this issue is worth opening a git-issue for this or just leaving be?

4

I also find it strange that we have to set this flag to silence the warning. It would be nice if it just didn’t warn. AFAICT, it already does the right thing on its own (that is, extract into where dune expects it). It is a good idea to ask Dune folks about it, whether it can be fixed or there is a good reason for this behavior.

1 Like