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).

[Bryan Gin-ge Chen]

Hi everyone -- the new backend for the queueboard is finally just about ready to use in production. I'm planning to swap the current #queueboard with this test site in a few days. Note that the frontend webpages are still the same, only the data source has changed.

Please take a look if you have a chance and let me know if anything is broken!

Known differences:

• the new backend is updated more frequently, so there may be discrepancies in labels / open-closed status when the old queueboard is using outdated PR data
• GitHub deletes CI logs after a little more than a year, so the new backend is missing CI data for old PRs
• "total time in review" and (to a lesser extent) "last status change" are fairly sensitive to historical data about the status of PRs, so the points above can lead these data points to differ
• There are still some differences in how PR statuses are computed for PRs that are not on the queue, so the numbers on the triage page and the pie chart will not match (I'm investigating this still)

[Bryan Gin-ge Chen]

The #queueboard is now using the new backend by default!

I've kept the old backend running for now; you can view the queueboard populated with that data at: https://leanprover-community.github.io/queueboard/legacy

[Anne Baanen]

That is great news! The sad thing about replacing the backend is that doing the best possible job will mean nobody notices a thing. But the new backend really is a big improvement that allows many more features in the future and I am grateful to Bryan for doing this work!

[Michael Rothgang]

As the main author of the old backend, I am really really happy about the work Bryan is doing. This is very fiddly technical work, which is easy to get wrong and has little reward when getting it right ("nobody notices"). The old architecture was working to a point, but certain big improvements were very hard to achieve. I'm hopeful that the new design will even the queueboard to have e.g. drastically lower latency and be useful in other ways previously impossible!

[Michael Rothgang]

Is there a way to ingest or backfill old PR data from the old backend into the database? (Yes, this would be a lot of effort. Perhaps it's worth it, for a one-time migration.)

[Michael Rothgang]

For historical trends, this could be interesting!

[Bryan Gin-ge Chen]

Thanks for the kind comments!

Michael Rothgang said:

Is there a way to ingest or backfill old PR data from the old backend into the database? (Yes, this would be a lot of effort. Perhaps it's worth it, for a one-time migration.)

It should be possible to do this -- not sure when I'll get to it but it's on my list!

[Snir Broshi]

Can you explain what changed, and maybe if there's something the community can help with? :heart:
AFAIK the previous backend worked by having GH actions that query the GH API and dump jsons to disk, then the website is a python script that converts the jsons to html

[Johan Commelin]

1-line summary: It's now backed by an honest sql database hosted on Heroku.

[Michael Rothgang]

I looked at the first five PRs in the #queue, and compared their data:

• the new data for #27100 is missing two initial time windows when it was waiting for review. The first is indeed a mistake in the new algorithm; I don't see the second in the PR history any more; this could be explained by new data downloaded after the force-push.
• the other data differs only in minor ways

[Michael Rothgang]

I have two comments about presenting the detailed times when a PR was on the queue, i.e. the format of the tooltip when hovering over this:

• in the new dashboard, a timespan is shown as 2025-11-26T03:22:49+00:00 → 2026-01-14T12:30:49.087553+00:00 --- can you remove the +00:00? I find these more visually distracting than helpful
• the old tooltip also displayed this as a human-readable value, as in (1 month); how difficult is it to add this back?
• I also like the old from ... to ... and since ... phrasing; I'm not attached to the from ... to but find the since helpful. What do you think?

[Bryan Gin-ge Chen]

Snir Broshi said:

Can you explain what changed, and maybe if there's something the community can help with? :heart:
AFAIK the previous backend worked by having GH actions that query the GH API and dump jsons to disk, then the website is a python script that converts the jsons to html

3-line summary: the new backend is a Django app (under qb_site in the queueboard-core repo) that runs on heroku. It is constantly scraping repo data into a Postgres database and then processing it to compute things like when PRs are on the queue. For now we're still using the same frontend pages, so that app is just serving the queue data as a JSON file that GitHub actions fetches every once in a while to build the HTML pages.

For the moment, what everyone can help with is reporting issues / feature requests here or in the queueboard-core repo issues!

[Michael Rothgang]

I'm happy to help by tweaking the tooltip, if you tell me the current location of the code. (If you agree with that, of course: it looks like you chose to change this.)

[Bryan Gin-ge Chen]

Michael Rothgang said:

I looked at the first five PRs in the #queue, and compared their data:

• the new data for #27100 is missing two initial time windows when it was waiting for review. The first is indeed a mistake in the new algorithm; I don't see the second in the PR history any more; this could be explained by new data downloaded after the force-push.
• the other data differs only in minor ways

Regarding #27100, it does look like there are issues with computing queue history from before force pushes. I'll take a closer look.

Michael Rothgang said:

I have two comments about presenting the detailed times when a PR was on the queue, i.e. the format of the tooltip when hovering over this:

• in the new dashboard, a timespan is shown as 2025-11-26T03:22:49+00:00 → 2026-01-14T12:30:49.087553+00:00 --- can you remove the +00:00? I find these more visually distracting than helpful
• the old tooltip also displayed this as a human-readable value, as in (1 month); how difficult is it to add this back?
• I also like the old from ... to ... and since ... phrasing; I'm not attached to the from ... to but find the since helpful. What do you think?

Yes, I think it shouldn't be hard to change the formatting of the tooltip here; I can probably do this quickly. One conscious change here though is that the new queueboard only shows up to the last 5 windows in the tooltip to avoid having to fetch all queue windows for all PRs.

[Michael Rothgang]

Thanks! IIRC, github does not notify you directly of force pushes, so keeping the data updated in their presence was already tricky. (How are you solving this now? I was cross-checking with REST API call data, which worked, but was of course a hack.) I wouldn't be surprised if there are further pitfalls.

[Bryan Gin-ge Chen]

Oh -- I wasn't aware that github didn't send notifications for force pushes. However, as long as a force push causes updatedAt for the PR to change, the syncer task will fetch (among other things) all force push events since the last sync; I think that should keep things there up to date.

[Michael Rothgang]

I don't think force-pushes change the updatedAt field. (That's what I meant to say.)

[Michael Rothgang]

You can probably trigger a webhook upon force-pushes, though --- so there is a way to enqueue a re-download.

[Michael Rothgang]

I believe mere title changes (also edits to the PR description) may also not change that field. I don't remember exactly; I may have documented this somewhere in one of the issues for migrating to just the aggregating data.

[Michael Rothgang]

Is there an easy way to say "this data for this PR looks outdated, please re-sync"? (The old backend used a text file... it was a hack, but worked well.)

[Bryan Gin-ge Chen]

Michael Rothgang said:

I don't think force-pushes change the updatedAt field. (That's what I meant to say.)

I was worried about this so I checked by force pushing to one of my PRs (#33044); it looks like the syncer did successfully detect the change and update the PR data though.

[Bryan Gin-ge Chen]

Michael Rothgang said:

I have two comments about presenting the detailed times when a PR was on the queue, i.e. the format of the tooltip when hovering over this:

• in the new dashboard, a timespan is shown as 2025-11-26T03:22:49+00:00 → 2026-01-14T12:30:49.087553+00:00 --- can you remove the +00:00? I find these more visually distracting than helpful
• the old tooltip also displayed this as a human-readable value, as in (1 month); how difficult is it to add this back?
• I also like the old from ... to ... and since ... phrasing; I'm not attached to the from ... to but find the since helpful. What do you think?

The tooltips should now be closer to their previous behavior (after queueboard-core#119 and queueboard-core#120). Let me know if there's something I missed!

[Michael Rothgang]

From that I tried, this looks great. Thanks for the quick response!

[Michael Rothgang]

#32600 appears to be have missing metadata. It's only one commit, so I'm not sure what went wrong. Can you re-sync?

[Bryan Gin-ge Chen]

Michael Rothgang said:

#32600 appears to be have missing metadata. It's only one commit, so I'm not sure what went wrong. Can you re-sync?

I re-synced the PR but It looks like the data is already up to date. However, there is a force-push in the history which appears to be breaking the queue computation. I'll investigate.

[Notification Bot]

6 messages were moved from this topic to #mathlib4 > upsteraming dashboard by Bryan Gin-ge Chen.

[Michael Stoll]

#33893 does currently not show up on #queue, even though it has a green check mark and no "awaiting-author" label. What should I do to make it appear?

[Artie Khovanov]

Usually when this happens I wait ~a day and it shows up

[Michael Stoll]

Shouldn't the new version be faster with updates?

[Bryan Gin-ge Chen]

The why is my PR not on the queue page says that the queueboard backend is missing CI information from the PR. There may be an issue with the syncing. I'm traveling now but I'll try and take a look when I have a chance.

[Bryan Gin-ge Chen]

I tried manually syncing the data a few ways and it looks like your PR is back on the queue now. I've made a note of it and will try and figure out what went wrong.

[Michael Stoll]

Thanks!

[Sébastien Gouëzel]

Do you have an estimate of the delay between queueboard updates? I have acted on several PRs this morning (delegating or merging them or adding the awaiting author tag) but they still show up on my queue with the same state they had before.

[Bryan Gin-ge Chen]

It's supposed to be around 10 minutes or so but it looks like there is an issue with the queue syncing at the moment. Could you check the legacy queueboard and see if it's more up to date: https://leanprover-community.github.io/queueboard/legacy/ ? I may switch the queueboard back to the old one tonight if I can't figure out what's going on quickly.

edit: I'm in the process of switching the #queueboard back to the old backend temporarily while I investigate this. After the change goes live (probably within half an hour or so), the queueboard using the new backend will be accessible at https://leanprover-community.github.io/queueboard/test-rule-set-1

[Bryan Gin-ge Chen]

I think I tracked down the issue causing PRs not to get synced so I've swapped the #queueboard back to the new backend. Please don't hesitate to post here if you notice any issues! As before, the old queueboard is available at https://leanprover-community.github.io/queueboard/legacy in case of emergency.

[Joseph Myers]

I believe I have four PRs available for review, but I only see two of them on the queueboard. I see #31891 and #33928 there, but not #30981 or #32260, although all four appear on the old queueboard (#30981 being in 3rd place there).

[Bryan Gin-ge Chen]

Yes, it does look like those two should be on the queue. I'll try and fix this today.

[Bryan Gin-ge Chen]

I've fixed the issue causing #30981 and #32260 to be missing CI data. Thanks again for the report!

[Louis Liu]

Hi @Bryan Gin-ge Chen ! I have a PR #34815 that has passed the check, but it is not on the queueboard with the displaying status of "missing CI information":

Screenshot of "missing CI information" on the queueboard

Is that a bug? Could you please check it when you have a minute, thank you!!

[Bryan Gin-ge Chen]

Thank you for the report! There was indeed a bug; a fix has been deployed and your PR is now on the queue: https://leanprover-community.github.io/queueboard/review_dashboard.html?search=34815#queue

[Bryan Gin-ge Chen]

(Note to reviewers: it looks like this fix added about 37 PRs that were accidentally being excluded to the queue. Please take another look if you have a chance!)

[Yongxi Lin (Aaron)]

@Bryan Gin-ge Chen May you take a look of #34890 again? It passes the CI but is not on the queue.
Screenshot 2026-02-09 at 2.30.56 PM.png

[Bryan Gin-ge Chen]

I think I see the issue; we don't have a good way to update CI statuses that have been re-run at the moment. I'll work on fixing this now.

In the meantime could you try pushing another commit to the PR? Maybe just merging master or something.

[Yongxi Lin (Aaron)]

I merged master and it now appears on the queue. Thank you for your help!

[Bryan Gin-ge Chen]

No problem, thank you for the report!

[Weiyi Wang]

A minor request... can the queueboard ignore bot actions (e.g. auto-assigning reviewers) as an "update" to PR? At the moment, if a PR waits for review for a week, it will be bumped down in the queue due to the bot action.

[Michael Rothgang]

The queueboard has a "last status change" column for precisely this reason! "update" counts any change (including you editing a comment of yours to fix a typo, or bot actions), "last status change" describes when the PR last changed from e.g. awaiting-author to awaiting review.

[Michael Rothgang]

Sorting by "last status change" is a much better criterion than "last update".

[Snir Broshi]

Michael Rothgang said:

Sorting by "last status change" is a much better criterion than "last update".

Does that mean that most reviewers/maintainers don't use the default sorting order? If so, can we make it the default? That would make it easier to know at what position a PR is in the queue

[Johan Commelin]

I use many of the different sorting orders. Sometimes I want to sprint through small PRs, so then I sort by size. Sometimes I want to see which PRs have spent the longest total time in review. Sometimes I reverse the sort, just because I want to look at some juicy new stuff. Etc...

Tl;dr: I don't even know what the default is.

[Michael Rothgang]

CC @Bryan Gin-ge Chen #35573 is missing from the queueboard --- do you know why? (The PR was opened 36 minutes ago; I would expect faster synchronisation with github, right?)

[Bryan Gin-ge Chen]

Looks like it was marked ready for review 4 minutes ago? Was it created as a draft?

[Bryan Gin-ge Chen]

I have changed the default sort order for the queueboard to be "total time in review" (descending). This should hopefully help with the issue that bot comments, etc. change the ordering of PRs in the frontend.

[Michael Stoll]

@Bryan Gin-ge Chen It looks like #35408 is missing from the queueboard. The "why is my PR not there?" page shows "???" under "CI status", even though CI is green.

BTW, It would perhaps be a good idea to add a link on the queue page to the "on_the_queue.html" page. I had to dig the link up from an earlier message in this thread.

[Michael Stoll]

Now it is back on the #queueboard, but the "on_the_queue" page shows ":cross_mark:?" under "CI status?"...

I also noticed that the link to "on_the_queue" is on #queueboard; I was using a deeper link to https://leanprover-community.github.io/queueboard/review_dashboard.html, so maybe also add the link there.

[Bryan Gin-ge Chen]

So I think I understand what's going on here. Basically, CI on the latest commit was re-run and the current backend doesn't have a good way of detecting that the re-run occurred, so things were a bit funny. I'm hoping this will be fixed after we add a webhook endpoint.

I'll also look into adding navigation links between each of the pages soon.

[Bryan Gin-ge Chen]

In the meantime I've manually re-synced the PR so hopefully it will show up when the queueboard is updated next.

[Michael Stoll]

Bryan Gin-ge Chen said:

CI on the latest commit was re-run

I think the cache upload step failed, probably due to some transient network failure, so I re-ran CI from there.

[Jon Eugster]

@Bryan Gin-ge Chen Currently there are at least 430 PR with "missing Ci information" (https://leanprover-community.github.io/queueboard/on_the_queue.html?search=%3F) which are way too many IMO.

(it's particularly annoying that all of my own PRs are among them, but that's not the main point)

Could you maybe either relax the requirements so far that these still appear on some queues or do a general (batched) re-syncing of all PRs?

[Bryan Gin-ge Chen]

Apologies, I didn’t realize there were so many. I will take a look.