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!

[Bolton Bailey]

I notice that there are a few PRs that are on the #queue, yet have unresolved conversations in their discussion threads.

• Do we ever want PRs like this to be on the queue?
• If not, is it easy/possible to add a condition to the queueboard website to only put PRs on the queue if all discussions are resolved?
• Barring that, should we be uniformly tagging these PRs as awaiting-author or awaiting-zulip or something?

[Yaël Dillies]

Yes, no, no. Basically, it is important to keep some discussions open when they provide extra context for the PR or contain hints towards future work. Prematurely resolving conversations can lead to several reviewers asking the same question.

[Andrew Yang]

What do you mean by "unresolved conversations"? Sometimes when the reviewer asks a question I would respond but not press the "resolve" button because I am not sure if the reviewer is happy with the answer but it is no longer "awaiting-author" so I will put it back on the queue. Do these count as unresolved?

[Andrew Yang]

keep some discussions open when they provide extra context for the PR or contain hints towards future work

Though arguably these should not live in some obscure review comment that is hard to find once the PR is merged, but in the PR message or in the docstring.

[Yaël Dillies]

Yes of course, but it is not always clear upfront what is and isn't worth recording. I think it's counter-productive to set strict boundaries like that

[Michael Rothgang]

I think we should just become more dilligent at labelling PRs correctly. (That way, the queueboard picks them up correctly, and that's a sure way to signal which kind of comment this is.)
That is: if a conversation is unresolved and waiting on author action, I think we should tag the PR with awaiting-author. If it needs a zulip discussion, it should be awaiting-zulip. If it's just open for context, we can leave as-is. Determining which is which can be a judgement call.

[Michael Rothgang]

The queueboard just gained a few feature (courtesy of @Johan Commelin and some AI help): there is now a dashboard showing the dependency structure between pull requests. There is some clustering, colour-coding (into no deps, blocked and draft/WIP), you can search for theorem number, name, labels, authors etc. Enjoy!

[Joscha Mennicken]

Very cool. However, dragging a PR around seems to make all the other PR clusters move away from the origin.

[Bryan Gin-ge Chen]

@Michael Rothgang I just noticed the queueboard update job has been failing for ~12 hours since the generated processed_data/all_pr_data.json is now >100MB and is too large for github: https://github.com/leanprover-community/queueboard/actions/runs/17115642373/job/48545858368#step:10:9

The queueboard is going to be stuck until we're able to revive that job (which I've disabled manually for now). Since you're on vacation, do you want me to take a stab at this? I'm thinking of just doing something quick and dirty with split to break up the giant JSON file into several pieces before we try to commit, and then make sure we reassemble those pieces again before we try to use it.

[Michael Rothgang]

Another band-aid is not generating that file, iirc it is not used for the final output.

[Michael Rothgang]

Help is very welcome. Thank you!

[Michael Rothgang]

I can take a detailed look on Monday, when I'm back.

[Michael Rothgang]

I just checked how all_pr_data.json is used:

• the main dashboards do not use it at all
• the data integrity check uses it to find PRs which are closed now, but not yet marked as such (this could probably be removed)
• a (hidden by default) assignment statistics page also counts assignments of closed PRs

In particular, I could rewrite everything to no longer use that file at all.

[Michael Rothgang]

(And e.g. add an option to process.py to also update that file, whenever somebody wants to use it for data analyses.)

[Michael Rothgang]

If we want to keep it, a more semantic split could be to create a file all_pr_data-1.json with the first 10,000 PRs' data, all_pr_data-2.json with the second batch, etc. This way, each file stays valid json and at a reasonable size.

[Bryan Gin-ge Chen]

Ah, while you were writing your comments I've already pushed my quick and dirty fix in queueboard#104 (and follow-up queueboard#105 to make the scripts use the split files instead).

[Bryan Gin-ge Chen]

Hello queueboard fans! I'd like to give an update on work-in-progress on the queueboard, and also see if there is anyone in the community who might be able to give advice on data-driven app design / review PRs.

As one of my responsibilities the Mathlib Initiative, and with lots of advice from Johan and Michael, I've been working over the past few weeks on a plan to move the queueboard from the current GitHub actions + GitHub repo based architecture to a more standard database-backed web app with hosting that the MI will pay for. This will have lots of advantages:

• the queueboard repo is already tens of GB in size (and growing), making git operations very slow
• we are already hitting rate limits trying to scrape data from GitHub; having an app which can schedule / backfill queries from GitHub and (eventually) listen for webhooks will be much more efficient
• a new architecture will also enable faster updates (current latency is 15 minutes)

More details on the current planned architecture of v2 is at queueboard-core#33, but basically, I think we'll need something with the following modules, which roughly correspond to parts of the existing architecture:

• a syncer in charge of getting data from GitHub and putting the raw data into the database
• an "analyzer" in charge of computing analytics from the raw data and putting those into analytics tables
• an API which will serve data from the database to the frontend

