what permissions do we need for PRs?

Stream: Infinity-Cosmos

[Emily Riehl]

I'd like anyone to be able to submit a PR to the infinity cosmos repository for review. Is this a good idea, and if so do I need to do anything with the permissions?

I ask because @Zeyi Zhao is having trouble sending us a PR from a branch of the repository (rather than a fork). How does mathlib make this possible?

I don't have a lot of experience maintaining public git repositories so general advice on this sort of thing is welcome.

[Dagur Asgeirsson]

Emily Riehl said:

I'd like anyone to be able to submit a PR to the infinity cosmos repository for review.

Anyone is able to submit a PR from a fork, this does not require any permissions

[Dagur Asgeirsson]

The way mathlib allows PRs from branches is that people who want to contribute ask for an invitation here on Zulip and then a maintainer sends them an invitation. It's probably a bad idea to allow anyone to push directly to branches of the repo

[Zeyi Zhao]

I think I shall push through a fork and see what happens.

[Kevin Buzzard]

I've been running FLT via the "submit a PR via a fork" principle and it's worked fine so far. The only objection I've had so far was from Yael Dillies, who complained that they were collaborating with someone else on a PR and the fork process apparently made it harder. But my understanding is that PRs from forks are the normal way that github is supposed to be used, and it's mathlib which is the outlier. The reason is that after every PR the mathlib people want a huge amount of stuff to be run to check that the PR passes various tests, and they apparently can't run these tests on PRs from forks. that is incorrect: the reason is to do with olean caches.

[Emily Riehl]

Some questions:

(1) How would I as a maintainer send an invitation (what sort of invitation?) if we were to go the mathlib route?

(2) Do folks create and delete forks for every PR? Or does it make sense to make one fork of a repository and use it always? If the latter, does the user have to manually keep the fork up to date?

[Nick Ward]

I don't know about (1), unfortunately. For (2), if you use a forking workflow, everyone would create a single fork and then essentially have two copies of the repository. For instance, I have write access to my fork at gio256/infinity-cosmos, but only read access to the "upstream" repository at emilyriehl/infinity-cosmos. If I had a bug fix to contribute, I would create a new branch at gio256/infinity-cosmos/bug-fix, then open a PR asking to merge the bug-fix branch of my repository into the main branch of the upstream repository (emilyriehl/infinity-cosmos/main).

You do need to keep the fork up to date, but it is the same process as incorporating changes from the main branch into a personal branch.

[Zeyi Zhao]

Zeyi Zhao said:

I think I shall push through a fork and see what happens.

Follow up question: If I already have a fork, How do I create a new pull request?

[Nick Ward]

@Zeyi Zhao If you visit the forked repository on github and select the branch you want to PR, you should see "This branch is n commits ahead of emilyriehl/infinity-cosmos:main" at the top of the page. Next to that you can click "Contribute" and then "Open Pull Request".

[Zeyi Zhao]

Nick Ward said:

Zeyi Zhao If you visit the forked repository on github and select the branch you want to PR, you should see "This branch is n commits ahead of emilyriehl/infinity-cosmos:main" at the top of the page. Next to that you can click "Contribute" and then "Open Pull Request".

Thanks for your help! I got it.

[Johan Commelin]

Emily Riehl said:

Some questions:

(1) How would I as a maintainer send an invitation (what sort of invitation?) if we were to go the mathlib route?

image.png

• Click on "Settings" in the menu at the top of the page of your repo.

image.png

• Click on "Collaborators and teams" in the vertical menu that appears on the settings page
• Authenticate

image.png

• Click "Add people"

image.png

• Search for the github username
• Choose "write" access for the role

[Floris van Doorn]

I recommend to not go via the Mathlib route, but just let contributors create a fork, and make a pull request from forks.

The only reason that we use our setup in Mathlib, is that we make the olean cache available for all branches of Mathlib, and it's tricky to do that for forks.

[Floris van Doorn]

You can still add contributors via Johan's instructions if you want to add additional people that are able to merge pull requests.

[Eric Wieser]

Kevin Buzzard said:

The only objection I've had so far was from Yael Dillies, who complained that they were collaborating with someone else on a PR and the fork process apparently made it harder

This can be resolved either by having Yael ask the author direct permission to their fork, or you deciding to give Yael maintainer powers on FLT (which grants access to PRs from forks too); which is to say, either you have to opt into giving Yael this power globally, or each contributor has to do so.

