Zulip Chat Archive

Stream: mathlib4

Topic: queueboard survey

Johan Commelin (Feb 11 2025 at 14:33):

Hi mathlib users/contributors/reviewers/maintainers!

In the past few months @Michael Rothgang and I have been working on the queueboard: https://jcommelin.github.io/queueboard
It is a dashboard to help manage the reviewing and maintenance work for mathlib. Many of you have already seen it (for example in Michael's talk at Lean Together). And many of you have also been using it.

We would like to get a better sense of how the queueboard is being used, and how it can be improved. If you are part of the queueboards' target audience, then you can help us by spending < 5 minutes and filling out this survey: https://easy-feedback.com/survey/1948060/YuOBV0

Thanks a lot!
Michael and Johan

Johan Commelin (Feb 13 2025 at 05:07):

I thank the 13 people that have filled out the survey already, and kindly invite others to consider doing so as well.

Johan Commelin (Feb 24 2025 at 05:53):

Thanks for taking your time to fill out the survey. I have now closed the survey, will process the responses and get back to you with the results.

Jon Eugster (Feb 25 2025 at 09:57):

@Johan Commelin I have two more feature requests, if you could add them to your list that would be great. Both concerning https://jcommelin.github.io/queueboard/on_the_queue.html:

  • Could this page flag PRs which have no topic label. Maybe with a ⚠️ in a new column "Has topic label". (they are on the queue but might not be seen without label).
  • Could the search key be a GET field in the URL, so that I could share a link to a specific search?

Johan Commelin (Feb 25 2025 at 13:18):

Thanks! Those are both good suggestions.

Michael Rothgang (Feb 25 2025 at 15:26):

The latter is part of how I'd implement "sharing links to the dashboard". I have code which "almost works", but would welcome help with the last part.

I'm virtually without internet, but can share details next week.

Johan Commelin (Feb 28 2025 at 13:11):

Once more, I want to thank everyone for filling out the survey. Especially the responses to the open questions were very useful. I've condensed all the feedback into 17 new issues: https://github.com/jcommelin/queueboard/issues

Kim Morrison (Mar 01 2025 at 01:25):

And implicitly: anyone is welcome to learn how the queueboard works, and contribute solutions to these issues. :-)

Michael Rothgang (Mar 02 2025 at 15:04):

I am very happy to answer any questions you have and/or provide mentoring instructions for some of these issues!

Michael Rothgang (Mar 04 2025 at 15:05):

Thanks again for all the feedback. This is having an impact right now, by indicating which changes are useful. A number of visual tweaks was already merged yesterday and today.

Michael Rothgang (Mar 04 2025 at 15:18):

