Karl Palmskog (Dec 23 2023 at 18:06): Karl Palmskog (Dec 23 2023 at 18:06):In Coq 8.19+rc1, I get the following warning when I use Dune extraction:
File "./Extract.v", line 20, characters 0-58:
Warning: Setting extraction output directory by default to
"path/to/stalmarck/_build/default/src". Use
"Set Extraction Output Directory" to set a different directory for extracted
files to appear in. [extraction-default-directory,extraction,default]
I guess the only way to get rid of this in Dune is to suppress the warning. But shouldn't the option Set Extraction Output Directory be set automatically by Dune instead if the Coq version is >= 8.19? Should I open an issue?
Emilio Jesús Gallego Arias (Dec 24 2023 at 16:07):I didn't follow the discussion about the output directory, but I'm not sure this warning makes sense.
Karl Palmskog (Dec 24 2023 at 17:36):regardless of whether the warning makes sense, anyone who uses Dune+extraction+8.19 will soon experience it, so I think there needs to be a decision on what to do:
Karl Palmskog (Dec 24 2023 at 17:37):happy to open issue about it in what might be considered the right place
Emilio Jesús Gallego Arias (Dec 24 2023 at 19:29):Well, if we determine the warning not to make sense, I guess what to do is affected
Emilio Jesús Gallego Arias (Dec 24 2023 at 19:29):It seems to me the first thing to determine is that; I'm not sure I understand what "regardless" means there
Karl Palmskog (Dec 24 2023 at 19:50):changing the warning in Coq for 8.19.0 seems unfeasible, so a Coq PR will only be shipped in 8.19.1 or 8.20.0. It also requires persuading other Coq devs that changing the warning is something that should be done. Meanwhile, changing Dune or suppressing the warning can be done independently.
Gaëtan Gilbert (Dec 24 2023 at 22:13):if testing the rc leads to a decision that the warning is bad it can be changed in 8.19.0
Karl Palmskog (Dec 25 2023 at 08:42):personally I have no problem with the warning as such, it may be helpful for people doing plain extraction without Dune.
but Dune extraction is supposed to have a layer to handle directory stuff, so actually using Set Extraction Output Directory then is probably a terrible idea. And thus the warning will be shown for every Dune build unless using -w
Karl Palmskog (Dec 25 2023 at 08:43):are lots of people except me using Dune-based extraction? Probably not
Emilio Jesús Gallego Arias (Dec 27 2023 at 00:25):I think the decision about the warning is orthogonal to the build system at use. I don't see how the warning is useful either to people not using Dune.
Let's take a regular Coq project, not using Dune, that was working OK in 8.18; what are the project devs supposed to do with the warning?
Why the behavior in 8.18 is not fine anymore in 8.19?
Emilio Jesús Gallego Arias (Dec 27 2023 at 00:26):@Karl Palmskog as the warning seems dubious to me, let's first decide the fate of the warning. Once that is settled, we can have Dune disable the warning in 8.19 if conveninet.
Karl Palmskog (Dec 27 2023 at 08:32):for a regular Coq extraction project using a make-based build, at least the warning tells you where extracted files end up, since this will be different depending on how coqc is invoked
Karl Palmskog (Dec 27 2023 at 11:49):my guess for how the warning is meant to work:
Set Extraction Output Directory, the coqc directory determines the extraction file output dir Ali Caglayan (Dec 27 2023 at 14:40):Once people start setting extraction directories in their Coq files however, it makes it very tricky for us to configure that from Dune. We can set the extraction directory by passing the option manually to coqc, however this doesn't scale well and means people might override it causing breakage.
Paolo Giarrusso (Dec 27 2023 at 15:10):Indeed, why's this a setting instead of just a command-line option?
Karl Palmskog (Dec 27 2023 at 16:26):I never worked on this PR, but I can see that one might want to have a large file with Extraction directives, where each command results in a file in a different directory. I don't think this could be done easily with a command-line option.
My view is that Dune-based extraction (where Dune takes care to check that you precisely generate the modules mentioned in a prelude in the directory where the dune file resides) is the only feasible alternative for large-scale extraction projects, but for less serious projects, people might like the flexibility of a setting.
Paolo Giarrusso (Dec 27 2023 at 16:57):The rationale in https://github.com/coq/coq/pull/16126 seems "plugins can't add command-line options", but https://github.com/coq/coq/pull/17392 would seem to address that
Paolo Giarrusso (Dec 27 2023 at 17:00):Maybe your use-case for a setting makes sense, but at least you'd want some way for dune to forbid such commands via some option..
Emilio Jesús Gallego Arias (Dec 27 2023 at 18:34):The thing is that for non-dune extraction projects, it seems to me that the current behavior of using the directory is "reasonable"
Emilio Jesús Gallego Arias (Dec 27 2023 at 18:34):so that's why I'm a bit puzzled by the warning in the first place, but indeed I will re-read the discussion
Emilio Jesús Gallego Arias (Dec 27 2023 at 18:35):This is really usability stuff, in my experience is pretty tricky to get right!
Karl Palmskog (Dec 27 2023 at 18:37):usability is one thing, but each choice in how to implement a feature seemingly comes with a myriad of consequences
Emilio Jesús Gallego Arias (Dec 27 2023 at 18:38):Indeed, but whether to show a warning in this case is more of a UI thing I think
Ali Caglayan (Dec 28 2023 at 16:13):I think the better option would be to remove the warning for the next release since it is not very useful nor recommended for every project and the -output-directory option seems like a suprior design.
Last updated: Oct 13 2024 at 01:02 UTC