Stream: Coq users

Topic: Notation conflict only when imports in a certain order


view this post on Zulip 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 *)

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Gaëtan Gilbert (Sep 29 2021 at 19:05):

it seems only printing is failing to skip the consistency check

view this post on Zulip Gaëtan Gilbert (Sep 29 2021 at 19:06):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Sep 29 2021 at 19:33):

I agree that rejecting both orders seems simpler

view this post on Zulip 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…

view this post on Zulip 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:

view this post on Zulip 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: Mar 29 2024 at 07:01 UTC