PR summary automation downstream of mathlib

Stream: general

[Damiano Testa]

For a project downstream of mathlib, I was missing the PR summary automation, so I wrote a script that copies it over. If you also want to use it, you can find the script that I wrote here!

[Damiano Testa]

(By the way, I do not think that the project needs to be downstream of mathlib for the automation to work, but

• I have not tested it in this situation;
• you will still have to point the script to a copy of mathlib's root directory.)

[Kim Morrison]

Ideally rather than a script which automatically incurs technical debt (unsynchronized copies of code being spammed across repositories!), we would instead package up the PR summary automation as a GitHub action, and remove the original code from Mathlib itself.

(AI is good at this sort of task!)

[Damiano Testa]

I created a standalone GitHub action for the PR summary, but have only tested on two of my repos.

If you want to try it, you can use a very preliminary version by adding a file containing

name: PR Summary
on:
  pull_request_target:

# Limit permissions for GITHUB_TOKEN for the entire workflow
permissions:
  contents: read
  pull-requests: write  # Only allow PR comments/labels
  # All other permissions are implicitly 'none'

jobs:
  pr-summary:
    runs-on: ubuntu-latest
    steps:
      - uses: adomani/PR_summary/@dev

in your .github/workflows directory. Once you merge it into master, the action will create a report on every push to every PR.

By default it runs the import diff, the declarations diff and the renamed/removed files checks.

The action has a few configuration options that I am happy to discuss, but right now, I would like to know that at least it does something useful if used as is! :slight_smile:

[Chris Henson]

I think this is a great idea. A couple of small suggestions/problems I'm having testing:

• In the above I would suggest pull_request vs pull_request_target for simplicity in getting started (since the former uses the merge commit, you can see that it's working on the PR adding the workflow)
• There is an Mathlib-specific assumption that a merge-conflict label exists, so it is currently failing for me (testing in Cslib) before it gets to the actual diff.

[Damiano Testa]

Ah, there are a couple of labels that the script expects: let me find them.

[Damiano Testa]

As for pull_request, I thought that it was "safer" to use pull_request_target, but I am not really sure about the details.

[Damiano Testa]

The script expects these labels:

• file-removed
• large-import
• merge-conflict

[Damiano Testa]

I wonder if I could make the trigger customizable, so that you can run the workflow on pull_request or pull_request_target by setting a flag.

[Chris Henson]

To clarify for everyone: I just meant pull_request if you're doing a quick test in your repo and want to see if it immediately works. We should probably use pull_request_target in general.