Stream: Coq users

Topic: Notation conflict only when imports in a certain order

Li-yao (Sep 29 2021 at 16:23):

How is it possible that importing things in one order leads to a notation conflict, while importing in the other order does not? And how can I find out where that notation is defined?

From mathcomp Require Import ssreflect.
From VST Require Import floyd.proofauto.
(*
Notation "_ : _" is already defined at level 100 with arguments constr
at next level, constr at level 100 while it is now required to be at level 26
with arguments constr at next level, constr at level 26.
*)

From VST Require Import floyd.proofauto.
From mathcomp Require Import ssreflect.
(* OK *)

Enrico Tassi (Sep 29 2021 at 18:34):

I think it is in ssreflect.v or ssrfun.v, both in coq (not mc, they are loaded transitively).

Enrico Tassi (Sep 29 2021 at 18:35):

To avoid the conflict you should be explicit, since there are defaults which may be different from what the other notation declares. cc @Hugo Herbelin

Guillaume Melquiond (Sep 29 2021 at 19:00):

Coq accepts the following sequence (and rejects the converse one). I have no idea if it is on purpose or a bug:

Notation "x @ y" := (x + y) (at level 26, only printing).
Reserved Notation "x @ y" (at level 100).

Gaëtan Gilbert (Sep 29 2021 at 19:05):

it seems only printing is failing to skip the consistency check

Gaëtan Gilbert (Sep 29 2021 at 19:06):

but since it doesn't add the notation the next command can succeed

Guillaume Melquiond (Sep 29 2021 at 19:12):

But should it actually succeed? It feels like it should not. Because once you do Notation "x @ y" := (x - y)., things become crazy with respect to associativity and levels.

Paolo Giarrusso (Sep 29 2021 at 19:33):

I agree that rejecting both orders seems simpler

Paolo Giarrusso (Sep 29 2021 at 19:40):

or rather: it’s a bug, unless somebody can describe a compelling use-case for the more liberal alternative. “Fewer errors on imports of incompatible notations” does not qualify as “compelling” if the resulting grammar isn’t robust…

Hugo Herbelin (Sep 29 2021 at 20:44):

Enrico Tassi said:

To avoid the conflict you should be explicit, since there are defaults which may be different from what the other notation declares. cc Hugo Herbelin

This is discussed at #6078, #11088, #11657. There was a PR at #6134 but it did not reach the level of preserving compatibility everywhere. Somehow looking for someone courageous to find a solution which works at best...

Alternatives include:

• making progress on #12324 which mostly requires deciding a concrete user syntax for deactivating a notation
• moving the ssreflect notation to a submodule that is then loaded only optionally
• ...

Hugo Herbelin (Sep 29 2021 at 20:54):

Guillaume Melquiond said:

Coq accepts the following sequence (and rejects the converse one). I have no idea if it is on purpose or a bug:

Notation "x @ y" := (x + y) (at level 26, only printing).
Reserved Notation "x @ y" (at level 100).

From memory, I would have said that both orders are accepted since #12950, so that an arbitrary number of printing notations can be given (under the responsability of the user). There might be a bug then.

Last updated: Dec 06 2023 at 14:01 UTC