Stream: general

Topic: finding what happened to an identifier

Scott Morrison (Feb 08 2021 at 03:44):

I'm trying to update a branch to work with current mathlib, and an identifier has gone missing, presumably renamed in the meantime. Can someone suggest a helpful git incantation which will show me the commit in which that identifier was removed? I'm particularly looking at fin.le_iff_val_le_val at the moment (which seems to have been replaced by fin.le_iff_coe_le_coe).

Scott Morrison (Feb 08 2021 at 03:45):

(And I know from git blame that that happened in #4925 --- but how would I have done this if I hadn't stumbled upon the replacement?)

Alex J. Best (Feb 08 2021 at 03:47):

I use git log -Sstring

Alex J. Best (Feb 08 2021 at 03:48):

which gives log entries that contain "string" in their diff

Bryan Gin-ge Chen (Feb 08 2021 at 03:52):

Right, from that command, I think the PR that made the change was actually #3955: diff that hopefully highlights the change

Bryan Gin-ge Chen (Feb 08 2021 at 03:53):

Ugh, I guess not, since data/fin.lean is collapsed. Anyways, it's lines 233 on the left and 249 on the right.

Last updated: May 08 2021 at 10:12 UTC