Consider the following directory/file structure:
. ├── A │ └── M.v ├── B │ └── M.v ├── C │ └── C.v ├── _CoqProject ├── dune ├── dune-project └── Makefile
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?
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
When I set
From DuneDeps.B Require Import M. and used some constant from
C.v, the compilation still worked and had the exact same warning.
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
sure, but since one obvious workaround is to use
-Q, is this something that could be added to Dune in the meantime?
-Q for the current lib?
that seems like a big change I think
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.
If we are talking about
-R/-Q options that's on purpose as users should specify their deps declaratively
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
the bug will eventually be solved
Is there any simple workaround to silence the warnings? I’d honestly be happy with false negatives (maybe not by default)
The bug also shows in coq_makefile by the way, see the bug report
I think the best use of time is to fix it
I have a plan to fix it but it will take some time
by moving all code for loadpahts into a common library
so we remove the current 3 (!) copies Coq has: for coqc, coqchk, and coqdep [and maybe even coqdoc?]
@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
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).
Though, I don't know if you can separate errors and warnings.
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.
@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.
What is the specific warning coqdep is giving?
I'm wondering because coqdep throws some useless warnings sometimes which I think is a bug.
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.
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