How easy is an easy PR?

Stream: mathlib4

[Jeremy Tan]

!4#3141 is easy, since it only modifies four SHAs

[Jeremy Tan]

@Scott Morrison is wrong

[Jireh Loreaux]

@Jeremy Tan, no, Scott is right here. The point is not just to check the diff on GitHub, the point is that one must verify that the content of the mathlib3 diffs already appear in mathlib4. This is nontrivial work.

[Scott Morrison]

This obviously takes more than 20s to review. In particular, one needs to check what has happened to the changes listed at https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/opposite?range=acebd8d49928f6ed8920e502a6c90674e75bd441..76de8ae01554c3b37d66544866659ff174e66e1f, and this is not obvious from the PR page.

Please do not add further easy tags (speaking with my maintainer hat on).

[Johan Commelin]

Declaring that someone is wrong is not a fruitful way to start a discussion.
(Especially if that person has several years and tens of thousands of lines of Lean experience.)

[Yaël Dillies]

Yeah, no, that's not an easy PR. Not too hard, but not easy.

[Jireh Loreaux]

(deleted)

[Matthew Ballard]

Does :butterfly: apply here also?

[Jireh Loreaux]

Yes, but only if it's clear what that means to the person receiving it.

[Matthew Ballard]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Community.20Guidelines

[Patrick Massot]

@Jeremy Tan, do you understand that you are being asked to no longer use the easy tag?

[Jeremy Tan]

Yes, we should eliminate it entirely

[Jeremy Tan]

There are very few situations where a review would take less than 20 seconds

[Heather Macbeth]

@Jeremy Tan There is a community consensus here which you will learn eventually. See the 2500 PRs labelled "easy" on mathlib3.
https://github.com/leanprover-community/mathlib/pulls?q=is%3Apr+label%3Aeasy+

[Jireh Loreaux]

#18519 is my most recent easy PR, just as a data point I could lay my hands on quickly. (edit: sorry, I originally had a typo in the PR number).

[Jireh Loreaux]

The easy tag has its place, it just doesn't happen to be on !4#3141 for the reasons specified above.

[Kyle Miller]

Jeremy Tan said:

Yes, we should eliminate it entirely

An easy thing you could do here is pretend it doesn't exist and not apply it to anything -- that way it effectively doesn't exist for you :smile:

(Also, please don't apply tags to other people's PRs. The community norm, or at least my understanding of it, is that the following people can apply tags: PR authors, PR coauthors, and maintainers. For example, applying awaiting-review is a decision that the author has to make; just because something passes CI doesn't mean it's ready for someone to look at. We often use PRs to keep track of work in progress.)

[Yaël Dillies]

One thing I do a lot is find a broken PR, fix it, then it awaiting-review. Even though I'm not the author of the PR, this falls under "PR coauthored" since I've touched the PR (or made sure it didn't need touching).

[Jeremy Tan]

How can I be respectful to all of you?

[Kyle Miller]

I prefer to reach out to the original PR author if possible before touching it, since you never know if they have some work in progress they haven't pushed, or they might have just gotten temporarily caught up in something.

[Jeremy Tan]

I always feel like you're all so slow

[Jeremy Tan]

Only @Eric Wieser has been able to tame me here

[Kyle Miller]

The mathlib port is important, but it's not the most important thing most of us who work on it are doing.

[Kyle Miller]

(I'm personally amazed we got to 50% already. I would have thought it would have been at least in another few months!)

[Jeremy Tan]

I do respect Eric, and I wait for Eric

[Yakov Pechersky]

Slow and steady will also prevent burnout. Breakneck pace is a recipe for miscommunication and disagreement

[Yakov Pechersky]

The port is not just an "ends". The "means" matter -- getting something right pays off in the end, instead of the instance gratification feeling of seeing some number go up quicker.

[Yaël Dillies]

You know, I am a final year undergraduate student. My end of year exams will significantly determine my future. I shouldn't be spending any time on any of this. I do it anyway (at the rate of 6 hours a day!) because I enjoy it.

[Yakov Pechersky]

Regarding "easy", it turns out to be the case that LOC changed isn't always correlated with how difficult it is to review. I think recognizing that and learning to pay attention to community behaviors is a way to succeed. We haven't yet figured out all the tooling that can track and do everything for us. So instead, we rely on human language and community decisions on how to communicate. Ignoring those, for the sake of the "tool", is missing the point. It's what the community achieves in the tool that's important, not what the tool does to the community.

[Scott Morrison]

@Jeremy Tan, my preference would be that you continue your great work making new PRs porting material from mathlib3 to mathlib4 --- this is very much appreciated! --- but that you simply stay away from others PRs for a while. It's obviously causing a lot of friction. I'm happy to try to promptly review and merge your porting PRs, as I appreciate that speedy turn arounds are helpful for the way you like to work.

[Jeremy Tan]

Scott Morrison said:

Jeremy Tan, my preference would be that you continue your great work making new PRs porting material from mathlib3 to mathlib4 --- this is very much appreciated! --- but that you simply stay away from others PRs for a while. It's obviously causing a lot of friction. I'm happy to try to promptly review and merge your porting PRs, as I appreciate that speedy turn arounds are helpful for the way you like to work.

:ok: Admittedly I'm slowly learning how to slow down here. I didn't tag Joel's chain of PRs for example

[Jeremy Tan]

Quite fittingly the character for "fast" appears in my Chinese name (the Jie in Jeremy Tan Jie Rui)

[Eric Wieser]

Jeremy Tan said:

!4#3141 is easy, since it only modifies four SHAs

For reference, this took me 5-10 minutes to review, but I imagine it would take others longer, because:

• I was the one who reviewed the corresponding mathlib3 PR so know what to expect
• The port-status pages are likely slightly less frustrating for me since I already adjusted them to match my workflow

So this certainly is not a 20 second PR. Pretty much the only plausibly "easy" sha update PRs are "someone already approved this forward port but I was stupid and forgot to actually update the SHAs in it" (I did this today...)

[Patrick Stevens]

Jeremy Tan said:

I always feel like you're all so slow

This is also the nature of large distributed projects, even if this one weren't staffed almost entirely by busy volunteers! See for example the fact that GitHub has their own internal fork of Git, which they upstream from at leisure, because that's just faster than coordinating with the distributed maintainers of Git; or for examples of what can go wrong when interacting with systems where these processes are mismanaged, see e.g. Hector Martin's adventures in upstreaming changes from Asahi to mainline Linux. Large entities are simply slower than small ones; the overhead of consensus is one of the prices you expect to pay in exchange for large parallelism and reduced bus-factors. Personally (from the outside) I'm perpetually astonished at how smoothly-functioning the mathlib project appears to be!

The desire for caution and consensus goes doubly when the project is intended to be a long-lasting foundation for other stuff, in which case it's relatively more important to get things right the first time up front: it'll be much more painful to fix later, when people are relying on it, than it is now when absolutely nobody is relying on it. You can't really blame anyone who would prefer to trade off towards "taking great care not to bake mistakes into the heart of mathlib4" rather than "get the ported lines to 100% as fast as possible" during the porting process; rejigging a million-line monolith because you made a mistake halfway up its dependency graph is not easy.

[Scott Morrison]

(Although it is easier in Lean than many other programming langauges. :-)