Feature request: support for extracted OCaml files in Coq builds

[palmskog]

Dear dune developers,

Coq vernacular files can contain extraction commands, that, when processed by Coq, produce OCaml code from Coq code. For example, coqc generates VarDRaft.ml and VarDRaft.mli when processing the following directive:

Extraction "VarDRaft.ml" vard_raft_failure_params.

There are many Coq projects that build large OCaml projects in this way by extracting OCaml code and then linking it with other code.

However, it's usually hard to set up a build that does the least amount of processing possible to produce the OCaml project (i.e., that skips proofs that may take hours). I have personally resorted to brittle Makefile hacks to accomplish this, e.g., in Verdi Raft.

If there was some way to make dune aware of extracted OCaml files, they could be included in composable builds as other files. I believe this has to be done by manual annotation, since it is not always possible to tell (at least not without a Coq plugin) which files will be produced by an extraction command.

cc: @ejgallego

[ejgallego]

I guess we can run Coq to generate the list of extracted files, as indeed recursive extraction is problematic.

[bobot]

In another way, could we choose in the dune file what to extract and then dune will instruct Coq about what to do.

[palmskog]

I would personally prefer to choose a file/module in the the dune file and let dune instruct Coq. This would work great for Verdi Raft. However, for other projects such as Disel which produces tons of files/modules during (recursive) extraction, this would not work as well (see, e.g., coq-disel-tpc in Disel vs. vard in Verdi Raft).

[mattam82]

Same for metacoq, if listing could be avoided it would be great. Although, currently, the make-based build does list the produced .ml files.

[ejgallego]

IMO explicit listing should only happen when somehow we'd like to constraint the default file list.

[bobot]

I agree that listing should happen only when the default list is not sufficient. But the main question, in my opinion, is should we need to run coq or another tool to know the list of generated files?

Currently dune only need the list of existing files and the content of dune files for all (most?) of the current rules. Could we make coq extraction follow this property by restricting which kinds of extraction are accepted?

[mattam82]

That would prevent the kind of Recursive Extraction Library Foo which extracts foo.ml but also all its dependencies.

[bobot]

Not completely, it is just not coq which is computing the recursive dependency, for javascript (separate compilation mode) there is something similar where the ocaml dependencies must be compiled to javascript. In the case of coq it could be the same, we extract once the dependencies separately that dune should be able to know in some ways.

[ejgallego]

I'd like to implement this soon, at least for the explicit listing mode; any suggestion on the syntax?

cc: @cpitclaudel

[cpitclaudel]

In most of my developments I extract a single file and the extraction command is fairly large (it lists a bunch of identifiers).

I imagine this could move to the dune file (something like (extraction "Extracted.ml" symbol1 symbol2 symbol3), but there would be multiple issues.

• Symbol names would have to be fully qualified
• Dependencies would have to be specified (how does dune know which files to load before running the extraction command?)
• Dependency loading order is important (if two files use different Extract Inductive commands, for example)

OTOH, I see the appeal of somehow putting all extraction commands inside of the dune file itself (but that's going to be a lot of code)

I would be fine with telling dune explicitly about the ml files that an extraction command generates, and I would also be fine with changing my workflow to use a different style of extraction (like library extraction) if that makes things easier.

[Zimmi48]

I think it would make sense to keep the extraction command within the Coq file and only inform Dune of what ML files are generated. In fact, this could even be the job of coqdep, much like it is its job to inform Dune of what files a given file depends.

[cpitclaudel]

Here's an extra thought: in my case an ideal solution would allow me to say that a .ml file is generated by extraction, and make that ml file a module of a regular Coq library (possibly through an intermediate rules that copies it, of course)

[Zimmi48]

a regular Coq library

Didn't you mean OCaml library?

[cpitclaudel]

Yes:) Woops.

[rgrinberg]

I think it would make sense to keep the extraction command within the Coq file and only inform Dune of what ML files are generated. In fact, this could even be the job of coqdep, much like it is its job to inform Dune of what files a given file depends.

Note that dune must know this information "statically". That means dune needs to know if a module is a target of some rule (in this case - extraction) without running any external commands. So I think you would at least need to say which modules you expect to be extracted with some sort of extract stanza.

I'd like to implement this soon, at least for the explicit listing mode; any suggestion on the syntax?

One example:

(coq.extract
 (targets foo.ml bar.ml) ;; we're writing file extensions not to rule out extraction to other languages
 (libraries f1 f2 f3) ;; coq libraries used by foo.v
 (module foo) ;; foo.v will contain "Extraction foo.ml" etc.
 )

[rgrinberg]

Another current limitation that dune imposes on extraction is that you will not be able to extract source in more than 1 directory. That means you will not be able to extract trees usable with (include_subdirs ..).

This is the same limitation with native compute. Hopefully we'll lift it soon. In any case, the above should be quite simple to achieve and it will require no additional boilerplate to use extracted sources in normal library or executable stanzas.

[cpitclaudel]

Thinking more of this, should this even be specific to coq? The following could tell dune that generating xyz.vo also generates foo.ml and bar.ml, as a way to tell dune about extra outputs of an existing rule:

(extra-outputs
 (target xyz.vo)
 (outputs foo.ml bar.ml))

[rgrinberg]

Thinking more of this, should this even be specific to coq? The following could tell dune that generating xyz.vo also generates foo.ml and bar.ml, as a way to tell dune about extra outputs of an existing rule:

In general, I would be careful with features that are low level like this. In dune we’ve learned the hard way that exposing more build artifacts to users than necessary is a common theme for breakage. For example, we’ve had to break many user written rules that relied on where dune would write cmi files.

When possible, we should strive to design features that are as high level possible so that we can evolve the internals of dune without breaking user rules. So in this particular case, it would be preferable to attach the extraction targets to the coq modules themselves:

(coq.lib
 ...
 (extract
  (xyz foo.ml bar.ml)
  ...)))

