Skip to content

fix: sort names alphabetically in Imports.Pretty - #171

Merged
kim-em merged 2 commits into
leanprover-community:mainfrom
thorimur:pretty-import-cmp
Oct 5, 2026
Merged

kim-em merged 2 commits into
leanprover-community:mainfrom
thorimur:pretty-import-cmp

Conversation

@thorimur

@thorimur thorimur commented Oct 5, 2026

Copy link
Copy Markdown
Collaborator

The previous comparison used Name.cmp, which considered names with fewer components to come before those with more. This leads to imports from the same library potentially not being grouped together.

Ideally, we would sort lexicographically from the name root, but converting to a string then comparing handles most cases, is compiled, and saves us complexity.

@kim-em
kim-em merged commit d058217 into leanprover-community:main Oct 5, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants