Write access

Stream: new members

[Pim Otte]

Per this thread I'd like to try polishing up the binomial branch and PR'ing it. Could I have push access? :) My github name is pimotte

[Anne Baanen]

Done! https://github.com/leanprover-community/mathlib/invitations

[Maxime Lucas]

Hi, I am Maxime Lucas, I have worked during my years in Academia with Haskell and Coq, now I am trying out Lean.
Would it be possible to have write access to mathlib? My guthub username is MaximeLucasSky

[Bernardo Borges]

Maxime Lucas said:

Hi, I am Maxime Lucas, I have worked during my years in Academia with Haskell and Coq, now I am trying out Lean.
Would it be possible to have write access to mathlib? My guthub username is MaximeLucasSky

Not that it isn't possible, but I guess your answer will be "If you want to start contributing with mathlib (or any open source in general) you can fork the repository and open pull requests with your changes to contribute". Correct me if I'm wrong in the case of mathlib

[Riccardo Brasca]

Bernardo Borges said:

Maxime Lucas said:

Hi, I am Maxime Lucas, I have worked during my years in Academia with Haskell and Coq, now I am trying out Lean.
Would it be possible to have write access to mathlib? My guthub username is MaximeLucasSky

Not that it isn't possible, but I guess your answer will be "If you want to start contributing with mathlib (or any open source in general) you can fork the repository and open pull requests with your changes to contribute". Correct me if I'm wrong in the case of mathlib

Wait wait wait. We don't use forks, so @Maxime Lucas's question is completely legitimate.

[Riccardo Brasca]

@Maxime Lucas can you just explain (very briefly!) on what are your working?

[Maxime Lucas]

Sure! I have a proof of Cauchy-Riemann equations, and then I'll probably prove some stuff about Riemann Surfaces

[Riccardo Brasca]

Invitation sent!

[Bernardo Borges]

@Riccardo Brasca what is the intended way to contribute? Is there a documentation page on that?

[Michael Rothgang]

@Bernardo Borges Have you seen the contribution guide already? If this does not answer your questions, feel free to ask again!

[Bernardo Borges]

While you're working on a new contribution to mathlib, you should do this on a different branch. It's okay to do this in your own fork of the mathlib repository, or you can introduce yourself on Zulip and ask for write access to non-master branches of the mathlib repository, you can either make your own thread to introduce yourself, or ask for access in this topic.

So, is this out of date info or we actually do have the option of using a fork?

[Michael Rothgang]

You can technically open a PR from a fork - but mathlib's CI cannot run on it, so it cannot be merged. In other words: for PRing something, please create a mathlib branch and file a PR from that.
The guide says so a few sentences later.

[Michael Rothgang]

Granted, that could be confusing!

[Michael Rothgang]

I guess the guide tries to say "using a fork is totally fine for tinkering locally" - but to push to mathlib, please create a branch there. I wonder if this should be changed, this difference is subtle...

[Bernardo Borges]

And therefore a contributor has to have write access to mathlib, and has to state here in zulip what the project is beforehand. Is this the procedure?

[Michael Rothgang]

That's the usual procedure, yup.