duplicated namespace

Stream: mathlib4

[Johan Commelin]

Don't duplicate folder names :rofl: :joy: :cartwheel:

/- The `dupNamespace` linter reports:
DUPLICATED NAMESPACES IN NAME: -/
-- Mathlib.Algebra.Algebra.Basic
 #check Mathlib.Algebra.Algebra.Basic._auxLemma.8.{u_2, u_1} /- The namespace Algebra is duplicated in the name -/

[Yury G. Kudryashov]

Who's going to fix the linter?

[Yury G. Kudryashov]

Currently, this is the only roadblock for Algebra.Algebra.Basic which is the roadblock on the path to metric spaces.

[Yury G. Kudryashov]

I mean, if nobody else volunteers, then I'll try to do it.

[Johan Commelin]

@Yury G. Kudryashov Can you set_option linter.dupNamespace false at the top of the file, with a porting note?

[Johan Commelin]

Or maybe attribute [nolint dupNamespace] «Mathlib.Algebra.Algebra.Basic._auxLemma.8» works?

[Yury G. Kudryashov]

I see that the linter is in Std, so I'll try one of these workarounds instead.

[Yury G. Kudryashov]

Filed as std4#103

[Yury G. Kudryashov]

attribute [nolint ..] .. doesn't work. It says "unknown constant '«Mathlib.Algebra.Algebra.Basic._auxLemma.7»'"

[Yury G. Kudryashov]

Probably, it's hard to set attributes on private lemmas.

[Yury G. Kudryashov]

And set_option is probably local to a file it won't affect #lint run in the CI.

[Reid Barton]

Hmm, it definitely works for the uppercase align linter

[Reid Barton]

So I think it should work for this one too.

[Yury G. Kudryashov]

What works?

[Yury G. Kudryashov]

set_option?

[Yury G. Kudryashov]

It seems that ther is no option linter.dupNamespace

[Reid Barton]

maybe you need to import it? Or maybe it is a different kind of linter. I don't really understand how these work

[Yury G. Kudryashov]

It seems that support for set_option linter.* false is not a built-in feature. Some other linters have explicit ifs to enable it.

[Reid Barton]

Does the attribute [nolint ..] .. work without the french quotes? They should definitely not be there

[Reid Barton]

But I'm not sure whether it will actually work without them

[Reid Barton]

Does it help to put @[nolint ..] on the main definition itself?

[Reid Barton]

assuming there is one?

[Yury G. Kudryashov]

To do this, I need to figure out which definitions generate these lemmas.

[Yury G. Kudryashov]

Without french quotes, it says "unknown constant 'Mathlib.Algebra.Algebra.Basic._auxLemma'"

[Reid Barton]

What if you leave off the .8

[Yury G. Kudryashov]

So, it doesn't treat ".7" as a part of the name.

[Reid Barton]

oh I guess that would do the same thing

[Reid Barton]

right

[Yury G. Kudryashov]

And I can't even #print this lemma to guess where it came from.

[Mario Carneiro]

names with numbers are a pain to write explicitly

[Reid Barton]

It's probably one of the ones that uses simp... if that helps

[Reid Barton]

I assume it probably doesn't help.

[Reid Barton]

I also doubt that this would fix it anyways

[Reid Barton]

So I guess we just fix the linter.

[Johan Commelin]

Another hacky workaround would be to rename the folder to Algebra/Algebra_ for now, and leave a porting note in Algebra/Algebra_/README.md.

[Johan Commelin]

And then we can fix the linter without blocking PRs in this directory.

[Yury G. Kudryashov]

Can we globally disable this linter for now?

[Yury G. Kudryashov]

Probably no because it has no set_option

[Reid Barton]

I assume it's like a one line if \not n.isInternal then fix to the linter

[Reid Barton]

But yeah, those would be options too

[Yury G. Kudryashov]

Yes.

[Mario Carneiro]

here's a hack to print declarations with internal names:

import Lean
import Mathlib.Tactic.RunCmd

open Lean
run_cmd
  Elab.Command.elabCommand
    (← `(#print $(mkIdent (.num `Mathlib.Algebra.Algebra.Basic._auxLemma 8))))

[Yury G. Kudryashov]

I get the same "unknown constant" error

[Mario Carneiro]

you also need to have that downstream of the definition

[Yury G. Kudryashov]

Can you checkout !4#2244 and try?

[Reid Barton]

and then, change #print to attribute [nolint ..]

[Yury G. Kudryashov]

I'm trying it at the end of the file.

[Mario Carneiro]

But at the risk of pointing out the obvious: this really seems like a true positive to me. Who thought that it would be a good idea to have an Algebra/Algebra/ folder?

[Reid Barton]

I guess whoever decided it would be a good idea to have a type of algebraic structure called an algebra?

