queueboard

Stream: mathlib4

[Johan Commelin]

In the past few weeks, @Michael Rothgang and I have been chipping away at a prototype review dashboard that should hopefully get rid of some bottlenecks in the review process for mathlib.
We are far from done, but the prototype is already at a stage where I regularly use it to find PRs that I want to review.

Here is the dashboard: https://jcommelin.github.io/queueboard
And here is the repo: https://github.com/jcommelin/queueboard

There are several ideas about how to improve the UX: see the open issues.
But I would be very happy to hear about more ideas, feel free to create more issues with feature requests.

Furthermore I would be happy to get some help. If you enjoy communicating with Github via one of its API then your help is particularly welcome. Currently there is a script pr_info.sh that tries to scrape as much info as possible from github about a given PR. Here is a concrete todo that I would like help with:

• The data should include all information about CI statuses for all the commits that are part of the PR.

[Michael Rothgang]

Let me cross-post the following from the private reviewer stream, to highlight some new features this dashboard gained over the past days. If you used this already, perhaps you'll find a new feature useful. Otherwise, feel free to take this as a guided tour of some new features :-)

What happened recently on the review dashboard prototype

Changes on the user experience side

• the dashboard now links to the github repository, and vice versa
• all dashboard headings are hyperlinks now: you can right-click on them and to determine the link to this dashboard
• when hovering over each section, you see an explanation which PRs are included in it
• some columns of each dashboard also have an explanation. (Don't remember if the comment bubble is the number of all commenta or just of review comments? Hover over it to find out.)

• added a table of contents, with quick links to each part
  Clicking on these jumps within the page: to open a dashboard in a new tab, ... open the link in a new tab (using e.g. middle-click or right-click -> open link in a new tab).

• you can now filter each list PRs by typing into the "search" box on the top right of each dashboard
  This will restrict to the PRs containing the given word in their title or labels. To find all PRs whose title mentions "unique", search for "unique". To find all t-linter PRs, searching for "t-linter" will do. (It would also find PRs with t-linter in the title, but these are extremely rare.)

New features

• added a new dashboard, of easy PRs on the review queue

• added a new dashboard with PRs which "just need a merge": except for a merge conflict, they match the review queue
  (If you're looking for something quick to do, pinging such a PR could be useful to bring it back on the review queue.)

• added a dashboard for PRs waiting for a decision (currently just five of them), and another for contradictory labels (just one)

• added an overview section, classifying the ~1000 open PRs into states like "waiting for review", "waiting for the author", "blocked on another PR", "work in progress", "merge conflict" and others. If you ever wondered where all these PRs went, now you can find out!

  • this page links to the relevant dashboards (where applicable)
  • there is also a pie chart showing the proportion of the respective PR categories (contributed by @Jon Eugster)

In progress/hopefully coming soon

• take CI status into account when determining PR's status: your help is welcome here

• update the dashboard in (closer to) real time: currently, the webpage updates about every ~15 minutes
  Making this change requires some changes to the underlying infrastructure, by caching information about pull requests.

• compute a better estimate for "when was this PR's status really changed". Github's "last updated" is misleading, it includes events which are not relevant for this purpose. For instance, tweaking a PR description, labelling a PR by its area or a merge conflict (resolved quickly) all mark a PR as "recently changed", fooling the heuristics of the current #queue.

• determine "how long is PR X waiting for review in total"
  This and the previous item are available in proof of concept stage: this can be computed for individual PRs automatically. Exposing this in the dashboard may require the infrastructure above.

[Jon Eugster]

Michael Rothgang said:

added a new dashboard with PRs which "just need a merge": except for a merge conflict, they match the review queue
(If you're looking for something quick to do, pinging such a PR could be useful to bring it back on the review queue.)

I noticed that the PRs with just a merge conflict queue also has some PRs with labels like "await-zulip", "help-wanted", "please-adopt". Did you mean to filter these PRs out?

(EDIT) Fix: queueboard#49

[Johan Commelin]

I modified the query so that it now includes CI info for each commit of a PR.

[Mario Carneiro]

Suggestion (queueboard#50): can we have a page on the queueboard website where you give it a PR number and it tells you why it's not on the queue? Maybe presented as a list of checkboxes so that authors can learn what they need to do to get their PRs reviewed

[Michael Rothgang]

Mario Carneiro said:

Suggestion (queueboard#50): can we have a page on the queueboard website where you give it a PR number and it tells you why it's not on the queue? Maybe presented as a list of checkboxes so that authors can learn what they need to do to get their PRs reviewed

That is a great idea and shouldn't be hard to implement.
I can to do that in the first week of October. (Until end of this month, I may have little or no Lean time.)

[Michael Rothgang]

Jon Eugster said:

Michael Rothgang said:

added a new dashboard with PRs which "just need a merge": except for a merge conflict, they match the review queue
(If you're looking for something quick to do, pinging such a PR could be useful to bring it back on the review queue.)

I noticed that the PRs with just a merge conflict queue also has some PRs with labels like "await-zulip", "help-wanted", "please-adopt". Did you mean to filter these PRs out?

(EDIT) Fix: queueboard#49

I deliberately made that dashboard's query match the criteria for #queue: that does include PRs which are labelled awaiting-zulip or help-wanted. I don't mind strongly which way this is decided, but I would prefer if this were consistent.

(Bonus points for updating the classification of PRs accordingly. I can do that in October.)

[Johan Commelin]

Idea for another sorting order: number PRs that are blocked by a given PR

[Jeremy Tan]

We definitely should have a technical debt section on the queueboard

[Yaël Dillies]

Johan Commelin said:

Idea for another sorting order: number PRs that are blocked by a given PR

That's an amazing idea

[Michael Rothgang]

Great ideas! Filed as queueboard#51 and queueboard#52. Both shouldn't be hard; I'll add them to my list of ideas for the first week of October.

[Johan Commelin]

Thanks!

[Ruben Van de Velde]

I tried to use the queueboard this morning but most of the PRs it showed on the queue either had unfinished or actually failing CI

[Michael Rothgang]

Side note: the "queueboard" linkifier points to the non-existent repo "https://github.com/leanprover-community/queueboard"; it should point at "https://github.com/jcommelin/queueboard" instead. Can some admin change this, please?

[Michael Rothgang]

Let me take a look. Did you look at the queue dashboard, or a different one? Because the former should use the exact same query as for #queue.

[Ruben Van de Velde]

https://jcommelin.github.io/queueboard/index.html

[Michael Rothgang]

Yes, sure. I meant, did you look at the "queue" section of that page? (It also has other dashboards, further below.)

[Michael Rothgang]

Ok, I think I found the culprit. The #queue uses "status:success", while the other dashboard just excludes failing PRs. That's an easy change, :working_on_it:

[Ruben Van de Velde]

Ah yeah, the "review queue" section. thanks for looking

[Michael Rothgang]

Pushed a fix (and started a conversation about aligning the definitions of the #queue in both sources). Should be live in ~10 minutes.

[Ruben Van de Velde]

So is the review queue ordered by pr number, but the 4 digits ones after the 5 digit ones?

[Michael Rothgang]

It seems so (the "PRs not into master" board shows this). That's a bug, thanks for reporting!

[Michael Rothgang]

I have a fix (and am exploring a more elegant fix now). I'll push some version tomorrow!Pushed now.

[Michael Rothgang]

New feature time: today, I implemented two feature requests from this thread

• there is now a dashboard of all technical debt PRs
• there is a separate page "why is my PR not on the queue" (which is available here.

Comments on both are welcome!

[Michael Rothgang]

Michael Rothgang said:

Side note: the "queueboard" linkifier points to the non-existent repo "https://github.com/leanprover-community/queueboard"; it should point at "https://github.com/jcommelin/queueboard" instead. Can some admin change this, please?

Bump, e.g. @Johan Commelin @Bryan Gin-ge Chen. Thanks!

[Bryan Gin-ge Chen]

Test: queueboard#50

[Michael Rothgang]

Works for me, thank you!

[Ruben Van de Velde]

Maybe also the repo should be moved if we actively rely on it now

[Michael Rothgang]

I have an opportunity for you to help improve this page: right now, sorting by the diff size will treat it as a string (and e.g. sort "1/90" before "1/100", even though the second PR has larger diff). I have most of the code to sort diffs properly, but am stuck at a question of javascript (which I'm not an expert on). Would somebody (e.g. @Jon Eugster @Bryan Gin-ge Chen) like to help?

In short: get this minimized webpage to behave as it says. Right now, the script fails to parse. It's presumably just a matter of syntax to fix this, but I don't know the right incantation.

<!DOCTYPE html>
<html>
<head>
<title>Datatable diff sorting test page</title>
<script src="[https://cdnjs.cloudflare.com/ajax/libs/jquery/3.5.1/jquery.min.js](view-source:https://cdnjs.cloudflare.com/ajax/libs/jquery/3.5.1/jquery.min.js)"
    integrity="[sha512-bLT0Qm9VnAYZDflyKcBaQ2gg0hSYNQrJ8RilYldYQ1FxQYoCLtUjuuRuZo+fjqhx/qtq/1itJ0C2ejDxltZVFg==]()"
    crossorigin="[anonymous]()"></script>
<link rel="[stylesheet]()" type="[text/css]()" href="[https://cdn.datatables.net/1.10.22/css/jquery.dataTables.css](view-source:https://cdn.datatables.net/1.10.22/css/jquery.dataTables.css)">
<script type="[text/javascript]()" charset="[utf8]()" src="[https://cdn.datatables.net/1.10.22/js/jquery.dataTables.js](view-source:https://cdn.datatables.net/1.10.22/js/jquery.dataTables.js)"></script>
</head>
<body>
<p>This is a test page for sorting diff sizes in data tables. The diff column should be sorted by the total changes, not as strings. Sorting as strings yields Alpha-Beta-Gamma, sorting by diff size should yield Alpha-Gamma-Beta.
Current error: how to make the `diff_stat` type be used?</p>
<table>
  <thead>
    <tr>
    <th>Title</th><th>Diff</th>
    </tr>
    </thead>
    <tr><td>Alpha</td><td>10/200</td></tr>
    <tr><td>Beta</td><td>100/10</td></tr>
    <tr><td>Gamma</td><td>60/60</td></tr>
</table>

<script>
$(document).ready( function () {
  let diff_stat = DataTable.type('diff_stat', {
    detect: function (data) { return false; },
    order: {
      pre: function (data) {
        let parts = data.split('/', 2);
        return Number(parts[0]) + Number(parts[1]);
      }
    },
  });
  $('table').DataTable({
    pageLength: 10,
    "searching": true,
    columnDefs: [{ type: 'diff_stat', targets: 4}],
  });
});
</script>
</body>
</html>

[Bryan Gin-ge Chen]

Ah, the links in the script tags look like markdown links to me instead of raw URLs, but maybe that was just an issue of copy pasting to Zulip? I tested after fixing them and it looks like the issue is that you're using v1 of DataTables, but DataTable.type requires v2? The following seems to work for me in VS Code's Live Preview server:

<!DOCTYPE html>
<html>
<head>
<title>Datatable diff sorting test page</title>
<script src="https://cdnjs.cloudflare.com/ajax/libs/jquery/3.5.1/jquery.min.js"
    integrity="sha512-bLT0Qm9VnAYZDflyKcBaQ2gg0hSYNQrJ8RilYldYQ1FxQYoCLtUjuuRuZo+fjqhx/qtq/1itJ0C2ejDxltZVFg=="
    crossorigin="anonymous"></script>
<link rel="stylesheet" type="text/css" href="https://cdn.datatables.net/1.10.22/css/jquery.dataTables.css">
<!-- <script type="text/javascript" charset="utf8" src="https://cdn.datatables.net/1.10.22/js/jquery.dataTables.js"></script> -->
<script src="https://cdn.datatables.net/2.1.8/js/dataTables.js"></script>
</head>
<body>
<p>This is a test page for sorting diff sizes in data tables. The diff column should be sorted by the total changes, not as strings. Sorting as strings yields Alpha-Beta-Gamma, sorting by diff size should yield Alpha-Gamma-Beta.
Current error: how to make the `diff_stat` type be used?</p>
<table>
  <thead>
    <tr>
    <th>Title</th><th>Diff</th>
    </tr>
    </thead>
    <tr><td>Alpha</td><td>10/200</td></tr>
    <tr><td>Beta</td><td>100/10</td></tr>
    <tr><td>Gamma</td><td>60/60</td></tr>
</table>

<script>
$(document).ready( function () {
  let diff_stat = DataTable.type('diff_stat', {
    detect: function (data) { return false; },
    order: {
      pre: function (data) {
        let parts = data.split('/', 2);
        return Number(parts[0]) + Number(parts[1]);
      }
    },
  });
  $('table').DataTable({
    pageLength: 10,
    "searching": true,
    columnDefs: [{ type: 'diff_stat', targets: 4}],
  });
});
</script>
</body>
</html>

[Jon Eugster]

Sorry, Im currently moving and am not on my computer; and I think that's not a question I can look at from my phone. Looks like Bryan is already on it though :)

[Michael Rothgang]

Bryan Gin-ge Chen said:

Ah, the links in the script tags look like markdown links to me instead of raw URLs, but maybe that was just an issue of copy pasting to Zulip? I tested after fixing them and it looks like the issue is that you're using v1 of DataTables, but DataTable.type requires v2? The following seems to work for me in VS Code's Live Preview server:

<!DOCTYPE html>
<html>
<head>
<title>Datatable diff sorting test page</title>
<script src="https://cdnjs.cloudflare.com/ajax/libs/jquery/3.5.1/jquery.min.js"
    integrity="sha512-bLT0Qm9VnAYZDflyKcBaQ2gg0hSYNQrJ8RilYldYQ1FxQYoCLtUjuuRuZo+fjqhx/qtq/1itJ0C2ejDxltZVFg=="
    crossorigin="anonymous"></script>
<link rel="stylesheet" type="text/css" href="https://cdn.datatables.net/1.10.22/css/jquery.dataTables.css">
<!-- <script type="text/javascript" charset="utf8" src="https://cdn.datatables.net/1.10.22/js/jquery.dataTables.js"></script> -->
<script src="https://cdn.datatables.net/2.1.8/js/dataTables.js"></script>
</head>
<body>
<p>This is a test page for sorting diff sizes in data tables. The diff column should be sorted by the total changes, not as strings. Sorting as strings yields Alpha-Beta-Gamma, sorting by diff size should yield Alpha-Gamma-Beta.
Current error: how to make the `diff_stat` type be used?</p>
<table>
  <thead>
    <tr>
    <th>Title</th><th>Diff</th>
    </tr>
    </thead>
    <tr><td>Alpha</td><td>10/200</td></tr>
    <tr><td>Beta</td><td>100/10</td></tr>
    <tr><td>Gamma</td><td>60/60</td></tr>
</table>

<script>
$(document).ready( function () {
  let diff_stat = DataTable.type('diff_stat', {
    detect: function (data) { return false; },
    order: {
      pre: function (data) {
        let parts = data.split('/', 2);
        return Number(parts[0]) + Number(parts[1]);
      }
    },
  });
  $('table').DataTable({
    pageLength: 10,
    "searching": true,
    columnDefs: [{ type: 'diff_stat', targets: 4}],
  });
});
</script>
</body>
</html>

Thanks so much! There was indeed a copy-paste issue with the markdown - and your other conjecture was spot on :man_facepalming: This seems to work locally now, I have pushed this change live.

[Bryan Gin-ge Chen]

I'm amazed that nothing broke when going from V1 to V2! (Well, almost nothing: queueboard#58)

[Michael Rothgang]

Me too, thanks for spotting! Adding a sub-resource integrity hash for the new URL, I realised the same mistake and fixed it already...

[Bryan Gin-ge Chen]

No time to investigate further at the moment, but the queueboard seems to be blank at the moment. I don't see any red X's in the recent actions, but the artifact uploaded by GitHub pages also contains a 0-byte index.html (scroll to the bottom to download the artifact): https://github.com/jcommelin/queueboard/actions/runs/11353648819

[Michael Rothgang]

A debugging change (disabling the generation of the dashboard) snuck in... fixed. Thanks for the report!

[Michael Rothgang]

Johan Commelin said:

Idea for another sorting order: number PRs that are blocked by a given PR

Were you thinking of (presumably, only open) PRs "directly blocked" by a given PR, or also transitively? The former is right in the PR description (hence easier), the latter may be more interesting. Both should be implementable.
I can also start with the former.

[Johan Commelin]

I was thinking of the latter.

[Johan Commelin]

Also. @Michael Rothgang switched refactored a bunch of plumbing, and now building the queueboard only takes ~1m. :octopus: We are now caching github metadata, instead of hammering the gh api on every queueboard build.

[Michael Rothgang]

(We are still querying github's API ~13 times during each build, but that's much less than the 500 calls we used to make --- and I have a plan to remove those as well.)

[Ruben Van de Velde]

Screenshot from 2024-10-17 10-06-29.png
Surprised by a PR having -1 comments (#17845)

[Michael Rothgang]

Good spot. These "-1"s means "detailed information" about this PR is missing when the dashboard is generated. In this case, this is a race condition (which a pending refactoring should fix).
There are about three PRs for which downloading this information causes the github runner to time out (as these PRs are huge). But these are tracking PRs, generally old and not on the queue.

[Michael Rothgang]

PSA: the statistics section is currently "broken" by a refactoring. (The github query it uses only returns up 1000 PRs, but mathlib has more. So it shows correct stats, but only for these 1000...) Proceeding with the refactoring will fix it. The queue is a separate query, and not affected. Sorry for the inconvenience!
Update: found a workaround (to the stats are fixed). Parts of the refactoring landed today.

[Ruben Van de Velde]

Better merge some PRs!

[Floris van Doorn]

Johan Commelin said:

contain a label with "t-algebra" as substring. (This includes "t-algebraic-geometry" and "t-algebraic-topology".)

Potential feature: encode label foo in the searchable text as foo$ (or label:foo$), so you can reliably search for a single label using t-algebra$ (or label:t-algebra$). Not the most important feature, but useful if easy to implement.

[Yaël Dillies]

Alternative solution: Rename t-algebraic-geometry and t:algebraic-topology to t:geometrie-algebrique and t:topologie-algebrique

[Michael Rothgang]

Floris van Doorn said:

Johan Commelin said:

contain a label with "t-algebra" as substring. (This includes "t-algebraic-geometry" and "t-algebraic-topology".)

Potential feature: encode label foo in the searchable text as foo$ (or label:foo$), so you can reliably search for a single label using t-algebra$ (or label:t-algebra$). Not the most important feature, but useful if easy to implement.

Interesting feature! Not sure how easy that that will be to implement --- but there is a middle ground that shouldn't be hard: add an input column below each table column; entering terms there allows filtering just that column. So, one could filter for user name, title or labels separately; global search is possible on top of this: this page has an example - what do you think?

[Floris van Doorn]

that doesn't resolve the precise "issue" that Johan had. Honestly, I would not put in much time in this direction, the current search box should suffice for most purposes.

[Michael Rothgang]

Here's a cursed idea to enable precise search: rename the algebra label to t-algebra$, then searching for t-algebra$ will only find it :exploding_head:

[Michael Rothgang]

(This is the only label with this property: algebraic-geometry and algebraic-topology can be distinguished by typing a few more characters.)

[Michael Rothgang]

The queueboard now has a table of all PRs opened from a fork.

[Ruben Van de Velde]

The queueboard seems to be redirecting to an index-old file. Anything going on?

[Michael Rothgang]

Please reload the page, the output should be different now. :-)

[Michael Rothgang]

Yes: I re-designed the webpage a bit, splitting it into several parts --- for reviewers, maintainers, folks just wanting to help out (by something other than reviewing) and triage (still partially under construction). The "old main page" is still available for now --- but I hope the new split helps you better find what you're interested in.

If you just want the review queue, the link is now https://jcommelin.github.io/queueboard/review_dashboard.html.

[Michael Rothgang]

Bildschirmfoto vom 2024-11-03 11-12-13.png

This is how the main page looks now.

[Michael Stoll]

Does -1 mean 0 in the "files modified" and "comments" columns?

[Ruben Van de Velde]

I think it means "no data"

[Michael Rothgang]

Which label would be clearest for you: "-1", "???" or "no data"? This is easy to change.

[Edward van de Meent]

i think a simple n/a should be clear

[Kim Morrison]

Can I braindump some queueboard requests here? If these are better as issues somewhere I can do that!

• Clicking on either an author or a label should not jump to github, but instead add that author or label to the search filter.

• At https://jcommelin.github.io/queueboard/triage.html, both these links 404 in the line

  28 PRs are waiting on maintainer approval (these), of which 21 have not been updated in a day (these)

• Could the "entries per page" selectors be sticky? (e.g. persisted via cookie?)

[Yaël Dillies]

Can we make filters appear in the URL? That would be very useful for review parties, to share the list we are looking at

[Michael Rothgang]

Thanks for reporting: The 404s are fixed now.

[Michael Rothgang]

The other ideas are good; I'd have to think how to implement them.

[Bryan Gin-ge Chen]

I have snippets of code around for persisting data in localStorage and encoding/decoding from URL so I could work on those or give pointers.

[Michael Rothgang]

PRs for these are very welcome; I'll be happy to review!

[Michael Rothgang]

@Bryan Gin-ge Chen I think now is a good time to add the above to the queueboard. Do you have a moment to share these snippets (and I can take it from there)? If you're feeling like it, I'll also review a PR instead :-)

[Bryan Gin-ge Chen]

Sure, I'll try and let you know either way by tomorrow!

[Yaël Dillies]

Could we also a linkifier for #queueboard ? Wait, I already asked for it a few weeks ago

[Bryan Gin-ge Chen]

Turns out there was a built-in option to save the state of the tables in localStorage: https://github.com/jcommelin/queueboard/pull/64

[Johan Commelin]

Fantastic!

[Michael Rothgang]

@Bryan Gin-ge Chen Sorry to ping you again: I thought about how to implement "reading table states from an URL" (so one could e.g. share one link for the triage meeting, which configures a table as desired). Your code snippet for reading parameters from a URL could be handy. Otherwise, I'll ask the internet, that's also fine :-)

[Bryan Gin-ge Chen]

@Michael Rothgang Here's a very rough snippet (not tested) with functions for reading and writing parameters in a URL: https://gist.github.com/bryangingechen/a9a34a0092ccf3abfa56c5fda3f0ade2

Feel free to ping me again if there are any issues!

[Artie Khovanov]

image.png
these percentages appear to be calculated inconsistently (one relative, one absolute)
not sure if this is an issue, but flagging it in case

[Michael Rothgang]

Thanks for the report. It should be relative percentages; a fix is coming shortly. Update: it's live now.

[Patrick Massot]

Does anyone understand why #21619 is indicated as “CI is still running”? It is a trivial PR that never had any CI issue.

[Patrick Massot]

@Michael Rothgang #15373 appears in the list of quick tasks for maintainers but probably shouldn’t since it’s actually awaiting author.

[Yaël Dillies]

Where do you see that? Here is all I'm seeing

[Patrick Massot]

This is not necessarily a queueboard bug, it can mean maintainers failed to do something.

[Patrick Massot]

I see
image.png

[Patrick Massot]

I see this at https://jcommelin.github.io/queueboard/on_the_queue.html, typing massot in the search box.

[Patrick Massot]

Yaël, since you’re here, don’t hesitate to tell me if this lemma is already somewhere. I couldn’t find it but I would happily get rid of this PR (and same with other two trivial PRs I opened yesterday).

[Yaël Dillies]

Woah, I had not seen this page of the queueboard. And no I had never seen your lemma before, and loogling (_ * _) ^ _ * _ gives nothing of interest

[Patrick Massot]

Ok, maybe we should wait until Michael or @Johan Commelin gets a chance to see this bug, and then merge the PR.

[Damiano Testa]

The PR also appears to be a Draft in the queueboard, although it never seems to have passed through that stage.

[Michael Rothgang]

Patrick Massot said:

Michael Rothgang #15373 appears in the list of quick tasks for maintainers but probably shouldn’t since it’s actually awaiting author.

Thanks for asking; I'm taking a look now. To make sure I understand correctly, you're referring to #15373 being on the stale ready-to-merge dashboard?

[Michael Rothgang]

This is by design: that dashboard contains all PRs labelled ready-to-merge which have not been updated recently. (Usually, these are PRs which failed a bors batch, so a maintainer should retry them.)

[Michael Rothgang]

For this PR, there are probably several things to fix

• the PR was never unlabelled ready-to-merge
  That can probably be fixed. @Damiano Testa @Bryan Gin-ge Chen Does the recent change you made cover this/can it be extended to make this so? (A bors r- did not remove the ready-to-merge label; I would argue it should.)

• The PR failed CI and still does: the on the queue page shows it as passing, though. That's a bug, I'll look into that now.

[Damiano Testa]

Currently, the bors r... action does not know at all about -: it only acts on bors r+, ignoring bors r-. Of course, this is easy to change!

[Michael Rothgang]

Patrick Massot said:

Does anyone understand why #21619 is indicated as “CI is still running”? It is a trivial PR that never had any CI issue.

The queueboard doesn't say there are CI issues, just "last time we checked, CI was still running". By now, CI has finished, of course.

Short version: this is a known issue, which has a mitigation in-place. Better solutions welcome.
Long version: the queueboard relies on github saying "this PR was updated" to know when to download new data for a PR. There is no explicit notification for "CI for this PR finished running" (but for most other events, there is): so, it can happen that a "CI just finished" is missed. To mitigate this, the queueboard automatically asks for updated data after 60 minutes. Then, the information is updated.

[Michael Rothgang]

Damiano Testa said:

Currently, the bors r... action does not know at all about -: it only acts on bors r+, ignoring bors r-. Of course, this is easy to change!

I think that would be helpful.

[Michael Rothgang]

Patrick Massot said:

I see this at https://jcommelin.github.io/queueboard/on_the_queue.html, typing massot in the search box.

Thanks for the clear instruction! I see the issue now. (The description right now lumps "marked draft", "CI fails" and "CI still running" into one. That's ... inaccurate at least. Will fix right now.)

[Damiano Testa]

Michael Rothgang said:

The queueboard doesn't say there are CI issues, just "last time we checked, CI was still running". By now, CI has finished, of course.

Would it be possible to add a CI step after a successful run that "pings" the queueboard, updating the status?

[Michael Rothgang]

One workaround could be to have a workflow add the awaiting-CI label on every push. Then, passing CI would remove that label, triggering an update.
Better ideas welcome!

[Michael Rothgang]

Update:

• I've fixed the strange labelling ("marked as draft"); the fix should be live now
• #15373 actually always passed CI (it was just a bors batch that was cancelled) - so the classification was arguably correct

From my side, everything looks as expected now. It would definitely be nice to make the bot also react to "bors r-". I'll look into a deeper fix for "update CI" status now.

[Damiano Testa]

#21636 removes the ready-to-merge and delegated labels when the comment contains bors r- or bors d-. Note that bors d- is not an actual bors command, but the "local" action still removes the label.

[Patrick Massot]

Thanks a lot Michael and Damiano. I’m happy that my questions led you to improvements in our tooling.

[Damiano Testa]

#21645 follows up the previous PR: it fixes a bug and should distinguish better between bors d+/bors delegate and bors d-. It also adds support for bors merge-.

[Damiano Testa]

Since no change to CI is small enough to contain only countably many bugs, #21676 fixes yet another bug with bors d- removal of delegated.

[Damiano Testa]

I just tested the bors r-/bors d- actions and they appear to work! Please, report if you notice any issue with them!

[Michael Rothgang]

It has been a while since my last update comment. In the meantime, quite a bit of work has happened: let me highlight a few shiny new features.

Show the last real status change

If you attended my Lean together talk, you saw this one already: the queueboard grew two new columns, for showing when a given PR

• last changed its status (e.g. from waiting on the author to waiting for review),
• the total time a PR was waiting for review.
  A very small share of PRs does not have this data (e.g., because downloading the necessary metadata would take too long to download), but in practice this works very well.

All open PRs

There is now a dashboard of all open PRs. Since yesterday, this dashboard is also linked on the main page. If you ever wanted to see all your PRs, or all PRs by somebody else, this is the place to go! The next feature makes this even more useful.

Saved table searches/ configure dashboards via the URL

Until now, there was no great way to save a dashboard's configuration. If you set a larger number of items per page, entered some search terms or chose some sorting, this was not really persistent. (The queueboard did save the last table configuration, but no more.) This has an end now: you can now tweak the page length, initial sorting and search terms by changing the URL you're visiting.

A few examples what this can be used for:

• sort the #queue table by total time in review (in descending order): https://jcommelin.github.io/queueboard/review_dashboard.html?sort=10-desc#queue. This might be a reasonable default for use in triage meetings. (You may want to check if a PR had recent activity: but the table contains this information at once glance.)

• show all t-differential geometry PRs on the queue, sorted by ascending diff size and then by author:
  https://jcommelin.github.io/queueboard/review_dashboard.html?search=t-differential%20geometry&sort=diff-asc&sort=author-asc#queue

• why are my PRs not on the queue? https://jcommelin.github.io/queueboard/on_the_queue.html?search=grunweg&length=100 shows the status of all my PRs, on one page. (To tweak: replace grunweg by your github handle; 100 is the number of items shown per page. Omitting it shows 10 PRs by default.)

• https://jcommelin.github.io/queueboard/triage.html?search=kim-em&sort=10-desc#all shows all open PRs by kim-em, sorted by total time waiting for review.

The current code is an MVP version, i.e. there are some rough edges/known issues.

• currently, you can tweak the page length, initial sorting and search terms by changing the URl you're visiting. Further criteria are totally possible: let me know if there are any you'd find helpful.
• filtering currently always filters all tables on a page; there's no way yet to filter only a certain table (help welcome, see here for details)
• the sorting configuration takes indices as default argument (the 10 you saw above was the 0-based column index, from the last). For some columns, I have defined human-readable names as stable aliasses already; the last few columns will follow soon.(Another complication is that a few less common tables have some columns omitted... so the current solution is not perfect yet. This will come in time.)
• there's no way yet to generate a URL for the current table: that's not hard to implement. In the mean-time, feel free to ask me any questions you have.

Beyond these points, some natural future directions are

• more rigid filtering syntax: currently, "kbuzzard" finds all PRs where kbuzzard is an author, a reviewer or assignee. Writing "author:kbuzzard" could be a way to make this precise.
• support for filtering by one of multiple authors or multiple labels. (This would allow e.g. saving a "list of all my favourite authors", individually.)

Visual tweaks

Thanks for all the responses to the queueboard survey! Some features were quick to implement; this includes

• diff size is now coloured (green for insertions, red for deletions)
• the "last update" is shown more compactly: it only displays something of the form "5 days ago" (with the exact data available upon hover)
• the "on the queue page" shows a warning for PRs which are missing a topic label (i.e., feature PRs without a label t-something)
• hovering above a PR number shows its github branch
  We would also like to make this copy-pastable, but are not sure about the best option yet. If you have a suggestion, we'd like to hear it!

Smaller changes

Some smaller changes include

• changed in mathlib CI: delegated PRs have their maintainer-merge label removed (making the maintainer merge dashboard less cluttered)
• refactored: the computation of "last updated" and "total time in review" is now performed during preprocessing: in particular, external tools consuming the .json files have access to this as well.
• added a field "first time on the queue" to the aggregate data (which is only implicitly exposed, through the line "88 PRs appeared on the review queue within the last two weeks" here)
• changed: stale unassigned PRs now uses the last status change as threshold for staleness, as opposed to github's "last update" (commit). I think this is better; there is certainly room to fine-tune this.
• significant effort was put into making the data collection more robust. One piece of infrastructure is missing: re-downloading a PR's metadata once its CI finishes (queueboard#91).

[Johan Commelin]

:alert: PSA :alert: The queueboard has moved: https://leanprover-community.github.io/queueboard/

[Johan Commelin]

Zulip linkifier updated. Old web address now hosts a redirect.

[Michael Rothgang]

To everybody who cloned the repository locally: please remember to update your configuration to change the upstream location. (There is a new placeholder repository, with just a redirect - which would confuse git otherwise.)

[Yaël Dillies]

Where does the JSON fuelling my upstreaming dashboards live now? The following line is failing now: https://github.com/YaelDillies/Toric/blob/master/scripts/upstreaming_dashboard.py#L15

[Yaël Dillies]

Is it the same thing but leanprover-community/queueboard instead of jcommelin/queueboard ?

[Michael Rothgang]

By the way: these json files recent got a bit larger, as we're adding additional metadata (PR descriptions, users who commented etc.) for displaying this information also. If that size poses an issue, we can think about creating files with just a subset of this information.

[Yaël Dillies]

For now it works great! (today was the first day any of my many upstreaming dashboards failed to build)

[Michael Rothgang]

Two new features have arrived in the queueboard:

• searching a list of PRs also searches the PR description
  Johan and I think this is a reasonable default, which coincidentally matches what github does. If you'd like a way to opt out, let us know - it wouldn't be hard to implement.

• you can search for PRs you commented on or reviewed: for each PR, we compute all users who commented on or reviewed this PR; searching a list of PRs also searches this list.

Fixed: sorting by diff size works again (a change a week ago broke this).

[Michael Rothgang]

Another update:

• Searching all PRs I commented on by default makes finding "my PRs" harder: to compensate, I added a mild hack. Searching for author:grunweg will find all PRs whose author is grunweg. (If you need this for other columns, reach out --- this can be implemented in a more general way.)
• Searching for t-algebra$ as part of your query will return all PRs whose label is t-algebra --- without false positives from t-algebraic-geometry. (I believe @Floris van Doorn mentioned this a while ago.)
• You can now search the files a PR modifies: simply search for the file name. (Small caveat: we only return the first 100 files a PR changes. If a PR modifies more files, this search will miss some of the files. Such PRs are rare, though.)

[Michael Rothgang]

And another one:

• all columns now have a stable "human-readable name" for the purposes of sorting: for instance, you can now use review_dashboard.html?sort=totalTimeReview-desc#queue to get a reasonable shared view for mathlib triage meetings
• I added a blob of user-facing documentation to the main page. Please let me know if anything is unclear or missing. (And if you're a better graphics designer, PRs for the formatting are also welcome.)

[Michael Rothgang]

I'd like to celebrate a small milestone with you: in the past months, I have been backfilling metadata for all closed PRs. To the best of my knowledge, this process is now complete: the repository has data for all mathlib4 PRs, past and present.

[Patrick Massot]

This is nice opportunity to say: Thank you so much for all the work you are doing for the community!