If one builds mathcomp locally there are plenty of warnings. This concerns:
Warning: Declaring a scope implicitly is deprecated;... Warning: This notation contains Ltac expressions: it will not be used for printing.
The former is everywhere, the latter only in
ssrAC.v. Am I right to assume that the reason why the implicit scope warning is not disabled is that for Coq
<=8.9, passing the warning causes an error and that
coq-8.9is still supported. Hence the warning cannot be fixed by explicitly declaring the scopes?
I'm asking because these warning increase the likelihood of missing warnings one introduced oneself while creating a pull request. This happened to me at least once already.
For what it's worth, the Ltac warning can be resolved by sprinkling a number of
(only parsing) over said file (should I PR that too?). Then one can get a warning free build by invoking
COQEXTRAFLAGS="-w -undeclared-scope" make -j9
Deprecation warnings should be fixed in priority though, the implicit scope declaration being an example.
Deprecated stuff is likely to be removed in the future, so better prepare for it in advance...
Well, one cannot (easily) fix a deprecation warning while still supporting versions prior to the one that introduced the means to do so. Mathcomp still supports
Declare Scope was only introduced in
@Christian Doczkal yes indeed you are right. However, I think it would be about time to consider dropping support for Coq < 8.10 for the next release of mathcomp 1.13.0. In particular it has to be if we merge math-comp/math-comp#501, which I am a strong advocate for...
Well, there are two issues here. The support for 8.9, which luckily is about to end; were you referring to the next release (1.12.0) or indeed to 1.13.0? Then there is the general issue of not being able to disable deprecation warnings one cannot do anything about. Maybe future versions of coq could silently discard unknown warning switches. Otherwise, mathcomp could test for the version of coq and configure the warnings accordingly, but that requires a bit of makefile programming.
@Christian Doczkal Why do you say that you cannot disable deprecation warnings? It is safe to use
Set Warnings "-foo". even when
foo is not defined.
Théo Zimmermann said:
Christian Doczkal Why do you say that you cannot disable deprecation warnings? It is safe to use
Set Warnings "-foo".even when
foois not defined.
Hmm, I was talking about the corresponding command line switches. But I just added
-arg -w -arg -undeclared-scope -arg -w -arg -notation-incompatible-format -arg -w -arg -foobar
Make file of mathcomp and this leads to a build without warning. So (assuming
-foobar is not a known switch) unknown warning switches are already silently discarded. I should have checked this. Now I wonder why the
-arg -w -arg -undeclared-scopewasn't added to that file around the time 8.10 was released. :thinking:
@Théo Zimmermann Thanks for pointing that out.
Last updated: Feb 09 2023 at 03:06 UTC