diffing porting PR against initial commit

Stream: mathlib4

[Kevin Buzzard]

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]

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

[Shreyas Srinivas]

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]

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

[Kevin Buzzard]

Thanks!

[Shreyas Srinivas]

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

[Shreyas Srinivas]

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]

You can also git diff branch1 branch2

[Yakov Pechersky]

For the "leading" commit of that branch

[Shreyas Srinivas]

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]

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