Pareto Distribution

Stream: mathlib4

[Alvan Arulandu]

Hey everyone! I'm new to Lean but was able to formalize the Pareto distribution https://github.com/arulandu/mathlib4/blob/pareto/Mathlib/Probability/Distributions/Pareto.lean

Was wondering if this could be useful to add to mathlib4?

[Johan Commelin]

I don't know much about probability, but this definitely sounds like it should fit (-;

[Johan Commelin]

cc @Rémy Degenne

[Rémy Degenne]

It looks good! Please make a PR!
Here are the guidelines on how to contribute: https://leanprover-community.github.io/contribute/index.html

[Alvan Arulandu]

@Rémy Degenne Here's the PR https://github.com/leanprover-community/mathlib4/pull/16712

[Rémy Degenne]

For technical reasons that have to do with our CI setup, we can't accept PRs from forks. As explained in the guidelines, if you don't have access to mathlib branches already you should give us your github username and ask for access. Then you should make your changes on a branch of the mathlib repository and PR from there.

[Rémy Degenne]

I see that you are already a collaborator, so you should be able to push your changes to a branch and open a PR from there.

[Alvan Arulandu]

Realized this after my message, setting up my branch now

[Alvan Arulandu]

@Rémy Degenne All checks pass https://github.com/leanprover-community/mathlib4/pull/16713

[Etienne Marion]

You can simply write #16713 :wink:

[Alvan Arulandu]

oh oops haha didn't realize zulip did that

[Alvan Arulandu]

@Rémy Degenne just fixed your comments in #16713

[Rémy Degenne]

Yes I saw! As I reviewed your PR, I am subscribed to it and I get an email when something happens. You don't need to additionally ping me here, and on a PR comment, and request a new review on github!
In general requesting reviews is not needed: if your PR is not awaiting-author and passes CI, it will appear on the reviewing queue, and if its t-something label is set, a competent reviewer will have a look.

[Yaël Dillies]

Actually, I have a disagreeing opinion here, Rémy

[Rémy Degenne]

I am not sure about which part you disagree, but then let's just say that this is my personal preference: I'd rather not get 5 emails for the same thing at the same moment.
Anyway that's not very important. I merged the PR. Thanks for that contribution!

[Yaël Dillies]

Sorry I had to jump out of the bus

[Yaël Dillies]

I meant to say that the main way I review PRs is by looking at my notifications. When I review a PR and leave comments, I label it awaiting-author. If the author then addresses those comments but doesn't remove the awaiting-author label immediately, I get a notification, see that the label is still there and must decide whether the author is actually done addressing my comments or not. Sometimes it's obvious, but often it's not, so I just mark the notification as read and go to the next one. If the author then removes the label without asking for my review, I don't get a second notification and the PR falls off my radar.

[Yaël Dillies]

Hence I am suggesting that PR authors removing awaiting-author somewhat later (>= 2-3min) than their last commit also request a review. I don't think this is incompatible with your suggestion?

[Alvan Arulandu]

Rémy Degenne said:

Yes I saw! As I reviewed your PR, I am subscribed to it and I get an email when something happens. You don't need to additionally ping me here, and on a PR comment, and request a new review on github!
In general requesting reviews is not needed: if your PR is not awaiting-author and passes CI, it will appear on the reviewing queue, and if its t-something label is set, a competent reviewer will have a look.

Super sorry for the inconvenience. I didn't realize that a reviewer is subscribed to notifs for comments on the issue already, and I also didn't realize that labels affect the reviewing queue. I'll make sure to be more considerate in the future, sincere apologies again

[Alvan Arulandu]

Sorry, and just to clarify, what's the best way to request a review for a new issue? (zulip ping, github ping, github review request?, label?)

[Kim Morrison]

I think the advice is:

• if it's a new PR, just make sure it is passing CI and appears on the #queue
• if, after at least a few days, you are sad that it is not getting attention, most a message on #PR reviews explaining how exciting and important your PR is :-)
• for PRs that have already been reviewed, make sure to "resolve" any finished conversations so other reviewers arriving don't need to work out the state
• removing awaiting-author when appropriate
• it's always okay to write a comment on the PR saying "I think I've done everything, and would like further review" etc
• please don't ping individual reviewers via DM on zulip unless you know it is okay (often it is, e.g. personally I appreciate pings on CI or meta PRs or Lean PRs that I've reviewed but then forgotten, but don't want pings on mathematical PRs that I've forgotten, for lack of time. :-)

[Alvan Arulandu]

ok perfect, thank you so much!