Stream: Dune devs & users

Topic: Discrepancy between Dune and coq_makefile


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 14:51):

Using -Q for the current lib?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 14:51):

that seems like a big change I think

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 15:01):

the bug will eventually be solved

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 17:36):

I think the best use of time is to fix it

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 17:36):

I have a plan to fix it but it will take some time

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 17:36):

by moving all code for loadpahts into a common library

view this post on Zulip 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?]

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Ali Caglayan (Sep 09 2020 at 08:12):

Though, I don't know if you can separate errors and warnings.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Sep 09 2020 at 08:37):

What is the specific warning coqdep is giving?

view this post on Zulip Ali Caglayan (Sep 09 2020 at 08:41):

I'm wondering because coqdep throws some useless warnings sometimes which I think is a bug.

view this post on Zulip 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.

view this post on Zulip 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: Oct 16 2021 at 09:07 UTC