Zulip Chat Archive

Stream: general

Topic: finding what happened to an identifier


view this post on Zulip 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).

view this post on Zulip 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?)

view this post on Zulip Alex J. Best (Feb 08 2021 at 03:47):

I use git log -Sstring

view this post on Zulip Alex J. Best (Feb 08 2021 at 03:48):

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

view this post on Zulip 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

view this post on Zulip 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