Tracking upstreaming PRs?

Stream: Carleson

[Joachim Breitner]

Just wondering: Do you happen to keep track of which mathlib PR came out of the Carleson projects, maybe to show off in the end “…and we contributed $n$ changes to mathlib?

[Floris van Doorn]

Yes, please just write "from the Carleson project" at the end of your commit message / PR description

[Yury G. Kudryashov]

Another option is to create a github "project" and add relevant PRs to this project. This can be done even after a PR is merged.

[Kim Morrison]

Another perfectly reasonable option is a label. It's more visible than a project, but I don't see that as being a bad thing.

[Johan Commelin]

We could have a bunch of project-XYZ labels. Maybe some of the existing labels should be renamed, to keep things mildly organized?

[Yaël Dillies]

Personally I've been adding From LeanAPAP/From LeanCamCombi/From PFR every time I upstream something and it works

[Joseph Myers]

It might be interesting to have statistics on commits coming from different projects (like the contributor statistics we used to have for mathlib3). Though if you look for lines starting "From" or "from" in commit messages, in either mathlib3 or mathlib4, you'll discover there are a lot of irregular cases that would complicate getting good statistics.

[Jeremy Tan]

Note: #16970 upstreams a lemma I needed for the project relating to max/min elements that are also upper/lower bounds