Skip to content

Sort messages by position when printing#2335

Draft
Kha wants to merge 1 commit into
leanprover:masterfrom
Kha:sort-msgs
Draft

Sort messages by position when printing#2335
Kha wants to merge 1 commit into
leanprover:masterfrom
Kha:sort-msgs

Conversation

@Kha

@Kha Kha commented Jul 19, 2023

Copy link
Copy Markdown
Member

As exhibited in #2276 but already encountered many times before I believe, so it is high time to make the message ordering more deterministic. Unfortunately there is some perhaps unwanted reordering for messages at the same position as shown in the diff below. If we agree to not reorder messages at the same position, is it time to implement a stable sort on arrays?

@Kha Kha added the awaiting-review Waiting for someone to review the PR label Jul 19, 2023
@leodemoura

Copy link
Copy Markdown
Member

is it time to implement a stable sort on arrays?

+1

@leodemoura leodemoura added awaiting-author Waiting for PR author to address issues and removed awaiting-review Waiting for someone to review the PR labels Jul 24, 2023
@leodemoura

Copy link
Copy Markdown
Member

CI is not green

@kim-em

kim-em commented Sep 27, 2023

Copy link
Copy Markdown
Collaborator

Does this just need all the tests cleaned up to match the new order? Or is this waiting on something else? I can't quite decipher the intention from the above.

@Kha

Kha commented Sep 27, 2023

Copy link
Copy Markdown
Member Author

It's waiting on a stable sort implementation. I haven't encountered the original issue since so I haven't made this PR a priority.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-author Waiting for PR author to address issues stale

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants