Reducing the number of displayed warnings

[affeldt-aist]

[NB(2023/01/11): we keep this issues to remind ourselves to check whether we can change the policy to silence warnings when dropping Coq versions]

This issue records comments that occurred with PR #447 (merged on the occasion of the release of MathComp 1.11).

By default, there are many warnings and we do not want to have too much of them when compiling, in particular for end-users (likely to compile via opam and thus using Makefiles in MathComp subdirectories).

See PR #528 for current policy.

Currently, we silence (see mathcomp/Make):

• "ambiguous paths" warnings
  • Developers may actually want to be aware of them and there is on-going work at the Coq level to reduce their numbers
• ~~"ident" vs "name" warning (from coq 8.13)~~ handled by https://github.com/math-comp/math-comp/pull/856 (merged)
• ~~deprecated-hint-without-locality (from coq 8.13)~~ handled by https://github.com/math-comp/math-comp/pull/891 (merged)
• projection-no-head-constant (from coq 8.?)
• redundant-canonical-projection (from coq 8.?)
• notation-overridden
• ~~-opaque-let: remove when requiring Coq >= 8.19~~ handled by https://github.com/math-comp/math-comp/pull/1382
• ~~-argument-scope-delimiter: fix and remove when requiring Coq >= 8.19~~ handled by https://github.com/math-comp/math-comp/pull/1382
• ~~-overwriting-delimiting-key: appeared in Coq 8.19, unclear how to handle as long as we use the stdlib, removed in 9.0 (c.f., https://github.com/rocq-prover/rocq/pull/19946 ) so just wait until we require Rocq >= 9.0~~ handled by https://github.com/math-comp/math-comp/pull/1382

@CohenCyril @ybertot

EDIT 2021-06-02

[pi8027]

"Undeclared scope" and "duplicate clear" warnings are introduced in Coq 8.10. If we continue to "support at least three recent versions," we can get rid of them after the release of Coq 8.12, which should be soon. So I think it is reasonable to start preparing a PR to get rid of them now. Also, getting rid of "undeclared scope" warnings would be helpful to find some typos such as #380.

[chdoc]

@affeldt-aist Has there been any decision on whether 1.12.0 should maintain compatibility with Coq 8.9 or not? Currently, #599 is milestoned for 1.12.0 and will break compatibility with 8.9.

Should there be a release meta-issue, since milestones cannot have a discussion attached to them.

[CohenCyril]

I know, let's discuss it in the next mathcomp meeting and I will open an issue meanwhile, where I can synthetize which PR/issue may benefit from dropping Coq 8.9.

[ejgallego]

Note that #316 provided a warning-free build. This is easier with dune as it is silent by default, so it may be useful for you folks to get a list of things that I disabled.

[CohenCyril]

I feel I need a crash-course in dune...

[affeldt-aist]

@affeldt-aist Has there been any decision on whether 1.12.0 should maintain compatibility with Coq 8.9 or not? Currently, #599 is milestoned for 1.12.0 and will break compatibility with 8.9.

According to the minutes of meetings in September, this possibility has been mentioned more than twice and nobody disagreed. I am not sure there was a formal decision taken, but I understood that we should maintain at least the last three versions of Coq, which does not contradict dropping 8.9. Am I mistaken?

NB: I realized after writing this comment that it corresponds to a comment by @CohenCyril in the conversation of PR #644

[ejgallego]

I feel I need a crash-course in dune...

Feel free to ask anything in Zulip's stream, dune files are pretty self-explanatory, invocation is dune build $target or dune build which is a shorthand for dune build @all [all targets]

[strub]

Seriously, I like this warnings. This reminds me the old good time when I was compiling an obscure C program on HP-UX in the 90's.

[pi8027]

FTR, my PR coq/coq#13909 reduces 3 pairs of ambiguous paths in ssralg.

@@ -1,30 +1,23 @@
 Warning:
 New coercion path [GRing.subring_closedM; GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing
 [GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed. [ambiguous-paths,typechecker]
 Warning:
 New coercion path [GRing.subring_closed_semi; GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing
 [GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
 New coercion path [GRing.subring_closed_semi; GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing
 [GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed. [ambiguous-paths,typechecker]
 Warning:
 New coercion path [GRing.sdivr_closed_div; GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing
 [GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed. [ambiguous-paths,typechecker]
 Warning:
 New coercion path [GRing.subalg_closedBM; GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing
 [GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed. [ambiguous-paths,typechecker]
 Warning:
 New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing
-[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
-New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM; GRing.smulr_closedN] : GRing.divring_closed >-> GRing.oppr_closed is ambiguous with existing
-[GRing.divring_closedBM; GRing.subring_closedB; GRing.zmod_closedN] : GRing.divring_closed >-> GRing.oppr_closed. [ambiguous-paths,typechecker]
+[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed. [ambiguous-paths,typechecker]
 Warning:
 New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing
-[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
-New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM; GRing.subring_closedB] : GRing.divalg_closed >-> GRing.zmod_closed is ambiguous with existing
-[GRing.divalg_closedZ; GRing.subalg_closedZ; GRing.submod_closedB] : GRing.divalg_closed >-> GRing.zmod_closed. [ambiguous-paths,typechecker]
+[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed. [ambiguous-paths,typechecker]
 Warning:
 New coercion path [GRing.Pred.subring_smul; GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing
 [GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul. [ambiguous-paths,typechecker]
-Warning:
-New coercion path [GRing.Pred.divring_sdiv; GRing.Pred.sdiv_smul; GRing.Pred.smul_mul] : GRing.Pred.divring >-> GRing.Pred.mul is ambiguous with existing
-[GRing.Pred.divring_ring; GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.divring >-> GRing.Pred.mul. [ambiguous-paths,typechecker]