Inconsistent sorting in Name.cmp

[joneugster]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The sorting of Names (i.e. in Name.cmp) is unexpected.

Context

From PR leanprover-community/import-graph#18

[Zulip]

Steps to Reproduce

import Lean
open Lean

#reduce Name.cmp `M.A `M.B   -- M.A   < M.B (✓)
#reduce Name.cmp `M.A.B `M.B -- M.A.B > M.B (⨯)

Expected behavior: In the second example, I expect M.A.B < M.B

I expected the following comparison:

• Compare first part of the name (M == M)
• Compare second part (A < B) ==> return lt
• ( ... )

Actual behavior:

• Compare length of name (3 > 2) ==> returns gt
• (Compare first part of the name)
• (Compare second part ...)
• ( ... )

Versions

4.11.0-rc1

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[mo271]

zulip discussion on the topic here:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Does.20Name.2Ecmp.20do.20the.20correct.20thing.3F

[Kha]

Triage team agreed on this not being a bug, the function is undocumented and as everything in Lean written for the purposes of Lean. You should create your own ordering function.

[joneugster]

ok, thanks for looking at it!