Karl Palmskog (Jul 27 2020 at 13:42): Karl Palmskog (Jul 27 2020 at 13:42):I just upgraded a bunch of projects that use MathComp libraries to 8.12.0, and all I get are tons of these warnings:
Notation "[ rel _ _ : _ | _ ]" was already defined with a different
format in scope fun_scope. [notation-incompatible-format,parsing]
Is this to be expected? What kind of refactoring should be done to fix, or should everyone just ignore these?
Enrico Tassi (Jul 27 2020 at 13:58):I don't really know. Looking at the milestone, it could be this PR that introduced the warning (CC @Hugo Herbelin) https://github.com/coq/coq/pull/10832
Hugo Herbelin (Jul 29 2020 at 12:56):@Karl Palmskog: This is indeed probably related https://github.com/coq/coq/pull/10832. Do you have examples of lines which produce the warning?
Karl Palmskog (Jul 29 2020 at 13:33):@Hugo Herbelin I'll try to minimize an example later today, basically I saw this for large code bases and didn't debug where it occurred
Karl Palmskog (Aug 11 2020 at 10:01):I dropped the ball on this, but I can now confirm that in 8.12.0, basically every Require of all_ssreflect and the like will raise:
Notation "[ rel _ _ : _ | _ ]" was already defined with a different format in scope fun_scope.
[notation-incompatible-format,parsing]`
It's basically like notation-overriden in that it must be ignored in all MathComp projects on 8.12.
Christian Doczkal (Aug 11 2020 at 10:28):I just had a look, it is caused by line 43 in ssrbool.v (in mathcomp). The file distributed with Coq does this:
Reserved Notation "[ 'rel' x y : T | E ]" (at level 0, x ident, y ident,
format "'[hv' [ 'rel' x y : T | '/ ' E ] ']'").
Notation "[ 'rel' x y : T | E ]" :=
(SimplRel (fun x y : T => E%B)) (only parsing) : fun_scope.
While the line in mathcomp's ssrbool.vreads:
Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T => E%B)) (at level 0,
x ident, y ident, only parsing) : fun_scope.
So, yes, the formats are indeed different. However, one cannot simply add a format string to that line, because format strings are ignored for only parsing notations.
Christian Doczkal (Aug 11 2020 at 10:38):Indeed, copying the lines from Coq file to the file in mathcomp gets rid of the warnings. So it appears that (a) repeating Reserved Notation is benign and (b) one can have an only parsing notation with a format string if one declares the format ahead of time using Reserved Notation. :unamused:
Christian Doczkal (Aug 11 2020 at 10:45):I'm in inclined to say that the warning can safely be ignored as we are taking about an only parsing notation. Also, I would say the proper fix is to remove the format string in the file shipped with Coq. @Cyril Cohen , do you agree?
Enrico Tassi (Aug 11 2020 at 10:58):CC @Maxime Dénès which was cleaning up some notations code recently. This looks like a warning one cannot easily fix (so it should not be a warning imo).
Karl Palmskog (Aug 11 2020 at 11:01):thanks for tracing this problem. Let me know if you want me to report issues (to either Coq or MathComp or both).
Cyril Cohen (Aug 11 2020 at 12:09):Christian Doczkal said:
I'm in inclined to say that the warning can safely be ignored as we are taking about an
only parsingnotation. Also, I would say the proper fix is to remove the format string in the file shipped with Coq. Cyril Cohen , do you agree?
If it does not trigger a warning/error, I would make sure the contents of ssrbool.v are identical for this particular notation.
Indeed, the rationale of mathcomp ssrbool.v is to make up for the lag in integration in Coq and is bound to disappear, so content should not be removed from Coq. I think it is interesting to keep the format directive, just in case someone would like to temporarily enable printing, so I would rather opt for adding the Reserved Notation directive in mathcomp ssrbool.v.
Finally, I do not understand how this is not a bug of Coq, the format is not specified, so why is it not drawn from the Reserved Notation directive? Is it the case that if one provides a subset of what of was already declared by Reserved Notation, what is left undeclared is made up from scratch? If so is it really the intended behaviour? If not, why does it trigger a warning?
Christian Doczkal (Aug 11 2020 at 12:37):I just created: https://github.com/math-comp/math-comp/pull/552
Hugo Herbelin (Sep 15 2020 at 10:13):Sorry, I see only now the follow-up to this discussion. Note that the spurious warning about a format with only parsing notation is fixed in https://github.com/coq/coq/pull/12949, so this should help.
Last updated: May 31 2023 at 02:31 UTC