Stream: math-comp devs

Topic: warnings when buidling locally

Christian Doczkal (Aug 11 2020 at 13:20):

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

Pierre-Marie Pédrot (Aug 11 2020 at 13:22):

Deprecation warnings should be fixed in priority though, the implicit scope declaration being an example.

Pierre-Marie Pédrot (Aug 11 2020 at 13:22):

Deprecated stuff is likely to be removed in the future, so better prepare for it in advance...

Christian Doczkal (Aug 11 2020 at 13:25):

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 coq-8.9 and Declare Scope was only introduced in 8.10.

Pierre-Marie Pédrot (Aug 11 2020 at 13:25):

Fair enough.

Cyril Cohen (Aug 11 2020 at 14:52):

@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...

Christian Doczkal (Aug 11 2020 at 15:08):

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.

Cyril Cohen (Aug 11 2020 at 16:12):

1.12.0

Théo Zimmermann (Aug 11 2020 at 19:44):

@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.

Christian Doczkal (Aug 11 2020 at 20:36):

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 foo is 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

To the 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: Dec 05 2023 at 06:01 UTC