waits requested

Stream: mathlib4

[Scott Morrison]

I just cleaned up #port-comments to remove wait requests where the PR has been merged. At the same time I add the wait-requested-on label to every mathlib3 PR for which there is a current request that a port wait for it.

These PRs are listed here, and the intersection with the #queue is here. It would be nice to clear these out of the way, so reviews are encouraged! :-)

[Eric Wieser]

Good thinking! I suppose a natural follow-up would be to have the dashboard read these labels directly, but that's maybe not worth the work

[Scott Morrison]

Hopefully not. :-)

[Scott Morrison]

Summarising the status of the wait requested list:

• #19073 is ready for review, with review requested from @Yury G. Kudryashov
• #18913 is ready for review
• #18649 and #18755 are awaiting-author @Moritz Doll
• #19008 is awaiting-author @Apurva Nakade
• #19049 and #18843 are WIP @Eric Wieser

It would be nice to get this list emptied, and then have it stay that way!

[Yury G. Kudryashov]

I will review once I add missing docstrings to deriv/*.lean

[Yury G. Kudryashov]

#19113 is blocking porting of large parts of calculus.

[Yury G. Kudryashov]

Ready for review modulo missing imports in a test. I'll fix it once I get oleans from CI

[Yury G. Kudryashov]

#19073 is on the queue

[Yaël Dillies]

Don't count me in. I have my final exams in a week

[Yury G. Kudryashov]

@Yaël Dillies Good luck!

[Eric Wieser]

Both my WIP PRs above are to leaf files, so hopefully there's no great rush to finish them; though #19049 should be easy to get over the line

[Yury G. Kudryashov]

Mathport finished, so I'm working on deriv/* now.

[Moritz Doll]

my two PRs in a file that has exactly one dependent file so not very high priority, but I try to finish them as soon as I can.

[Eric Wieser]

#19049 is now maintainer-merged