Zulip Chat Archive

Stream: mathlib4

Topic: How to help


Winston Yin (Nov 17 2022 at 01:24):

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 (Nov 17 2022 at 02:03):

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

Scott Morrison (Nov 17 2022 at 02:03):

It is fine to start dependent PRs.

Scott Morrison (Nov 17 2022 at 02:04):

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

Scott Morrison (Nov 17 2022 at 02:04):

Alternatively, work on the existing PRs.

Scott Morrison (Nov 17 2022 at 02:04):

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

Scott Morrison (Nov 17 2022 at 02:04):

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

Winston Yin (Nov 17 2022 at 05:31):

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

Mario Carneiro (Nov 17 2022 at 05:43):

git merge specific_PR


Last updated: Dec 20 2023 at 11:08 UTC