Splitting the mathlib4 stream

Stream: mathlib4

[Adam Topaz]

What do people think about splitting up the mathlib4 stream into smaller parts? This is currently by far the most active stream we have right now. I think it makes sense to have a dedicated stream for porting, and one for general mathlib4 inquiries. Thoughts?

[Matthew Ballard]

Some things can naturally migrate to existing streams right?

[Adam Topaz]

I guess so, but I do think that, for example, the #PR reviews stream should remain for mathlib3 PRs and that we should have a separate stream for porting PRs

[Yaël Dillies]

Is there a point in having a non-porting mathlib4 stream, though?

[Yaël Dillies]

I would suggest renaming this stream to "porting" and then it's all pretty accurate.

[Eric Wieser]

Separate streams for "general porting problems" vs "please review my porting PR" might be useful

[Jireh Loreaux]

I don't see why #PR reviews needs to be different for mathlib3/4. I'm not having much trouble filtering interests or keeping up with the mathlib4 stream, but I am not deeply opposed to splitting either.

[Adam Topaz]

I just think that the mathlib4 stream has gotten to the point where it's hard (for me at least) to keep up with all the new unread messages I see after being offline for a while. I think splitting it up into smaller parts would make that easier.

[Yaël Dillies]

Redirecting PR review comments to #PR reviews looks reasonable to me. This stream is currently mostly dead given the lack of review of mathlib PRs.