queue

Stream: general

[Johan Commelin]

Hey everyone, if you have a minute to spare, and some experience with mathlib PRs, feel free to help out reviewing!
The top 10 or so PRs of the #queue were last updated more than 2 days ago, and would love to get some feedback.
For the maintainers it's really great help if someone takes a close look, and if everything looks good give it a LGTM comment.
Keep up all the good work!

[Yaël Dillies]

Sorry, I've been giving maintainers lots of work recently :upside_down:

[Arthur Paulino]

I noticed that #queue sorts the PRs by updated-asc. A downside of this sorting is that PRs might get pushed down in the queue by people commenting on it, even if it's a commentary that requires no code change.

That said, what do you guys think about this sort parameter?
sort:commit-desc -- does it work though?

It mitigates two things:

• What I said about comments that require code changes
• Lately added awating-review label even on older PRs (with higher chances of conflicting)

Side-kick idea: use status:success instead of -status:failure to filter out PRs that are still pending

[Yaël Dillies]

The problem is that some pending are actually ready for review. This is the case when they are blocked by other PR but still require attention or when the Github actions bot screws up for some reason.

[Arthur Paulino]

Huh, the sorting that I wanted doesn't seem to work :thinking:

[Johan Commelin]

I like the idea of sorting by commit time.

[Arthur Paulino]

I thought the parameter I suggested worked, but I'm finding some counter examples. And GitHub's page about sorting doesn't seem to say anything about sorting by the date of the last commit :(

[Huỳnh Trần Khanh]

perfect solution: when a PR is ready to review, the author should make a post on the Zulip to beg for reviews!!! we don't have to rely on GitHub's sorting algorithm!

[Johan Commelin]

I certainly wish there was better tooling for this. The Github inbox is pretty worthless. And these sorting options also don't seem to be developed for power users.

[Johan Commelin]

They work fine for hobbyists that receive 10 notifications per week. But I want stuff that can deal with > 100 notifications per day.

[Arthur Paulino]

GitHub's API does provide a rich set of possibilities tho. This URL lists all PRs. Every PR has a commits_url key that leads to data like this. If we ever need something more robust and that's worth the effort, the data is available :+1:

[Huỳnh Trần Khanh]

lol someone rightfully disliked my tongue in cheek suggestion :joy: oh oops what do mathlib maintainers use to identify PRs in need of attention :joy: just #queue?

[Huỳnh Trần Khanh]

ah the GitHub API is pretty simple to use and it supports CORS so :joy: I think we can just code a simple web application to pull data from the API and then sort the pull requests... this shouldn't require any server side code

[Huỳnh Trần Khanh]

Johan Commelin said:

I like the idea of sorting by commit time.

it occurred to me that... https://github.com/leanprover-community/mathlib/actions does exactly that!

[Arthur Paulino]

Aw, it does, but we can't access other parameters like the ones we can in the standard filter, like labels etc

[Andrew Yang]

Is sort:committer-date-asc what you are looking for?

[Johan Commelin]

Huỳnh Trần Khanh said:

what do mathlib maintainers use to identify PRs in need of attention :joy: just #queue?

Mostly the #queue, but also the stream #PR reviews and other pings here on zulip. And the github inbox that I mentioned before, although it's quite a flood of notifications there.

[Arthur Paulino]

Andrew Yang said:

Is sort:committer-date-asc what you are looking for?

I tested it but I could find some counter examples for that ordering too

[Stuart Presnell]

So what ordering are you aiming for? What goes wrong with the ones that you tried?

[Arthur Paulino]

Stuart Presnell said:

So what ordering are you aiming for? What goes wrong with the ones that you tried?

I want the last PRs in the list to be the ones with the most recent latest commit (independently of other updates like comments, labels added/removed etc). I don't understand the ordering of my previous attempts

[Stuart Presnell]

Would it be possible/useful to promote smaller PRs (or those tagged easy) in the queue?

[Johan Commelin]

nah, I think those are merged pretty fast already.

[Arthur Paulino]

Is there a place where #queue is easily/directly clickable?

[Yaël Dillies]

#queue <- here

[Arthur Paulino]

No I mean pinned somewhere so we don't need to type in messages before clicking

[Eric Rodriguez]

yeah that'd be nice, I often find myself searching #queue or just keeping one in my drafts so I can cluck it

[Kevin Buzzard]

I have it bookmarked in my browser

[Yaël Dillies]

Same as Kevin here. I also keep bookmarked the #bors queue.

[Adam Topaz]

Maybe we should add a link somewhere on the community website?

[Arthur Paulino]

Is it possible to add hyperlinks where it says

For discussion of current PRs to mathlib, as well as soliciting help on PRs, ...

(When you click on the stream #PR reviews )

[Arthur Paulino]

The bookmark idea is good too. IDK why it didn't cross my mind

[Kevin Buzzard]

What would one link to in the general stream? Each individual thread has a link in the thread title to the relevant PR (the up-and-right arrow, at least on a computer; I don't think it works on mobile)

[Arthur Paulino]

Hm I didn't understand the question. Not all streams would need links

[Yaël Dillies]

But all streams already do

[Kevin Buzzard]

Arthur I don't understand your question. I wasn't asking a question. My understanding of your question is "why don't we have a link associated to the PR stream". My answer is "what would it link to? Note that individual threads already have links although they can be hard to spot."

[Arthur Paulino]

Ah, I was commenting that we could have useful links on the description of some streams. These descriptions don't show up on the mobile app unless you're in the browsing streams tab. But on the web app the description shows up at the very top of the page when you visit a stream