[cpitclaudel]

So in this particular case, it would be preferable to attach the extraction targets to the coq modules themselves:

Got it

[palmskog]

I would definitely prefer

(coq.lib
 ...
 (extract
  (xyz foo.ml bar.ml)
  ...)))

and not having to worry (specify statically) what the dependencies of the .v file that produces foo.ml and bar.ml are. It may also be a good idea to require full disclosure of the accompanying .mli files produced by Coq for all extracted files by default, i.e., (xyz foo.ml foo.mli bar.ml bar.mli).

[rgrinberg]

and not having to worry (specify statically) what the dependencies of the .v file that produces foo.ml and bar.ml are.

Just to clarify: dune only requires a complete static description of the targets. It lets you discover dependencies dynamically as any good build tool.

It may also be a good idea to require full disclosure of the accompanying .mli files produced by Coq for all extracted files by default, i.e., (xyz foo.ml foo.mli bar.ml bar.mli).

Not only it's a good idea, but it is also a hard requirement. Otherwise, dune will delete those .mli files on the next run.

[palmskog]

Not only it's a good idea, but it is also a hard requirement. Otherwise, dune will delete those .mli files on the next run.

In that case, and since to my knowledge there is no way to not produce both .ml and .mli files through Extraction, it may be a good idea to drop the extensions and just write:

(extract
  (xyz foo bar)

and make dune account for all of foo.ml, foo.mli, bar.ml, and bar.mli implicitly.

[rgrinberg]

it may be a good idea to drop the extensions and just write:

Doesn’t coq support extraction to languages other than OCaml? Granted, none of those languages need dune as a build system but at least it’s conceivable that it will be useful.

…

On Nov 2, 2019 00:39 +0900, Karl Palmskog ***@***.***>, wrote: > Not only it's a good idea, but it is also a hard requirement. Otherwise, dune will delete those .mli files on the next run. In that case, and since to my knowledge there is no way to not produce both .ml and .mli files through Extraction, it may be a good idea to drop the extensions and just write: (extract (xyz foo bar) and make dune account for all of foo.ml, foo.mli, bar.ml, and bar.mli implicitly. — You are receiving this because you commented. Reply to this email directly, view it on GitHub, or unsubscribe.

[cpitclaudel]

Doesn’t coq support extraction to languages other than OCaml?

It does; that's a good point to keep in mind.

[vzaliva]

Let's not forget about composable builds. I have a project (Helix) that uses extraction, which in turn depends on another project (Vellvm) which also uses extraction. Ideally, it would be nice to compose dune builds of both projects for both Coq and OCaml.

[ejgallego]

At the Dune meeting @rgrinberg proposed a design for extraction support which IMO is the way to go for now. The basic idea is to add an (extract ...) field to (coq.theory ...) stanzas so that Dune will generate the proper Coq's Extraction vernaculars.

IMO this should provide a nice solution for many use cases. For example in CompCert we would turn:

Separate Extraction
   Compiler.transf_c_program Compiler.transf_cminor_program.

into

  (extract
    (modules
       (Compiler (definitions transf_c_program transf_cminor_program)))

etc...

[vzaliva]

What about customizing extraction? Here is an example:

https://github.com/vellvm/vellvm/blob/master/src/ml/extracted/Extract.v

See Extract Inlined statements.

[ejgallego]

What about customizing extraction?

These can go in a .v file which is used by Dune by a (prelude .,,) field.

[rgrinberg]

I've tried building the vellevm project and it seems like the amount of code you guys extract is quite high. It might be too tedious for you to list all your modules statically like in my earlier suggestion.

However, if you don't mind this boilerplate. It will not be hard for me the form of extraction suggested by Emilio above.

[ejgallego]

It might be too tedious for you to list all your modules statically like in my earlier suggestion.

At some point we can have Coq generate the list of targets and use something like promotion to keep it up to date.

[Zimmi48]

Or have coqdep give this info directly to dune? Anyway, Rudy's suggestion is good to have extraction supported in Dune even with older versions of Coq, correct?

[rgrinberg]

Or have coqdep give this info directly to dune

There is no way to do this properly in dune currently. Why should coqdep know about the list of targets some .v extracts by the way? A link to the docs regarding this would be appreciated.

Anyway, Rudy's suggestion is good to have extraction supported in Dune even with older versions of Coq, correct?

Yes, it should work with old versions. Note that to support this feature properly, no new features from coq are required. What is required is to relax some current design limitations in dune to allow dynamic targets. Unfortunately, lifting these limitations is a bit of a slow process, as we're bound both by both backwards compatibility and performance needs of our users.

Which is why I think that it would be best to provide something functional in the short term for coq users, even if it requires a bit of boilerplate (listing all modules they intend to extract in a dune file) from users.

[cpitclaudel]

Which is why I think that it would be best to provide something functional in the short term for coq users, even if it requires a bit of boilerplate (listing all modules they intend to extract in a dune file) from users.

This sounds quite fine. But how will it work with extracting multiple definitions to a single file?

[ejgallego]

This sounds quite fine. But how will it work with extracting multiple definitions to a single file?

I guess the field could be something such as

   (extraction
      (module foo (constant a b c))
      ...

[cpitclaudel]

Works for me :)

[mattam82]

It's fine to list the modules we extract, that's the same requirement today using coq_makefile(repeating them in .mllib/.mlpack files as well).

[ejgallego]

Rudy has just submitted a PR adding extraction support to Dune c.f. #3299