lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

Sort messages by position when printing

Open Kha opened this issue 2 years ago • 4 comments

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 avatar Jul 19 '23 08:07 Kha

is it time to implement a stable sort on arrays?

+1

leodemoura avatar Jul 20 '23 15:07 leodemoura

CI is not green

leodemoura avatar Jul 24 '23 15:07 leodemoura

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.

kim-em avatar Sep 27 '23 03:09 kim-em

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.

Kha avatar Sep 27 '23 07:09 Kha