View PRs that affect a file

Stream: mathlib4

[Tristan Figueroa-Reid]

I discussed this slightly in @Yaël Dillies 's DMs (I believe I misremembered hearing that this was in development at the Lean Together conference), but it would be really nice to have an online tool that allowed someone to see the active pull requests that affected certain lean files / folders in mathlib4.

[Tristan Figueroa-Reid]

This might have been one of the roles for the PRs tags other than assigning reviewers, but with the growing scope of mathlib4, it would be nice to see what PRs affected what section of the lean codebase for users and contributors alike to see what changes are being made to a section of mathlib that they want to use/contribute to.

[Yaël Dillies]

What do people think of adding this functionality to #queueboard ? I have code that interrogates the queueboard data in the correct way here, so it would just be a matter of piping it back into the webpage

[Tristan Figueroa-Reid]

(Meta question, but is there a list of all of these external tools? I heard that something like queueboard existed, but I've never actually seen it till now)

[Yaël Dillies]

Hopefully, #queueboard will eventually be integrated in the community website, but no there isn't such list

[Johan Commelin]

Yaël Dillies said:

What do people think of adding this functionality to #queueboard ? I have code that interrogates the queueboard data in the correct way here, so it would just be a matter of piping it back into the webpage

That sounds like a useful feature! Do you want to upstream it yourself, or would you rather prefer that Michael and I do that?

[Yaël Dillies]

I will give it a go today and, in the (likely) case I fail miserably, I will ask you to do it

[Michael Rothgang]

On the technical level, the integration should be very doable. The hardest question (to me) is "how to display this data".

[Michael Rothgang]

Tristan Figueroa-Reid said:

(Meta question, but is there a list of all of these external tools? I heard that something like queueboard existed, but I've never actually seen it till now)

I absolutely agree there should be a better list of such tools. My Lean together talk aims to collect most useful tools; you can e.g. just scroll through the slides directly.

[Yaël Dillies]

I would love if for each file it could be displayed similarly to the list of open PRs

[Yaël Dillies]

And I would love for the file for each file to be browsable like the #docs

[Edward van de Meent]

i imagine that once you've chosen some file(s), the page displaying them will display a list of prs with checkboxes, allowing you to toggle which selected PRs should be applied to the file? (possibly as a diff view?)

[Michael Rothgang]

Phew, applying a series of diffs is tricky (among others, because they might not apply cleanly on top of each other). I'd rather not re-implement that.

[Michael Rothgang]

Having a file tree like in docs, and for each file tree a table of all PRs changing that file is definitely doable. The page size might go up a bit, but if necessary one could split this into a separate page.

[Johan Commelin]

How about a search box, where you can enter a path-regex, and then show the PRs touching files that match the regex?

I might want to find all PRs that touch a certain combo of files (or some specific subdirectory, say)

[Michael Rothgang]

That's easy to do: basically have a table of all open PRs, list the matching files and search those.

[Michael Rothgang]

There is one caveat: right now, the queueboard metadata only contains the first 100 files for a PR (so such a search will not find PRs modifying 500 files). I could change that, though.

[Michael Rothgang]

There is now a table of all open PRs. I have not added the file info, in case @Yaël Dillies would like to try their luck.