I've decided to try and build this new backend as a Django project, with separate apps for the modules above; this is mostly because the queueboard is already mostly written in Python (and because I have a smidgen of experience with it).

Let me say now that while I've been a user of this kind of analytics web app before, I've never built one before, so at the moment I'm doing my best with django tutorials and advice from AI. What I have so far is at queueboard#59, which adds a django project skeleton. Here we'd like to reach out to the community -- if you have experience with this sort of thing and are willing to help review PRs / provide advice, please reply here or DM me! Feel free of course to comment on the open PRs at queueboard-core too!

[Patrick Massot]

I have experience with Django, but not much time.

[Christian Merten]

I left some comments on queueboard-core#33. Feel free to reach out if you have questions. I won't have time to write code, but I have experience with Django and am happy to answer questions.

[Joachim Breitner]

sorry if this suggestion was raised before: I find the view at https://leanprover-community.github.io/queueboard/on_the_queue.html with my username in the search field very useful to monitor progress. But if I Ctrl-R, the search is gone.

It would be useful if the search box content was reflected in the url (in the #… part), so that this can be reloaded/bookmarked/shared more easily.

[Bryan Gin-ge Chen]

I think this might be queueboard-core#10. I've been mostly working on the v2 backend, but I can take a look at some frontend stuff like this this week.

[Joachim Breitner]

Thanks!

[Vlad Tsyrklevich]

In tips and tricks here it mentions that you can get this by using a URL like this (but I agree that from a front-end perspective it should be a # fragment not a query and be automatic)

[Bryan Gin-ge Chen]

I have a first version of a new feature where making changes to queueboard settings will automatically update the URL at queueboard-core#66. I'm still doing some final testing, but before deploying, I wanted to mention a few possibly controversial choices I made:

• After this change, whenever you make a change to either the search, page length (number of rows per page), or column ordering settings, they will be reflected in the URL.
• We don't have per-table settings yet so if you load a URL with settings, they will be applied to all tables on the page
• The back and forward buttons should work to navigate to previous states stored in the URL
• changes to the search settings are debounced; the search parameter in the URL will only be updated after 500ms without any changes
• I decided to stick with putting the params in the query string rather than a fragment because sometimes we also want to link to specific tables using the fragment (maybe there are clever ways to support both but I couldn't find any quickly)

Please let me know if you feel strongly about any of the above, or have any other comments!

[Bryan Gin-ge Chen]

The above change making it so the #queueboard URL automatically updates when searching, sorting, or changing page length settings is now live! Please let me know if anything is broken!

[Michael Rothgang]

I just looked over the js-only changes, and they look good to me. Testing the queueboard changes, everything appears to work well. (If I find a bug, I'll report it, of course.)
Thanks a lot for implementing this, this is really nice!

[Michael Rothgang]

Actually, I have one idea/small request: can you update the "tips and tricks" section on the main page to mention this fact, that a page URL is updated automatically --- so you can mostly "generate" your URL by making the dashboard configuration you want and then copying the URL?

[Bryan Gin-ge Chen]

Good idea! I'll do that now.

[Bryan Gin-ge Chen]

I've opened queueboard-core#67; not sure about the wording, so suggestions welcome!

[Michael Rothgang]

I suggested some tweaks (and like the general gist of it)!

[David Loeffler]

Minor remark about the queueboard: several PR's (including one of mine) are listed on the queueboard as having a "WIP" tag, when in fact the tag has previously been removed:

https://leanprover-community.github.io/queueboard/review_dashboard.html?search=WIP

(This seems all the more strange given that PR's which actually do have a WIP tag don't appear on the queueboard at all, so somehow the queueboard simultaneously knows and doesn't know that these PR's have been untagged...)

[David Loeffler]

(Note that the removal of the WIP label from #30089 on github was four days ago, so this is not just a time-lag issue.)

[Johan Commelin]

Thanks! I noticed something similar a few days ago. Bryan has been working on designing and implementing a new backend for the queueboard that will scale better. When the frontend is switched over to the new backend, my hope is that this bug will also magically be solved. Should happen in a matter of days.

[Sébastien Gouëzel]

Similar report on #26923, where the merge-conflict report has been removed three days ago, but still shows up in the queueboard. It just looks like the info of the queueboard (at leat on this PR) has not been updated recently. Let's wait for the improved queueboard, hoping it fixes everything!

[Bryan Gin-ge Chen]

Sorry for the issues with the outdated data. I'll try and revert some changes I made while I work out what's going on.

[Bryan Gin-ge Chen]

I had a look and it looks like the initial cause is that there was some extended downtime Dec 8-9 (related to some changes I made) which led to ~140 PRs to end up with outdated data. The queueboard scripts are supposed to gradually re-download data for outdated PRs but for some reason I don't understand yet it's not really making progress. I'll look a bit more, but if I don't figure it out I will switch to getting the new backend ready (currently everything is finally connected, but the queue computation is completely wrong).