Already-forward-ported files

Stream: mathlib4

[Eric Wieser]

A summary of a remark from the meeting: there are lots of "out of sync files" at https://leanprover-community.github.io/mathlib-port-status/out-of-sync which differ by only one or two lines (the right column can be sorted), and are likely already forward ported. It would be helpful to:

• diagnose these
• create mathlib4 PRs that manually forward-port the one/two-line change (and update the SHA), and include a https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/subring/basic link in their description, so that the reviewer can visually compare the diff

We should wait for more tooling for the larger files.

[Johan Commelin]

@Eric Wieser Should it sort on the diff column by default?

[Eric Wieser]

Probably, yes

[Yury G. Kudryashov]

I'll go over the repeat/replicate today.

[Eric Wieser]

I suppose what we're missing is a mechanism to prevent two people forward-porting the same thing

[Yury G. Kudryashov]

I'll start with updating SHA sums in files that don't need to be modified.

[Yury G. Kudryashov]

E.g., !4#2116

[Yury G. Kudryashov]

(not a complete list, I'll continue later today)

[Ruben Van de Velde]

Please someone review https://github.com/leanprover-community/mathlib4/pull/1726 before starting on Finset/Multiset.Basic :)

[Eric Wieser]

Let's edit the descriptions of existing PRs to include links to the out of sync page

[Yury G. Kudryashov]

Am I right that these links will become obsolete after PRs are merged?

[Yury G. Kudryashov]

If yes, then should we move them under -- ?

[Eric Wieser]

I've updated the suggested link to contain the SHAs

[Yury G. Kudryashov]

I had to manually remove whitespaces and newline between ] and (

[Eric Wieser]

Oh, I thought it would work with that

[Eric Wieser]

I'll remove that newline again

[Eric Wieser]

The link might still become obsolete, but at least the URL will contain the relevant info and the page can add a warning saying the link no longer works

[Yury G. Kudryashov]

Updated !4#2116

[Yury G. Kudryashov]

Also, I suggest that we leave SHA sums in the URL but not in [filename]

[Yury G. Kudryashov]

BTW, what about using links to github "compare revisions" page? Then it won't become obsolete.

[Eric Wieser]

Those don't let you compare a single file

[Eric Wieser]

Besides, the port status page can always generate a link to that page based on the URL it receives

[Eric Wieser]

Here's an example of what it does with the links: https://leanprover-community.github.io/mathlib-port-status/file/algebra/big_operators/basic?range=9003f28797c0664a49e4179487267c494477d853..47adfab39a11a072db552f47594bf8ed2cf8a722

[Eric Wieser]

The link above is now more useful than it used to be, and actually highlights the commits in the URL

[Eric Wieser]

!4#2255 adds CI that generates these links automatically in review

[Notification Bot]

26 messages were moved here from #mathlib4 > Mathlib4 porting meeting series by Eric Wieser.