Zulip Chat Archive

Stream: mathlib4

Topic: diffing porting PR against initial commit


Kevin Buzzard (Dec 20 2022 at 14:51):

Giit noob question. I would like to diff a mathlib4 porting PR against the initial "non-master" commit to the branch, which I'm hoping is a commit of the autoported file. Right now I just do diff Mathlib/Path/To/File.lean ../mathlib3port/Mathbin/Path/To/File.lean and hope that I pulled mathlib3port at approximately the right time. Assuming the initial commit on the branch really is just a commit of the autoported file, and my HEAD is on origin/the-relevant-branch, what's a better way to do this? I know git diff something something but do I have to manually figure out the commit hashes and paste them in or is there a short cut?

Kevin Buzzard (Dec 20 2022 at 14:51):

Aah, is git diff [commit hash of initial commit on the branch] what I want?

Shreyas Srinivas (Dec 20 2022 at 14:55):

Unless the commits are tagged, you will need the commit hashes. The good news is that you don't need the full hash. the first 7 or 8 characters suffice. You can get them from git log

Shreyas Srinivas (Dec 20 2022 at 14:57):

If you only provide one hash, then you are performing a diff w.r.t your current staging area.

Kevin Buzzard (Dec 20 2022 at 15:02):

Thanks!

Shreyas Srinivas (Dec 20 2022 at 15:16):

I think people who understand math find this brief tutorial useful : https://eagain.net/articles/git-for-computer-scientists/

Shreyas Srinivas (Dec 20 2022 at 15:17):

The key point is that names are like post its. There are a handful of them. If you don't have a post it, you need to reach a node by its hash.

Yakov Pechersky (Dec 20 2022 at 15:35):

You can also git diff branch1 branch2

Yakov Pechersky (Dec 20 2022 at 15:35):

For the "leading" commit of that branch

Shreyas Srinivas (Dec 20 2022 at 15:38):

Yakov Pechersky said:

For the "leading" commit of that branch

My understanding is that this only serves the purpose Kevin describes if no commits have been made on that branch beyond the initial commit with the autoported file.

Shreyas Srinivas (Dec 20 2022 at 15:39):

OTOH, is it a good idea to tag this initial commit? Perhaps reviewers might find it useful.


Last updated: Dec 20 2023 at 11:08 UTC