Karl Palmskog (May 27 2020 at 09:00): 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.
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
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.
Emilio Jesús Gallego Arias (May 27 2020 at 09:28):Actually that should work, provided you remove the extraction prelude from modules
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
Emilio Jesús Gallego Arias (May 27 2020 at 09:29):we could tho support this case in the regular (coq.theory ) stanza
Emilio Jesús Gallego Arias (May 27 2020 at 09:29):so it becomes easier
Emilio Jesús Gallego Arias (May 27 2020 at 09:29):the code is fully ready for that
Emilio Jesús Gallego Arias (May 27 2020 at 09:29):it would be just a matter of extending the parser
Emilio Jesús Gallego Arias (May 27 2020 at 09:30):Please Karl don't hesitate to amend the manual upstream
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
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
Karl Palmskog (May 27 2020 at 09:34):in any case, splitting into separate dirs works fine
Emilio Jesús Gallego Arias (May 27 2020 at 09:35):I meant in the coq.theory, use (modules :standard \ Extraction)
Karl Palmskog (May 27 2020 at 09:35):ah, OK, I already had: (modules :standard \ Extract ... in my theories/dune
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
Karl Palmskog (May 27 2020 at 09:36):should I report it as an issue?
Emilio Jesús Gallego Arias (May 27 2020 at 09:36):It is doing -Q . Buchberger -R . ExtractionPrelude I guess?
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
Karl Palmskog (May 27 2020 at 09:37):yes, I got a "directory remapping" warning
Emilio Jesús Gallego Arias (May 27 2020 at 09:37):in that currently doubly-binding directories is unsupported
Emilio Jesús Gallego Arias (May 27 2020 at 09:37):we could add a note on the dune docs
Emilio Jesús Gallego Arias (May 27 2020 at 09:37):or we could just forgive this case
Emilio Jesús Gallego Arias (May 27 2020 at 09:37):IIANM the OCaml part of Dune is strict with this
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
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?
Karl Palmskog (May 27 2020 at 09:40):I think this is fine as long as documented clearly
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.
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.
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
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
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
Théo Zimmermann (May 27 2020 at 14:06):Wherever you publish it, we could advertise it through the CoqLang Twitter account.
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
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.
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
Emilio Jesús Gallego Arias (May 27 2020 at 14:09):in particular we are makinginclude_subdirs per language
Emilio Jesús Gallego Arias (May 27 2020 at 14:09):etc...
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
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?
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
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.
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.
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.theoriesin 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?
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: Jun 03 2023 at 18:01 UTC