[Kevin Buzzard]

I edited my post above removing my claim that the issue was CI and replacing it with the claim that it's oleans. Thanks Eric for the explanation of how to do the joint PR thing -- mathlib was basically my first experience with open source coding and FLT is my second.

[Emily Riehl]

What is an "olean" (aside from a city in New York, which is what google tells me)?

[Damiano Testa]

It is one of the kinds of files that Lean produces while type-checking. Lean produces a few different files, containing different information, the oleans is where basically all the typing information is contained. When you import a file, Lean checks to see if there are available oleans for all the dependencies: if it finds them, then it loads the pre-processed information contained in them, instead of re-building the files. Loading is much faster than rebuilding.

[Damiano Testa]

(Also, .olean is the extension of such files.)

[Adam Topaz]

IIUC the *.olean name is meant to be analogous to *.o for c programs

[Kevin Buzzard]

It's the 5000 things which get downloaded when you type lake exe cache get which mean that you don't have to wait for 2 hours when you type import Mathlib

[Zeyi Zhao]

Nick Ward said:

Zeyi Zhao If you visit the forked repository on github and select the branch you want to PR, you should see "This branch is n commits ahead of emilyriehl/infinity-cosmos:main" at the top of the page. Next to that you can click "Contribute" and then "Open Pull Request".

Another question: what I have is I created my own fork from infinity-cosmos and I am able to create a pull request on my end. What happened is that when I log into my Github account, I can see the pull request only on my account and it does not appear on Emily's account. Ideally it should appear on Emily's end and she will be able to see it the same place where she create her own pull request. Maybe my words are quite clear because I am totally new to it. What should I do? Any help is appreciated.

[Ben Eltschig]

Do you mean this PR? it seems that you've opened it in your own fork instead of the main repository

[Zeyi Zhao]

Ben Eltschig said:

Do you mean this PR? it seems that you've opened it in your own fork instead of the main repository

I think you are right. I need to open it in the main repository. What I am trying to do is I have some code to send to Emily(merge them into the main repository?) and I am trying to do by creating a pull request.

[Nick Ward]

@Zeyi Zhao Apologies, I should have explained more thoroughly. Clicking on "Open Pull Request" should bring you to the "diff" showing the lines of code that would be added or removed should your pull request be merged. At the top of this page, you can select "base repository" and a branch in the base repository, as well as "head repository" and a branch in the head repository. The "base" is where you want the code to go, and the "head" is where you want the code to come from. In this case, you want to select the following:

base repository: emilyriehl/infinity-cosmos, base: master
head repository: {username}/infinity-cosmos, compare: {branch_with_your_work}

[Zeyi Zhao]

Nick Ward said:

Zeyi Zhao Apologies, I should have explained more thoroughly. Clicking on "Open Pull Request" should bring you to the "diff" showing the lines of code that would be added or removed should your pull request be merged. At the top of this page, you can select "base repository" and a branch in the base repository, as well as "head repository" and a branch in the head repository. The "base" is where you want the code to go, and the "head" is where you want the code to come from. In this case, you want to select the following:

base repository: emilyriehl/infinity-cosmos, base: master
head repository: {username}/infinity-cosmos, compare: {branch_with_your_work}

Thanks! I will take a try.

[Nick Ward]

Feel free to send a direct message as well. Git is neat for many reasons, but user-friendliness is not among them.

[Kevin Buzzard]

Note also that this is not a lean question, there will be many resources out there on the internet explaining how to use GitHub in this way. Nick is right though, like lean it's a bit of a steep learning curve!

[Emily Riehl]

@Zeyi Zhao any luck with this?

[Zeyi Zhao]

Emily Riehl said:

Zeyi Zhao any luck with this?

So far I can see a pull request at your end. Hopefully I didn't mess up with anything in there. @Emily Riehl

[Zeyi Zhao]

Zeyi Zhao said:

Emily Riehl said:

Zeyi Zhao any luck with this?

So far I can see a pull request at your end. Hopefully I didn't mess up with anything in there. Emily Riehl

Please let me know if there are any adjustments needed.

[Emily Riehl]

Great, I see it now. I just left several comments on your code. You should be able to make the changes locally and push them back to this PR. Let me know if you have any questions @Zeyi Zhao