pull request permission

Stream: new members

[Xavier Généreux]

Hello! I have been learning to write proofs in lean for some time. As a first little project, @Frédéric Dupuis suggested that I try to formalise Hadamard's three lines theorem.
As I am close to the end, I would like to create a pull request to share my proof. Would someone grant me permission?
Here is my Github: https://github.com/Louddy.
Finally, I would like to note that the project is in lean 3.

[Eric Wieser]

Invite sent!

[Xavier Généreux]

Thanks! :)

[Kostiantyn Tolmachov]

Hi all! My name is Kostya Tolmachov, I am a postdoc at the University of Edinburgh learning some Lean as a part of GlaMS course. May I have a permission to create a pull request? My username is ktlmchv.

[Kevin Buzzard]

For mathlib3 or mathlib4?

[Kostiantyn Tolmachov]

mathlib3

[Kevin Buzzard]

You know that this project is being retired, right? Are any of the files you're proposing to edit already ported to mathlib4?

[Kostiantyn Tolmachov]

I am not sure yet which files I am proposing to edit (either module/injective.lean - not ported, as far as I understand, or ring_theory/principal_ideal_domain.lean - ported, as far as I understand) - wanted to figure it out at a later stage. Do you suggest I start with porting to Lean4? Thanks.

[Kevin Buzzard]

Different people have different opinions on this matter, but my personal opinion is that right now any new PRs to mathlib3 are a step in the wrong direction, especially those that modify ported files (which are two steps in the wrong direction). Unfortunately mathlib4 is not quite ready to accept new PRs because right now the community is in a transition phase where we are porting files from mathlib3 to mathlib4. Again my personal opinion is that by far the most helpful thing that a newcomer to our community can do is to learn how to port files from mathlib3 to mathlib4, and there are details instructions on how to do this here. Note that I am not "withholding" permission for you to make PRs -- I do not have the rights to give you permissions. Furthermore I don't know your background so I don't really know what is more appropriate. What I've been telling my students is that if they are working on mathlib3 projects then they should just make a new repository of their own for now, and put their results there. But I have no idea whether you're just thinking of adding one lemma or an entire new directory consisting of a large project. The maintainers are able to give you rights to either mathlib3 or mathlib4 and once you've decided which direction you want to go you can ping them by writing @maintainers

I should stress again that other people have different opinions. What we're all agreed on is that right now we're in a transition phase and right now things are a lot more complicated than they were 6 months ago and than they will be in 6 months' time.

[Kostiantyn Tolmachov]

Got it, thank you for the explanation! My contribution is a simple exercise - proving the criterion for a module over a PID to be injective. This, naturally, uses both ported and unported libraries I mentioned. I will look if I can port an unported one first and then see what's more appropriate.

[Kevin Buzzard]

If it's just a short single-PR project filling in a hole in the library then I think it's not unreasonable to add it to mathlib3, although if you edit a ported file then it's also your job to port the edits to mathlib4. @maintainers it sounds like github user ktlmchv needs push access to non-master branches of both mathlib3 and mathlib4.

[Frédéric Dupuis]

Right now I think it very much depends on whether the PR is on parts of mathlib that are already ported (or close to the porting frontier) or not. In fact one reason I suggested a project in complex analysis to @Xavier Généreux is that it will still take several months for the port to reach this area of mathlib.

[Eric Wieser]

One advantage of working on mathlib3 (in parts yet to be ported) as a beginner is that you get to see the code you wrote automatically translated to Lean 4; which is helpful both for learning Lean 4, and for helping with the port which usually requires bits and pieces of Lean 3 knowledge