mathlib4 PR titles

Stream: PR reviews

[Apurva Nakade]

Is there a preferred style for mathlib4 PR titles? I'm looking at the commit history for mathlib4 and the commits use all kinds of conventions.

[Apurva Nakade]

Are we not reverting back to mathlib conventions?

[Scott Morrison]

I think the rule has changed to match Lean 4, so the file name isn't specified in the commit title. That is, it should be one of feat, chore, fix, doc (maybe some others?), following by a colon, followed by a very short description, and then hopefully more explanation in the PR description. (Which becomes part of the commit message when we squash merge.)

[Scott Morrison]

But we should actually decide, and document whatever the decision is!

[Jireh Loreaux]

Also perf

[Yury G. Kudryashov]

Are refactors chore, feat, or something else?

[Jireh Loreaux]

I would say it depends on the refactor.

[Eric Wieser]

Scott Morrison said:

But we should actually decide, and document whatever the decision is!

IMO the mathlib3 convention (feat(some/path): some summary) was better: It's a lot easier for me to tell whether I'm a suitable reviewer for a file if I can see an estimate of the files changed from the PR list. I don't think consistency with the Lean4 core repo is particularly important.

[Damiano Testa]

I'm also in favour of having the changed files.

Having the list readily available in the description helps to debug breaking changes, when you merge master and want to figure out what is causing issues.

[Eric Wieser]

/poll which convention should we use in mathlib4

• type(partial/path): summary, like we did in mathlib3
• type: longer summary, like the core lean4 repo does

[Eric Rodriguez]

I feel like often changed files leads to unwieldy titles. I get that homogeneity is valuable, but I think being able to make the choice is also good

[Eric Rodriguez]

I often typed feat(*) or chore(*) in mathlib3 for stuff that toiched many files in different ways

[Eric Wieser]

I think having type(*): summary for PRs that touch too many things is fine

[Mario Carneiro]

We could just make it optional? I think the file name was useless or misleading a not insignificant fraction of the time, and it's quite noisy, often using up all of the ~50 characters reserved for git commit headers

[Eric Wieser]

Do we care about the 50 character limit?

[Eric Wieser]

Most of our review happens on github where that limit is irrelevant

[Mario Carneiro]

I mean, it's a UX issue

[Mario Carneiro]

people see commits in a variety of ways, not just on github

[Mario Carneiro]

the point is so that you can easily summarize the commit in short log-like formats

[Mario Carneiro]

and github will also automatically spill some of the first line into the PR description sometimes

[Eric Wieser]

That behavior is certainly annoying, but can be overriden manually

[Mario Carneiro]

yeah but you don't always catch it, I'm sure there are plenty of those in the history

[Eric Wieser]

The behaviour is only relevant if your branch has only one commit on it though

[Eric Wieser]

Otherwise you get some stupid yourusername de slugged branch name PR title anyway

[Mario Carneiro]

sure, but that's the majority of my PRs, since I don't use commits for development until after putting the PR up

[Eric Wieser]

According to the link above some other web search I made the problem goes away if you make the PR via the github command line rather than the web interface

[Mario Carneiro]

also Mathlib/ are 8 characters I don't want to see in a PR title

[Mario Carneiro]

the whole thing looks like just so much busy work and hides the actual description. I am very happy the lean 4 convention is so much lighter and don't think we should go back. If you want to include a file name nothing is stopping you

[Eric Wieser]

I completely agree if we go back to the old convention it should be feat(Data/Nat/Basic): summary not feat(Mathlib/Data/Nat/Basic): summary; just like how we dropped src before

[Eric Rodriguez]

I'd prefer Nat/Basic there for example though

[Eric Rodriguez]

The Data/ takes a lot of space already

[Jireh Loreaux]

I think if people want to add this info it should be the first line of the body, but not included in the subject line.

[Eric Wieser]

The problem with not including this info in the title is that it's not there to help attract reviewers when looking at the PR list

[Eric Wieser]

I guess to some extent the t-topic labels can serve that role, but they're inevitably much coarser

[Eric Wieser]

My claim would be that >90% that people are actually reading the first line of a mathlib commit message, it is because they are looking (or searching) through the PR list

[Jireh Loreaux]

Yes, I would say that is what t-topic is for. The queue filtered by these is generally small enough for review.

[Scott Morrison]

How about a compromise:

• type: summary by default, unless the best way to summarise the change is by specifying the file which the PR modifies, in which case type(partial/path): missing @[simps] or type(partial/path): lemmas for X, etc is preferred?

Along with strong encouragement to use t-topic, along with a linkifier for #queue items without a t-topic for assistance managing this?