Zulip Chat Archive

Stream: mathlib4

Topic: Alignment not firing


Patrick Massot (Dec 13 2022 at 14:04):

Despite https://github.com/leanprover-community/mathlib4/blob/c8da4dbf7ff19167b9e9b2c268b187f0494ef4c5/Mathlib/Logic/Function/Basic.lean#L82, the name isn't aligned at in unop_injective.Ne https://github.com/leanprover-community/mathlib3port/blob/25aba9a00dd0c7af7df362a275829ce34ac8dd48/Mathbin/Algebra/Ring/Opposite.lean#L92. Is this a known issue because of dot notation?

Chris Hughes (Dec 13 2022 at 14:07):

I've seen this a lot

Kevin Buzzard (Dec 13 2022 at 17:24):

Yes I've seen this quite a bit too. My memory is that Mario just said that the autoporter didn't have enough information so we had to just fix this stuff manually.

Mario Carneiro (Dec 13 2022 at 17:25):

yes, there is no easy fix. If it becomes a sufficiently high priority I can try for the hard fix though

Floris van Doorn (Dec 13 2022 at 17:27):

I think it's quite high priority, it happens quite a lot.

Luckily there is a workaround that is not too bad. If you see (someDef : SomeType).some_lemma you can search all files / grep for SomeType.some_lemma, and you'll likely find the #align SomeType.some_lemma SomeType.some_other_lemma_name line.

Chris Hughes (Dec 19 2022 at 11:40):

Align seems to have a lot of problems with namespaces. I was porting a file with a lot of lemmas starting with equiv.set and in the Mathlib3port file when the Equiv namespace was open, all the lemmas that started equiv.set, and referred to as set._ because the equiv namespace was open were still set._ with uncapitalised set.

Chris Hughes (Dec 19 2022 at 12:53):

To be honest, I'm not sure align fires at all on lemmas inside a namespace when they're referred to without the namespace because the namespace is open.


Last updated: Dec 20 2023 at 11:08 UTC