Local notation conflict

Stream: mathlib4

[Anatole Dedecker]

I'm having a small problem in mathlib4#1205: Order.Chain and Order.Antichain both declare local infixl:50 " ≺ " => ..., and I get an error in Mathlib.lean saying that it can't import Order.Chain because environment already contains '«term_≺__3»._closed_6._cstage2'. Note that it doesn't happen if any of the two files import the other, so I guess the problem is that both file come up with the same auto-generated name because they don't know about the other file, but that will be very annoying in the long run. Is there a known fix?

[Mario Carneiro]

name the notations

[Sebastian Ullrich]

But also that sounds kind of like a Lean 4 bug. I don't recall off the top of my head whether we should/can use more private there.

[Heather Macbeth]

I hit this problem (conflicts of supposedly local notation) again in mathlib4#1254. @Sebastian Ullrich You suggested before that this should be considered a Lean 4 bug; should I open an issue for it?

[Reid Barton]

Yes, I think so

[Reid Barton]

Also add a porting note with a link to the issue to whatever workaround you end up using

[Anatole Dedecker]

Naming the notation works fine, but I had a hard time finding the syntax for that :sweat_smile:

[Heather Macbeth]

https://github.com/leanprover/lean4/issues/2000

[Heather Macbeth]

I'll supplement mathlib4#1254 with porting notes referencing the issue in all the files mentioned in this thread.