Zulip Chat Archive
Stream: PR reviews
Topic: mathlib_stats #5
Bolton Bailey (Jul 29 2022 at 20:30):
I'm not sure anyone looks at this repo regularly but https://github.com/leanprover-community/mathlib_stats/pull/10 has been open a while. It seems like a nice way to clean up the contributor table on the mathlib stats page by removing the "number by commits" column and adding a simple numbering of the rows on the left-hand side.
Eric Wieser (Jul 29 2022 at 21:40):
I had a quick look at it, but I'm not sure whether it's useful
Eric Wieser (Jul 29 2022 at 21:41):
Was the intent to have the row numbers be fixed in position, or just a shorter way to show the existing information?
Eric Wieser (Jul 29 2022 at 21:43):
Eric Wieser (Jul 29 2022 at 21:43):
(that's with the new column added but without the old column removed)
Bolton Bailey (Jul 30 2022 at 14:10):
The intent is partially to have the row numbers be fixed in position, to be able to sort by whichever column you want and see the order numbers for that column, as well as to save a bit of space. I don't like that it seems to be sorting by author name first, I would prefer it to stay sorted the same way as it is now.
Bolton Bailey (Jul 30 2022 at 15:48):
@Eric Wieser is it sorting by author name because you clicked on it, or was that the default?
Eric Wieser (Jul 30 2022 at 15:52):
Ah sorry, the sorting was indeed prompted by me clicking the header
Eric Wieser (Jul 30 2022 at 15:52):
Can you include that intent in the PR description? I think I just misunderstood the premise.
Bolton Bailey (Jul 30 2022 at 15:53):
Yeah, ok, I'll add about that
Bolton Bailey (Jul 30 2022 at 16:01):
I guess I can't change the description because I didn't author the PR myself, but I left a comment explaining my rationale for trying to get this change through.
Last updated: Dec 20 2023 at 11:08 UTC