Karl Palmskog (Sep 08 2020 at 11:09): Karl Palmskog (Sep 08 2020 at 11:09):Consider the following directory/file structure:
.
├── A
│ └── M.v
├── B
│ └── M.v
├── C
│ └── C.v
├── _CoqProject
├── dune
├── dune-project
└── Makefile
Let's say M.v is empty and C.v is as follows:
From DuneDeps.A Require Import M.
Now, the builds with Dune and coq_makefile are seemingly not equivalent. Dune gives the following warning:
*** Warning: in file C/C.v,
required library M matches several files in path
(found M.v in B and A; used the latter)
... while coq_makefile builds without complaints.
Is this due to the differences in how coq_makefile and Dune invoke coqdep?
Karl Palmskog (Sep 08 2020 at 11:15):the warning also seems to be incorrect, since in B and A; used the latter (referring to A) is always output, regardless of whether A is actually used by coqc.
When I set From DuneDeps.B Require Import M. and used some constant from B in C.v, the compilation still worked and had the exact same warning.
Emilio Jesús Gallego Arias (Sep 08 2020 at 14:40):IIRC the warning is incorrect, and indeed that's a bug on coqdep, as you have noticed. Coq issue is https://github.com/coq/coq/issues/11631
Karl Palmskog (Sep 08 2020 at 14:46):sure, but since one obvious workaround is to use -Q, is this something that could be added to Dune in the meantime?
Emilio Jesús Gallego Arias (Sep 08 2020 at 14:51):Using -Q for the current lib?
Emilio Jesús Gallego Arias (Sep 08 2020 at 14:51):that seems like a big change I think
Karl Palmskog (Sep 08 2020 at 14:54):the problem is that we will likely see more of these disparities between Dune and coq_makefile, in particular if there's no way to send the same options to coqc.
Emilio Jesús Gallego Arias (Sep 08 2020 at 15:01):If we are talking about -R/-Q options that's on purpose as users should specify their deps declaratively
Emilio Jesús Gallego Arias (Sep 08 2020 at 15:01):In this case that's a clear coqdep but [which is by the way triggered even in the stdlib] so IMHO I'm not eager to introduce complex workarounds
Emilio Jesús Gallego Arias (Sep 08 2020 at 15:01):the bug will eventually be solved
Paolo Giarrusso (Sep 08 2020 at 17:25):Is there any simple workaround to silence the warnings? I’d honestly be happy with false negatives (maybe not by default)
Emilio Jesús Gallego Arias (Sep 08 2020 at 17:36):The bug also shows in coq_makefile by the way, see the bug report
Emilio Jesús Gallego Arias (Sep 08 2020 at 17:36):I think the best use of time is to fix it
Emilio Jesús Gallego Arias (Sep 08 2020 at 17:36):I have a plan to fix it but it will take some time
Emilio Jesús Gallego Arias (Sep 08 2020 at 17:36):by moving all code for loadpahts into a common library
Emilio Jesús Gallego Arias (Sep 08 2020 at 17:37):so we remove the current 3 (!) copies Coq has: for coqc, coqchk, and coqdep [and maybe even coqdoc?]
Ali Caglayan (Sep 09 2020 at 08:11):@Paolo Giarrusso I'm not sure if there is a current work around for dune. But Emilio opened an issue on the coq repo recently about having a more configurable output. https://github.com/coq/coq/issues/12923
Ali Caglayan (Sep 09 2020 at 08:12):Ideally, if we could pass flags to coq*, we can get dune to silence it. I believe this functionality is hacked in with most common coq makefiles. At least in the HoTT repo, we just run coq silently (i.e. redirect stdout).
Ali Caglayan (Sep 09 2020 at 08:12):Though, I don't know if you can separate errors and warnings.
Ali Caglayan (Sep 09 2020 at 08:14):Also, there is an option Set Warnings "-notation-overridden" you can add to a .v file. Obviously you would replace -notation-overridden with the specific coq warning you get.
Paolo Giarrusso (Sep 09 2020 at 08:36):@Ali Caglayan Thanks! But I should have clarified : the warnings in question are exclusively from coqdep. Which is called by dune. So I’d like to tell dune to silence all warnings from coqdep.
Ali Caglayan (Sep 09 2020 at 08:37):What is the specific warning coqdep is giving?
Ali Caglayan (Sep 09 2020 at 08:41):I'm wondering because coqdep throws some useless warnings sometimes which I think is a bug.
Paolo Giarrusso (Sep 09 2020 at 08:44):The warnings in question are the ones that this Zulip thread is about, which are indeed a bug — see the top post in https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/Discrepancy.20between.20Dune.20and.20coq_makefile.
Emilio Jesús Gallego Arias (Sep 09 2020 at 13:29):there is not way to silence the coqdep warning other than fixing the bug in coqdep :) the code is not so bad XD if any of you fancy having a look
Last updated: Jun 04 2023 at 23:30 UTC