Zulip Chat Archive

Stream: batteries

Topic: tidying commit messages

Bulhwi Cha (Jul 05 2024 at 08:56):

I think the following commit message would've been better without an extended commit description, which had messages of the commits that had been already merged into the main branch. Also, the coauthors should've been Mario Carneiro and me only.

It's not a big deal, but I prefer to keep commit messages tidy. In this case, squashing the commits would've helped.

commit 4115b22

Kim Morrison (Jul 06 2024 at 18:20):

I'm sorry, but I'm not sure what you're asking someone to have done differently.

Bulhwi Cha (Jul 07 2024 at 00:46):

One thing I regret doing is rebasing the branch for my PR on the main branch of Batteries. This decision led to commits that had already been merged into the main branch getting in the middle of your PR.

It wouldn't have been a problem if my PR was merged directly into the main branch, but I chose the branch for your PR as the base branch of my PR. I didn't want to suggest closing your PR. Instead, I wanted to leave it for you to decide; I'm sorry that I didn't express it clearly.

Here are some ways you could've handled this situation before merging your PR into the main branch:

How to clear away unwanted commits in your PR

Method 1

  1. Rebase the branch for your PR on the main branch.
  2. Merge my PR into your PR.
  3. Squash all commits in your PR into a single commit and edit its commit message.

Method 2

  1. Merge my PR into your PR.
  2. Rebase the branch for your PR on the main branch.
  3. Squash all commits in your PR into a single commit and edit its commit message.

Method 3

  1. Merge my PR into your PR.
  2. Reorder the commits in your PR so that those that have already been merged into the main branch precede your and my commits.
  3. Squash your and my commits into a single commit and edit its commit message.

Eric Wieser (Jul 07 2024 at 10:22):

(batteries#857 for context)

Mauricio Collares (Jul 07 2024 at 11:36):

I think using bors (and thus using the PR description as the squashed commit's message) would be a "free" way to get better messages, but there's the issue that bors is currently unmaintained and requires self-hosting. Maybe this will be easier once a Bors replacement is chosen. Doing anything manually seems too much to ask of the very small team of Batteries maintainers.

Shreyas Srinivas (Jul 07 2024 at 12:15):

I addressed in another thread where Kevin had the same issue

Shreyas Srinivas (Jul 07 2024 at 12:15):

Here : https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/how.20to.20resolve.20conflicts.20without.20messing.20up.20branch.3F/near/448724629

Kim Morrison (Jul 07 2024 at 14:08):

I'm confused, still. I hit "squash and merge", so there's only a single commit in the main history from this PR. Is the issue that the commit message contains information about the history of that branch, in the lines after the first line?

Kim Morrison (Jul 07 2024 at 14:09):

(If so, to be honest I think there is no problem here.)

Eric Wieser (Jul 07 2024 at 14:17):

I think the complaint is the very minor one that you didn't tidy the commit message, for which most of the fault falls on GitHub for generating a bad default

Richard Osborn (Jul 07 2024 at 14:18):

It is fine to create a branch off of another branch, but you should avoid rebasing to prevent already merged commits re-entering the history.

Bulhwi Cha (Jul 07 2024 at 14:21):

Kim Morrison said:

Is the issue that the commit message contains information about the history of that branch, in the lines after the first line?

Yes.

(If so, to be honest I think there is no problem here.)

I disagree, but I'm okay with your opinion. As I said before, it's not a big deal. You're one of the maintainers of Batteries, so the decision is yours.

Bulhwi Cha (Jul 07 2024 at 14:23):

Richard Osborn said:

It is fine to create a branch off of another branch, but you should avoid rebasing to prevent already merged commits re-entering the history.

My bad. When I created my branch, I didn't intend to base it on Kim's branch.

Eric Wieser (Jul 07 2024 at 14:28):

Eric Wieser said:

for which most of the fault falls on GitHub for generating a bad default

Another thing to blame is bors, which does the "right" thing. Reviewers already have to remember whether to use bors merge or click the merge button (and fight muscle memory for the former), and fixing the message after the fact is just one more thing to forget.

Kim Morrison (Jul 07 2024 at 14:36):

I will try to look more closely at the suggested commit message in future. I accept that I've become lazy here because bors let us be lazy. :-)

Joachim Breitner (Jul 07 2024 at 14:41):

Eric Wieser said:

I think the complaint is the very minor one that you didn't tidy the commit message, for which most of the fault falls on GitHub for generating a bad default

You can configure GitHub to use the PR description when squash merging these days, that's what we use for the lean4 repo, and I'd recommend that as the least bad solution

Kim Morrison (Jul 07 2024 at 22:31):

Okay, I've made this change.

Notification Bot (Jul 09 2024 at 17:16):

Synergylab 003 has marked this topic as resolved.

Notification Bot (Jul 09 2024 at 17:17):

Synergylab 003 has marked this topic as unresolved.

Last updated: May 02 2025 at 03:31 UTC