[Yury G. Kudryashov]

Adding nolint dupNamespace attr to a lemma that generates the aux lemma doesn't help

[Johan Commelin]

@Mario Carneiro We should have Algebra/Module, since we have _root_.Module. But we also have _root_.Algebra...

[Mario Carneiro]

I get it, but that doesn't make it any less confusing to everyone who runs across it

[Yury G. Kudryashov]

I suggest that we don't rename a folder mid-port

[Mario Carneiro]

I think all the aspects which make the dupNamespace linter worth linting still apply

[Johan Commelin]

I remember being terribly confused about what an algebra was in my 2nd year. It wasn't explained in my lecture notes on ring theory, which was called "Algebra II"... :rofl:

[Reid Barton]

I'm not sure what other name would be less confusing

[Reid Barton]

I mean short of renaming Algebra.X to Algebra.Xs or something

[Reid Barton]

or Algebra to GA (is that the right code)

[Reid Barton]

I think it would be fair to say that the only redeeming feature of Algebra.Algebra_ is to satisfy the linter

[Yury G. Kudryashov]

I think that the way to go before the port is done is to add an option linter.dupNamespace.

[Johan Commelin]

Reid Barton said:

or Algebra to GA (is that the right code)

Probably RA: https://arxiv.org/list/math.RA/recent

[Mario Carneiro]

Aha, you need to use mkCIdent instead of mkIdent for my hack to work

[Mario Carneiro]

unfortunately the declaration has no declaration range so it doesn't actually help that much for locating who added it

[Thomas Murrills]

Why is there a folder called Algebra within Algebra in the first place? What’s intended to go in Algebra/Algebra that shouldn’t just go in Algebra? 🤔

[Yury G. Kudryashov]

How do you run it in a loop?

[Yury G. Kudryashov]

We have Algebra/AlgebraicStructure folders.

[Yury G. Kudryashov]

E.g., Algebra/Group, Algebra/Module, Algebra/Algebra.

[Thomas Murrills]

It looks like the files in Algebra/Algebra talk about a range of algebraic structures rather than just the most general notion of “an algebra”. Is that right?

[Thomas Murrills]

Or wait. Is it that they talk about “algebras over _”?

[Yury G. Kudryashov]

Pushed a workaround

[Yury G. Kudryashov]

Thanks Mario.

[Reid Barton]

Back in the day, algebras were the only algebraic structures around.

[Reid Barton]

Maybe the abstract concept of a group is from around the same time

[Thomas Murrills]

I’d propose either Algebra/Algebras or Algebra/AlgebraOver as a rename (post-port), just for clarity—the duplication of folder names is a bit awkward even aside from linter errors imo! 🙃 (Either that or nest all the algebraic structures in a Structures folder.)

[Mario Carneiro]

(I agree this isn't really the time to be making folder hierarchy changes, but we should probably keep it in the back of our minds.)

[Mario Carneiro]

The present issue is very trivially fixed in the linter

[Mario Carneiro]

Although on the topic of duplicated namespaces, there are some fun section names in the file: CommSemiringSemiring, CommRingRing, CommSemiringCommSemiring

[Yury G. Kudryashov]

For now, I pushed a workaround, and !4#2244 is ready for review again.

[Yury G. Kudryashov]

I guess, it is "TCAssumptionOnRTCAssumptionOnA"

[Mario Carneiro]

Mathlib.Algebra.Module.Submodule.Lattice has a lot of nouns in it

[Thomas Murrills]

Is there a “post-port tracking issue”? Might be helpful if we want to remember to come back to little things like this.

[Mario Carneiro]

I thought there was a tag for this

[Thomas Murrills]

Oh yes, there is: after-port. I wonder if it would reduce friction to quickly edit a common issue with ideas instead of making a standalone issue for every thing we might want to address, though.

[Thomas Murrills]

(I can make one if people think there’d be any benefit.)

[Yury G. Kudryashov]

I think that we'll fix things one by one after port, so it makes sense to have separate issues.

[Mario Carneiro]

fixed in std4

[Yury G. Kudryashov]

Should we try to update std4 now, or merge !4#2244 with a workaround first?

[Thomas Murrills]

Yury G. Kudryashov said:

I think that we'll fix things one by one after port, so it makes sense to have separate issues.

We’d still have separate issues, I’m just saying we might want to track them all and create quick precursors to them in a common issue. (The GitHub checklist even lets you create an issue straight from a checklist entry when you’re ready to do so.)

for example, aren’t there more things—especially minor things—that have been discussed on zulip as “for after the port” than there are after-port issues? If not, then nevermind…but, so far Yury is the only one who’s been industrious enough to actually create any after-port issue. 🙃 That’s why I thought there might be value to reducing the friction here.