Stream: Dune devs & users

Topic: Dune extraction example


view this post on Zulip Karl Palmskog (May 27 2020 at 09:00):

Is there a Dune extraction example ("real" Coq project producing some OCaml module) somewhere? The manual is quite abstract about a lot of commands.

view this post on Zulip Karl Palmskog (May 27 2020 at 09:02):

I tried naively:

(coq.extraction
 (prelude Extract)
 (extracted_modules sin_num))

Where Extract.v has content:

Require Import LexiOrder.
Require Import BuchRed.
Require Extraction.
Extraction "sin_num.ml" redbuch splus smult sscal spO sp1 sgen orderc_dec degc total_orderc_dec.

But this results in:

File "./Extract.v", line 12, characters 0-25:
Error:
The file /home/palmskog/src/coq-community/buchberger/_build/default/theories/LexiOrder.vo contains library
Buchberger.LexiOrder and not library DuneExtraction.LexiOrder

view this post on Zulip Karl Palmskog (May 27 2020 at 09:15):

ah, I see, it's seemingly not possible to have Extract.v in the same directory as other .v files, due to remapping of logical paths.

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 09:28):

Actually that should work, provided you remove the extraction prelude from modules

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 09:29):

oh well, I dunno what Coq will do tho then a double-binding for -Q is found

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 09:29):

we could tho support this case in the regular (coq.theory ) stanza

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 09:29):

so it becomes easier

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 09:29):

the code is fully ready for that

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 09:29):

it would be just a matter of extending the parser

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 09:30):

Please Karl don't hesitate to amend the manual upstream

view this post on Zulip Karl Palmskog (May 27 2020 at 09:32):

given that the .ml/.mli files end up in the directory where Extraction.v resides, it may be a good convention to have it live separately from other .v files

view this post on Zulip Karl Palmskog (May 27 2020 at 09:33):

@Emilio Jesús Gallego Arias I'm not sure what you mean by "remove the extraction prelude from modules"? I tried doing Require Import Buchberger.LexiOrder. in Extraction.v, but didn't work

view this post on Zulip Karl Palmskog (May 27 2020 at 09:34):

in any case, splitting into separate dirs works fine

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 09:35):

I meant in the coq.theory, use (modules :standard \ Extraction)

view this post on Zulip Karl Palmskog (May 27 2020 at 09:35):

ah, OK, I already had: (modules :standard \ Extract ... in my theories/dune

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 09:36):

and in the coq.extraction you should have the right theories , but indeed Coq gets confused about the paths it seems

view this post on Zulip Karl Palmskog (May 27 2020 at 09:36):

should I report it as an issue?

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 09:36):

It is doing -Q . Buchberger -R . ExtractionPrelude I guess?

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 09:37):

For the docs yes please, for the Coq behavior, this is more of a Coq issue

view this post on Zulip Karl Palmskog (May 27 2020 at 09:37):

yes, I got a "directory remapping" warning

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 09:37):

in that currently doubly-binding directories is unsupported

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 09:37):

we could add a note on the dune docs

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 09:37):

or we could just forgive this case

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 09:37):

IIANM the OCaml part of Dune is strict with this

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 09:38):

so it fails if the users does some ambigous mappigns, maybe we should that for Coq, as indeed, having two (coq.theories in the same dir is not supported

view this post on Zulip Karl Palmskog (May 27 2020 at 09:39):

ah, so then having both (coq.theories ...) and (coq.extract ..) in the same dir is not supported as well?

view this post on Zulip Karl Palmskog (May 27 2020 at 09:40):

I think this is fine as long as documented clearly

view this post on Zulip Karl Palmskog (May 27 2020 at 09:43):

I think what happens is that the last logical path mapping overrides all previous ones, so it's not possible to have files in the same directory live in different logical paths, hence it might be impossible to have Extract.v in theories dir with everything else and use dune.

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 09:53):

Yeah, that's what happens; likely a bit more subtle as the code in Coq is a bit messy there. There are some choices that would be possible there.

view this post on Zulip Karl Palmskog (May 27 2020 at 14:01):

ah, I think I figured out everything, it's actually possible to be backwards compatible with coq_makefile with just a bit of reorganization

view this post on Zulip Karl Palmskog (May 27 2020 at 14:02):

with some luck I will be able to port big projects like Verdi Raft to dune extraction quickly

view this post on Zulip Karl Palmskog (May 27 2020 at 14:05):

I could even do something like writing a blog post about the experience (converting Coq+OCaml project fully to dune), but not sure what would be the best forum for publishing that

view this post on Zulip Théo Zimmermann (May 27 2020 at 14:06):

Wherever you publish it, we could advertise it through the CoqLang Twitter account.

view this post on Zulip Théo Zimmermann (May 27 2020 at 14:06):

But now that I think about it, Dune devs might be happy to have this blog post on the Dune blog: https://dune.build/blog
cc @Rudi Grinberg

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 14:09):

Great to hear @Karl Palmskog ; indeed coq.discourse could be a nice venue, not sure the dune blog is the most on topic unless it would be a part of a greater issue than we are planning.

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 14:09):

Note that we plan to do some improvements for the next version of the coq dune lang, these should faciliate the extraction in some scenarios such as in compcert

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 14:09):

in particular we are makinginclude_subdirs per language

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 14:09):

etc...

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 14:10):

I'd like to do a call for Beta testing of Coq + Dune soon, just a few nits missing before I feel comfortable, if you write that post I'll for sure link to it

view this post on Zulip Théo Zimmermann (May 27 2020 at 14:12):

Where are we with the editor support? Is the _CoqProject hack the way to go for the time being?

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2020 at 14:35):

That's a good question @Théo Zimmermann , issues are open upstream for the medium-term plan is not clear for either ocaml-lsp / vs Dune.

My plan is to submit the PR for dune coqtop before the beta call

view this post on Zulip Rudi Grinberg (May 27 2020 at 19:14):

Théo Zimmermann said:

But now that I think about it, Dune devs might be happy to have this blog post on the Dune blog: https://dune.build/blog
cc Rudi Grinberg

Sounds fine to me. Guest posts are welcome, or you can post it where you like and we can just link to it from our side.

view this post on Zulip Rudi Grinberg (May 27 2020 at 19:16):

Karl Palmskog said:

Is there a Dune extraction example ("real" Coq project producing some OCaml module) somewhere? The manual is quite abstract about a lot of commands.

Yeah, that's because my understanding of how coq maps paths to modules is pretty bad.

view this post on Zulip Rudi Grinberg (May 27 2020 at 19:19):

Emilio Jesús Gallego Arias said:

so it fails if the users does some ambigous mappigns, maybe we should that for Coq, as indeed, having two (coq.theories in the same dir is not supported

We had somewhat related problems with ocaml libraries. OCaml's -I ended up being a huge pain in the neck for making things work reliably with multiple libraries in the same dir. In the end, we just ended up transparently moving the build of any OCaml lib/exe into its own sub-directory in _build. Perhaps it would make sense for Coq as well?

view this post on Zulip Karl Palmskog (May 27 2020 at 19:23):

Rudi Grinberg said:

In the end, we just ended up transparently moving the build of any OCaml lib/exe into its own sub-directory in _build. Perhaps it would make sense for Coq as well?

I think this would actually work, since in my example, the file Extract.v would then be moved to its own directory in _build with the Coq logical path DuneExtraction, while the other files in the original directory would still be mapped properly (in this case, to the logical path Buchberger). However, it seems like a good practice to place files with extraction commands in separate directories anyway, at the repo/project level.


Last updated: Oct 16 2021 at 07:02 UTC