Does Lean.Name.cmp do the correct thing?

Stream: lean4

[Moritz Firsching]

It seems like min_imports does not sort correctly, caused by the behavior of Name.cmp, at least if it does not do the same thing you'd get when converting to a String first.
The issue to fix it for min_imports is here: https://github.com/leanprover-community/import-graph/pull/18.
@Jon Eugster suggested to bring it up and potentially change the behavior of Name.cmp?

[Moritz Firsching]

ah, I see just now there is also https://github.com/leanprover/lean4/issues/4944

[Damiano Testa]

The sorting that Name.cmp uses is good if you are trying to figure out, for instance, how many folders you have to cross to get to a file, so I am not so sure that Name.cmp should just look at a string.

[Eric Wieser]

I'd expect it to do a lexicographic comparison on the lists of strings it consists of

[Damiano Testa]

Well, it is currently doing the "graded" lex comparison, right?

[Damiano Testa]

As in, depth in the hierarchy and, within a given depth, lex.

[Eric Wieser]

Right, and I agree with Moritz that this is not the thing you want when sorting imports

[Jon Eugster]

Eric Wieser said:

Right, and I agree with Moritz that this is not the thing you want when sorting imports

That for sure! My question was whether this graded sorting is the right "default" sorting on Name

[Damiano Testa]

Ok, I think that we all agree that imports should be sorted as a string, lexicographically, treating the . as a character. I was mostly arguing that the Name.cmp is not necessarily undesirable as a sorting for Name.

[Eric Wieser]

Damiano Testa said:

treating the . as a character.

I don't agree, that would make `Foo.«A.B» and `Foo.A.B equal. . needs to be treated specially

[Kyle Miller]

What you could do is sort the result of docs#Lean.Name.components, taking advantage of lex order for List

[Damiano Testa]

Note also that docs#getAllModulesSorted, which is the function that mk_all uses to sort imports in Mathlib.lean does indeed sort the strings, not the names (even if the array of strings is called names in the code).

[Eric Wieser]

Kyle Miller said:

What you could do is sort the result of docs#Lean.Name.components

I was expecting this to return docs#Lean.NamePart s

[Kyle Miller]

At least . comes before letters in ASCII, so sorting Name.toString should mostly work, though it could do some odd things with names with french-quoted dots. (@Eric Wieser, Name.toString of Foo.«A.B» is "Foo.«A.B»", so it would be sorted after Foo.A.B)

[Jon Eugster]

For the imports (← getEnv).minimalRequiredModules.qsort (·.toString < ·.toString) instead of .qsort Name.lt should do what we want in that case. (see commit)

Thanks for the comments

[Eric Wieser]

This came as a surprise to me:

import Lean

#guard Lean.Name.cmp `A `ZZZ == .lt
#guard Lean.Name.cmp `A `ZZZ.Z == .lt
#guard Lean.Name.cmp `A.A `ZZZ == .gt -- wat
#guard Lean.Name.cmp `A.A `ZZZ.Z == .lt

docs#Lean.Name.cmp is undocumented, but this is not the order I would expect.

(docs#Lean.Name.lt is consistent with cmp, but I mention it here for future Zulip searches)

[Eric Wieser]

(cc @Damiano Testa for #20908)

[Damiano Testa]

I think that something similar was discussed here as well.

[Eric Wieser]

Thanks, I've merged the threads