upstreaming dashboard

Stream: mathlib4

[Yaël Dillies]

I assume the upstreaming dashboard I've been spreading around needs updating? It fetches the data of mathlib PRs from the queueboard

[Yaël Dillies]

Here is the script in Toric for example: https://github.com/YaelDillies/Toric/blob/master/scripts%2Fupstreaming_dashboard.py

[Bryan Gin-ge Chen]

Yaël Dillies said:

I assume the upstreaming dashboard I've been spreading around needs updating? It fetches the data of mathlib PRs from the queueboard

I believe @Marcelo Lynch will be taking a look at this. We're keeping the legacy backend scripts running, so the currently-deployed upstreaming dashboard should continue to work for the time being. (It might be good to collect a list of all known places where that script is used though so we know where to push updates.)

[Yaël Dillies]

Bryan Gin-ge Chen said:

It might be good to collect a list of all known places where that script is used though so we know where to push updates.

I have a list of 11 of my projects/projects I help maintain that use it. I don't know of other uses.

[Marcelo Lynch]

I was able to update the Toric script to use the new API endpoint, but I'm not sure if that's the model we want to adopt for consuming this data at the moment... Because the upstreaming dashboard as a concept seems generically useful, I'm thinking of creating an action that can be used as part of the GH Pages generation to create the dashboard

[Yaël Dillies]

Indeed that has been my plan all along, but I'm not techy enough that the required time investment has so far been too high to justify

[Marcelo Lynch]

Unfortunately it seems like the Toric page-generation workflow has become too large for the runners (https://github.com/YaelDillies/Toric/actions/runs/20210338903/job/58015168843) so I'm looking into creating a smaller project to iterate on this

[Ruben Van de Velde]

I copied it a few places, I think FLT and PNT+

[Notification Bot]

6 messages were moved here from #mathlib4 > queueboard by Bryan Gin-ge Chen.

[Marcelo Lynch]

I've written a GitHub Action to generate the upstream dashboard data based on the Toric one, adapting @Yaël Dillies 's scripts to the generic case.

You can see it in action in this workflow run that has generated the .md snippets for this page based on this puppet of the Toric project

I wouldn't depend on this yet as I guess we might want to publish it from an official location rather than my username, I published it to test it end-to-end and gather feedback :)

[Yaël Dillies]

Great, thank you! Now I can request a few improvements:

1. There should be some explanation in the text as to what the list of PRs represents
2. Taking the current example, there should be a visual way to determine which of

    feat(EllipticCurve): ZSMul formula in terms of division polynomials #13782
    t-algebra, t-number-theory, blocked-by-other-PR, merge-conflict, t-algebraic-geometry
    feat(EllipticCurve): the universal elliptic curve #13847
    merge-conflict, awaiting-author, t-algebra, t-algebraic-geometry
    feat: Group scheme structure on Weierstrass curve #14167
    merge-conflict, WIP, t-algebraic-geometry, workshop-AIM-AG-2024
    refactor(Polynomial/Bivariate): swap X and Y for improved notation #27196
    WIP, t-algebra, toric

is coming from toric. I suggest you add a configurable (list of?) github label (here, toric) and then display the PRs with this label (here, #27196) in bold. The fact that you're printing the labels makes this less useful than before, but I don't find this a very strong visual signal.

3. The PR lists should be collapsible

[Marcelo Lynch]

Thanks for the feedback @Yaël Dillies ! Some comments

(1) Yeah, I guess there is a spectrum of how much 'pre-packaged' the generated files can be, where one end is "spit out the whole dashboard". I started with just the .md snippets so people can customize it however they want. But we could also toggle this with some parameter to the task. Also note that the plan is to integrate this within https://github.com/leanprover-community/LeanProject, so some of the UI choices/standardization could be made 'outside' the action that generates the snippet.

(2) Good point! I think the label idea is possible and maybe desirable anyways, but we can even know from the data which fork the PR has come from, so we can group them in that way ("from this fork" / "from elsewhere")

(3) Sure, although this and other UI points are related to my question of customizability that I touched above. But I think it makes sense as a 'default'.

[Yaël Dillies]

2. Not sure what forks have to do with this? One of my goals with the upstreaming dashboard is to allow separate people to upstream files with little to no oversight, so the relevant PRs might come from many different forks

[Marcelo Lynch]

Ah, yes, I got confused there - this whole thing is meant exactly for non-forks. Disregard :-)

[Marcelo Lynch]

I incorporated @Yaël Dillies's feedback (hopefully!). The action now

• groups PRs by 'including relevant labels' (which are an input to the action) and 'others'
• takes the website directory and writes files under _includes. It generates multiple files including the full dashboard so it suffices to {% include _upstreaming_dashboard/dashboard.md %} to get the whole thing (but one could include only certain snippets, etc.)

Latest looks here.

[Marcelo Lynch]

Eventually we could decouple the output with "Jekyll + GH Pages" but I think the point is to use it in this scenario to start

[Marcelo Lynch]

I have published the action at leanprover-community/upstreaming-dashboard-action. Hopefully this is usable as-is for current users, but additional feedback is appreciated, of course. Some tweaking might be warranted when adding it to leanprover-community/LeanProject

[Bryan Gin-ge Chen]

One quick comment is that it probably would be good to add the YAML syntax for an example workflow step using this action that people can copy and paste into their workflows.