How to help

Stream: mathlib4

[Winston Yin]

I've got some time to help with porting mathlib while the UC academic workers strike is ongoing. What's the best way to help? Should I wait until the PR-ed files are merged before attempting its succeeding file? I'm having trouble finding a "No" that isn't preceded by a "No: PRd as ..." on the port status page. I've already watched the video tutorial and got it all set up to begin.

[Scott Morrison]

As you observe, right now we have a lot of PRs in progress!

[Scott Morrison]

It is fine to start dependent PRs.

[Scott Morrison]

Just use the block-by-PR label on github, and be prepared for some breakage.

[Scott Morrison]

Alternatively, work on the existing PRs.

[Scott Morrison]

Often when something is marked as awaiting-author anyone could jump in and do the work.

[Scott Morrison]

I'm expecting that real-soon-now we will be through the bottleneck and there will be too much to port.

[Winston Yin]

Thanks! Is there a git command for merging a specific PR into my local working branch?

[Mario Carneiro]

git merge specific_PR