Let me post some low-hanging fruit where help is welcome:

  • improving the "persistent state from URLs" feature (I will post about this next)
  • allow searching the PR description also (queueboard#79): this should be relatively short; it has mentoring instructions, which hopefully explain all the key steps
  • compute the transitive closure of a PR's dependencies (queueboard#80): also has instructions, but is a big longer (and involves writing some actual logic)
  • automated reviewer suggestion (queueboard#74): most of the logic already exists, and just needs to be put together in the right way. I'll extend the current instructions in a moment.
  • improved filtering: clicking on an author name should add the author to the search terms, not replace them (remainder of queueboard#77). I have some ideas, but this will involve reading a bit about datatables

Michael Rothgang (Mar 04 2025 at 15:20):

And some more open-ended issues (which are "contributions welcome", but it's less clear to me what these need to look like):

Michael Rothgang (Mar 04 2025 at 15:35):

Here are further details on the URL searching feature: currently, specifying a search term in the URL means all tables are populated with this term. Sometimes, that's what you want, but sometimes, it isn't. I prefer a heuristic of "if a table is specified as a fragment identifier (e.g. an URL triage.html#all specifies the table all), only apply these settings to the relevant table". I cannot quite make that work; help is welcome.

Here's a somewhat minimized example (I did not try to shrink the table to e.g. two columns). The real question is in the last 20 lines: how can I

  • set the options for every table, but
  • make the particular option values depend on the particular table?
    The answer ought to be simple, for somebody who knows these things.
<!DOCTYPE html>
<html>
<head>
<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" href="https://cdn.datatables.net/2.1.8/css/dataTables.dataTables.css"
    integrity="sha384-eCorNQ6xLKDT9aok8iCYVVP8S813O3kaugZFLBt1YhfR80d1ZgkNcf2ghiTRzRno" crossorigin="anonymous">
<script src="https://cdn.datatables.net/2.1.8/js/dataTables.js"
    integrity="sha384-cDXquhvkdBprgcpTQsrhfhxXRN4wfwmWauQ3wR5ZTyYtGrET2jd68wvJ1LlDqlQG" crossorigin="anonymous"></script>
<link rel='stylesheet' href='style.css'>
<base target="_blank">
</head>
<body>
<h2 id="from-fork"><a href="#from-fork" title="all non-draft PRs, not labelled WIP, opened from a fork of mathlib">PRs from a fork of mathlib</a></h2>
  <table id="t-from-fork">
    <thead>
    <tr>
    <th>Number</th>
      <th>Author</th>
      <th>Title</th>
      <th>Labels</th>
      <th><a title="number of added/deleted lines">+/-</a></th>
      <th><a title="number of files modified">&#128221;</a></th>
      <th><a title="number of standard or review comments on this PR">&#128172;</a></th>
      <th><a title="github user(s) this PR is assigned to (if any)">Assignee(s)</a></th>
      <th><a title="this pull request's last update, according to github">Updated</a></th>
      <th><a title="The last time this PR's status changed from e.g. review to merge conflict, awaiting-author">Last status change</a></th>
      <th>total time in review</th>
    </tr>
    </thead>
    <tr>
      <td><a href='https://github.com/leanprover-community/mathlib4/pull/15617' title=''>15617</a></td>
      <td><a href='https://github.com/vigoux'>vigoux</a></td>
      <td><a href='https://github.com/leanprover-community/mathlib4/pull/15617'>perf: use foldl for implementation of Multiset.fold</a></td>
      <td><a href='https://github.com/leanprover-community/mathlib4/labels/awaiting-author'><span class='label' style='color: #000000; background: #f9d0c4'>awaiting-author</span></a></td>
      <td><span style="color:green">9</span>/<span style="color:red">0</span></td>
      <td>1</td>
      <td>1</td>
      <td>nobody</td>
      <td><div style="display:none">199-8681</div> <a title="2024-08-14 14:17">6 months ago</a></td>
      <td>2024-08-14 14:17:15+00:00 (6 months ago)</td>
      <td><div style="display:none">0-0</div> <a title="">0 seconds</a></td>
    </tr>
    <tr>
      <td><a href='https://github.com/leanprover-community/mathlib4/pull/13941' title=''>13941</a></td>
      <td><a href='https://github.com/TucanoUrbano'>TucanoUrbano</a></td>
      <td><a href='https://github.com/leanprover-community/mathlib4/pull/13941'>feat: metric entropy</a></td>
      <td>
        <a href='https://github.com/leanprover-community/mathlib4/labels/t-measure-probability'><span class='label' style='color: #000000; background: #33DBEC'>t-measure-probability</span></a>
        <a href='https://github.com/leanprover-community/mathlib4/labels/merge-conflict'><span class='label' style='color: #000000; background: #f99094'>merge-conflict</span></a>
        <a href='https://github.com/leanprover-community/mathlib4/labels/awaiting-author'><span class='label' style='color: #000000; background: #f9d0c4'>awaiting-author</span></a>
      </td>
      <td><span style="color:green">4074</span>/<span style="color:red">2</span></td>
      <td>10</td>
      <td>2</td>
      <td>nobody</td>
      <td><div style="display:none">189-86033</div> <a title="2024-08-23 16:48">6 months ago</a></td>
      <td>2024-08-23 16:48:03+00:00 (5 months ago)</td>
      <td><div style="display:none">0-0</div> <a title="">0 seconds</a></td>
    </tr>
  </table>

  <h2 id="needs-decision"><a href="#needs-decision" title="all PRs labelled 'awaiting-zulip': these are blocked on a zulip discussion or similar">PRs blocked on a zulip discussion</a></h2>
  <table>
    <thead>
    <tr>
    <th>Number</th>
      <th>Author</th>
      <th>Title</th>
      <th>Labels</th>
      <th><a title="number of added/deleted lines">+/-</a></th>
      <th><a title="number of files modified">&#128221;</a></th>
      <th><a title="number of standard or review comments on this PR">&#128172;</a></th>
      <th><a title="github user(s) this PR is assigned to (if any)">Assignee(s)</a></th>
      <th><a title="this pull request's last update, according to github">Updated</a></th>
      <th><a title="The last time this PR's status changed from e.g. review to merge conflict, awaiting-author">Last status change</a></th>
      <th>total time in review</th>
    </tr>
    </thead>
    <tr>
      <td><a href='https://github.com/leanprover-community/mathlib4/pull/12331' title=''>12331</a></td>
      <td><a href='https://github.com/mo271'>mo271</a></td>
      <td><a href='https://github.com/leanprover-community/mathlib4/pull/12331'>chore: replace `refine ?_` and `refine' _` by `apply`</a></td>
      <td>
        <a href='https://github.com/leanprover-community/mathlib4/labels/awaiting-zulip'><span class='label' style='color: #000000; background: #53A5FF'>awaiting-zulip</span></a>
        <a href='https://github.com/leanprover-community/mathlib4/labels/merge-conflict'><span class='label' style='color: #000000; background: #f99094'>merge-conflict</span></a>
      </td>
      <td><span style="color:green">200</span>/<span style="color:red">200</span></td>
      <td>136</td>
      <td>1</td>
      <td>nobody</td>
      <td><div style="display:none">213-30478</div> <a title="2024-07-31 08:13">7 months ago</a></td>
      <td>2024-05-24 18:24:14+00:00 (8 months ago)</td>
      <td><div style="display:none">0-0</div> <a title="">0 seconds</a></td>
    </tr>
    <tr>
      <td><a href='https://github.com/leanprover-community/mathlib4/pull/11800' title=''>11800</a></td>
      <td><a href='https://github.com/JADekker'>JADekker</a></td>
      <td><a href='https://github.com/leanprover-community/mathlib4/pull/11800'>feat : Define KappaLindelöf spaces</a></td>
      <td>
        <a href='https://github.com/leanprover-community/mathlib4/labels/awaiting-zulip'><span class='label' style='color: #000000; background: #53A5FF'>awaiting-zulip</span></a>
        <a href='https://github.com/leanprover-community/mathlib4/labels/t-topology'><span class='label' style='color: #000000; background: #33DBEC'>t-topology</span></a>
        <a href='https://github.com/leanprover-community/mathlib4/labels/merge-conflict'><span class='label' style='color: #000000; background: #f99094'>merge-conflict</span></a>
      </td>
      <td><span style="color:green">301</span>/<span style="color:red">2</span></td>
      <td>3</td>
      <td>38</td>
      <td>nobody</td>
      <td><div style="display:none">194-25642</div> <a title="2024-08-19 09:34">6 months ago</a></td>
      <td>2024-09-15 22:44:55+00:00 (5 months ago)</td>
      <td><div style="display:none">119-10687</div> <a title="from 2024-04-02 17:12:37 to 2024-04-02 17:14:08 (1 minute)
from 2024-04-04 05:57:14 to 2024-04-04 05:57:14 (0 seconds)
from 2024-04-04 06:52:22 to 2024-07-09 13:35:38 (3 months)
from 2024-07-09 13:35:38 to 2024-08-01 09:48:58 (22 days)">119 days</a></td>
    </tr>
  </table>

<script>
$(document).ready( function () {
  let params = new URLSearchParams(document.location.search);
  const search_params = params.get("search");
  // Options for all tables.
  let options = {
    "searching": true,
  };
  // Goal: apply the above options to every table, apply the next line
  // only to the table "t-from-fork". How to do this?
  if (params.has("search")) {
    options.search = {
      search: search_params
    };
  }
  $('table').DataTable(options);
  // The following should be equivalent to the current code, and already fails.
  // let tables = $('table.datatable');
  // for (t of tables) {
  //   t.DataTable(options);
  // }
});
</script>
</body>
</html>

Michael Rothgang (Mar 04 2025 at 15:35):

@Jon Eugster @Bryan Gin-ge Chen In case you'd like to help with the above URL searching question.

Jon Eugster (Mar 04 2025 at 18:48):

Thanks for the MWE @Michael Rothgang ! I think you can replace your <script> with something like the following.

In order to test, make sure all tables have an id and append ?search_t-from-fork=vigoux&search_t-blocked=mo271 to the url.

$(document).ready( function () {
  let params = new URLSearchParams(document.location.search);
  const search_params = params.get("search");
  console.log(search_params)
  // Options for all tables.
  let options = {
    "searching": true,
  };

  $('table').each(function () {
    let tableId = $(this).attr('id')
    console.log(`table: ${tableId}`)
    let searchParam = params.get(`search_${tableId}`)
    let tableOptions = { ...options }
    if (searchParam) {
      tableOptions.search = {
        search: searchParam
      }
    }
    $(this).DataTable(tableOptions);
  })

});

full code

Michael Rothgang (Mar 18 2025 at 10:34):

@Jon Eugster Thanks a lot, this is really helpful! Johan and I have decided to not change the behaviour of search, but this trick will be useful and necessary in other places of the queueboard.

Last updated: May 02 2025 at 03:31 UTC