Algebraic Geometry Library

Stream: mathlib4

[Brian Nugent]

Hello! I am a postdoc at the University of Utah working in algebraic geometry and I would like to contribute to the AG library in mathlib. I just finished formalizing some facts about Artinian schemes (quasi-compact schemes that are locally spec of Artinian rings) and I'm about to make my first PR. Is there anyone currently working on the AG library in mathlib?

[Adam Topaz]

Pinging the usual suspects: @Andrew Yang @Christian Merten @Junyan Xu

[Andrew Yang]

Hi! There are a few active contributors to algebraic geometry in mathlib but not many. AFAIK no-one is working on artinian schemes and we would love a PR on that! Feel free to request my review once that is open.

[Brian Nugent]

Thanks! How do I request a particular reviewer on my PR?

[Christian Merten]

On a pull request, in the top right there is a "Reviewers" section. If you click on the little wheel, you can select a reviewer.

[Andrew Yang]

There are these panels on the sidebar of a PR page once you opened it and you can select me (erdOne). But also you can just ask here or on the #PR reviews channel or just DM me :)
image.png

[Brian Nugent]

Got it, thank you! I just opened the PR.

[Adam Topaz]

@Brian Nugent if you PR number is ***** and you write #***** here, it would create a link and provide additional visibility to reviewers.

[Brian Nugent]

#32412

[Brian Nugent]

Oh, that's cool

[Snir Broshi]

Andrew Yang said:

There are these panels on the sidebar of a PR page once you opened it and you can select me (erdOne). But also you can just ask here or on the #PR reviews channel or just DM me :)
image.png

This is what I see on my own PR:
image.png

I think having the "Request" button and cog wheels as in your screenshot requires permissions to the repo, no?
Is Mathlib still willing to give permissions to contributors, now that it transitioned to fork-based workflows?

[Christian Merten]

Can you not click on "Reviewers"? Brian managed to request a review on the above PR and they are a new contributor, so don't have any special permissions.

[Snir Broshi]

No, there's nothing clickable other than "Convert to draft".
Also the "Edit" button at the top only lets me edit the PR title.
What am I doing wrong then? I'd really appreciate help on solving this, especially if it'll let me edit tags :folded_hands:

[Andrew Yang]

I think you might need triage access to do this, which Brian somehow does seem to have.

[Snir Broshi]

Andrew Yang said:

I think you might need triage access to do this, which Brian somehow does seem to have.

How do I get such access?

[Kim Morrison]

@Snir Broshi, please check your email inbox for an invite for triage access.

[Snir Broshi]

Thank you!