old mathlib3 PRs

Stream: PR reviews

[Scott Morrison]

I'm not sure how many people are still looking at #queue. Could I ping for attention on two backporting PRs:

• #18740
• #18839

[Scott Morrison]

Generally, I do wonder how many @maintainers are still regularly looking at #queue (for mathlib3). I am not. There are current 97 PRs there ready for review. I think we need to plan for wrapping this up at some point. At the current rate of progress we are no more than 3-4 months from closing mathlib3, I think. (Assuming we don't close for PRs before the very last file is ported, which is a dubious assumption?) Ideas?

[Yaël Dillies]

I have been going through PRs and either making them ready or closing them and adding the tag maybe-later if they are

• still relevant
• too much work for me to port

[Yaël Dillies]

But of course there will be leftover PRs. I see two solutions for those:

• redo them from scratch (lots of work, inaccurate)
• merge the latest master, bump, let them run through mathport

[Yaël Dillies]

This is why I've been reviving so many PRs. It's less work to do them now than later.

[Scott Morrison]

Thanks, it's great that you're salvaging PRs before its too late. We just need to make sure they get merged as well. :-)

[Yaël Dillies]

Of course the PR throttling doesn't help but I'm not complaining too much because I'm supposed to be revising for my final year exams :grinning:

[Yaël Dillies]

One thing to take into account for forward-ports is that the only way a feature PR can hinder the port is if it's halfway underwater.

[Yaël Dillies]

Refactors are a different beast

[Kevin Buzzard]

One issue is that the total number of PRs is still going up; it's currently at over 500.

[Yaël Dillies]

I don't think the number of PRs is a great indication of what's happening. I've been splitting up PRs and stuff to make them more amenable to forward-porting.

[Yaël Dillies]

If you look at the distribution of PRs, most people have now less open PRs than 3 months ago, the exceptions being @Eric Wieser and I because we've taken over other people's work.

[Yaël Dillies]

And it's not really going up either. It's been stable for two weeks.

[Eric Wieser]

I'm guilty of mostly not looking at #queue, and just looking at the latest PRs to come in

[Eric Wieser]

Could I ping for attention on two backporting PRs:

Note that there is a mathport tag that I assume is intended for this sort of thing, which we should probably use to prioritize

[Eric Rodriguez]

Yeah, I revived the little weddeeburn + splitting field ones because I feel the same as Yael - it'd be a real shame to let existing work rot and not finish the PRs in Lean3

[Eric Wieser]

I'll try to look at the splitting field one again today

[Riccardo Brasca]

I just delegated it, but waiting for another look cannot harm.

[Anne Baanen]

My small slices of Lean time have been mostly occupied with directly requested reviews, with only superficial #queue checking :sad:. I have good hope that in June I'll be going through lots of the queue again!

[Eric Wieser]

Eric Rodriguez said:

Yeah, I revived the little weddeeburn + splitting field ones because I feel the same as Yael - it'd be a real shame to let existing work rot and not finish the PRs in Lean3

While reviewing this I found a lean bug, lean#804

[Jireh Loreaux]

I also have not been checking the #queue unless someone explicitly requests a review. Our semester is about to end though, so I should have more time in a week or so.

[Ruben Van de Velde]

Since we're talking about this... Thanks to Yael, #4798 (Create an inner product from a norm) is ready for review